%%  A quick introduction to Prolog


% Prolog is a programming language rooted in classical logic.
% Its most distinguishing features are *search* and *unification*

% A Prolog program consists of *predicates*. A predicate defines a relation between its arguments.
%
% A predicate has
% - a name (atom)
% - 0..n arguments that are Prolog terms
%
% A predicate consist of an arbitrary number of clauses. These denote /alternatives/:
% If any clause is true, the whole predicate is true.
%
% In its simplest form, a predicate relates *atoms*:

mentor(sokrates, plato).

mentor(plato, aristotle).

mentor(aristotle, alexander-the-great).

% Terms related by a predicate may also be *variables*.
% A variable starts with an upper-case letter or `_` (if the variable is unused)
%
% So far we've only seen *facts*. A fact is a clause with an empty body.
% When the body is non-empty, the clause is called a *rule*.
% A rule is a clause of the form
%
% Head :- Body.

mortal(X) :-
    human(X).

% In fact we can think of facts as special cases of rules, using the builtin 0-ary predicate `true`:

mentor(parmenides, zeno) :- true.

% is equivalent to
% mentor(parmenides, zeno).

% Interaction with a Prolog program is done via *queries*.
% A query is a Prolog term that may contain variables. Variables in a query are existentially quantified.
%
% In response to a query, Prolog answers with a logically equivalent answer:
%
% ?- mentor(sokrates, plato).
% true.
%
% ?- mentor(parmenides, X).
% X = zeno.

% It is worthwhile to examine what exactly Prolog means by a term like `X = zeno`:
% `=` is a binary predicate that holds iff both its arguments can be *unified*
%
% ?- sokrates = plato.
% false.
%
% ?- plato = X.
% X = plato.
%
% If multiple clauses unify with a goal, the alternatives are tried on *backtracking*

human(sokrates).
human(plato).
human(aristotle).

% ?- mortal(X).
% X = sokrates ;
% X = plato    ;
% X = aristotle.

% Predicates may also be recursive:

influenced(X, Y) :-
    mentor(X,Y).

influenced(X, Y) :-
    mentor(X, Z),
    influenced(Z, Y).

% Note how variables in the body of a clause are existentially quantified.

% ?- influenced(sokrates, X).
% X = plato ;
% X = aristotle ;
% X = alexander-the-great.

% A simple representation of directed graphs:
adj(a,b).
adj(b,c).
adj(c,a).
adj(c,d).

path(X, Y) :-
    adj(X, Z),
    path(Z, Y).

% Some additional examples
append([], Y, Y).
append([X | Xs], Ys, [X | Zs]) :-
    append(Xs, Ys, Zs).

member(X, [X |_]).
member(X, [_ | L]) :-
    member(X, L).

%% Logical Foundations
% ====================
%
% Prolog is based on the logic of first-order horn clauses.
%
% A clause is a disjunction of literals (atoms their negations), e.g.:
%
% a ∨ b ∨ (¬ c) ∨ (¬ b)
%
% Equivalently in set notation:
%
% { a, b, ¬ c, ¬ b }
%
% A Prolog program is a conjunction of clauses, i.e. a formula in
% Clause Normal Form (CNF).

rainy.
cold.

snowy :-
    rainy,
    cold.

% This Program can be translated into a formula in CNF:
% We interpret `:-` as an implication ←
%
% rainy ∧ cold ∧ (snowy ← (rainy ∧ cold))    % We swap ← for →
% rainy ∧ cold ∧ ((rainy ∧ cold) → snowy)    % We apply material implication
% rainy ∧ cold ∧ (¬ (rainy ∧ cold) ∨ snowy)  % De Morgan
% rainy ∧ cold ∧ (¬ rainy ∨ ¬ cold ∨ snowy)

% We get a set of clauses:
% 1. { ¬ rainy , ¬ cold , snowy }
% 2. { rainy }
% 3. { cold }

% One very important property presents itself here: All clauses of a
% Prolog program have at most one positive (non-negated) literal.
% A clause that observes that property is called a horn clause.
%
% To evaluate a query ⇔ prove that a query is satisfiable relative to
% a program, Prolog uses a resolution calculus.
%
% A resolution calculus is a proof calculus that works on formulae in CNF.
% In its most basic form it looks like this:
%
% A ∨ C    (¬ B) ∨ D    σ = mgu(A,B)
% ==================================
%       σ(C) ∨ σ(D)
%
% Horn clauses interact particulary nicely with this rule:
% When two horn clauses are resolved, the resolvent is again a horn clause.
%
% An example proof:
% We want to prove the goal
% ?- snowy.
%
% Resolution is a refutation calculus. To prove a goal, we show that
% its negation is unsatisfiable.
%
% We add the negated goal as a clause:
% { ¬ snowy }
%
% Now we do resolution:
%
% { ¬ snowy } + { ¬ rainy, ¬ cold, snowy } ⇒ { ¬ rainy, ¬ cold }
% { rainy }   + { ¬ rainy, ¬ cold }        ⇒ { ¬ cold }
% { cold }    + { ¬ cold }                 ⇒ ∅

% We have reached the empty clause, meaning our proof is done

% Another example:
%
% Goal:
% ?- mortal(X).
%
% Variables in a Query are existentially quantified.
% That means our goal corresponds to the following formula:
%
% ∃ X. mortal(X)
%
% We need to negate and translate this into CNF:
%
% ¬ ∃ X. mortal(X)
% [ V₁ / X ] ¬ mortal(X)    % where V₁ ∉ free(mortal(X))
% ¬ mortal(V₁)
%
% We get a goal clause:
%
% { ¬ mortal(V₁) }
%
% Program Clauses:
%
% 1. ∀ X. human(X) → mortal(X)
%    ⇒ [ V₂ / X ] human(X) → mortal(X)
%    ⇒ human(V₂) → mortal(V₂)
%    ⇒ (¬ human(V₂)) ∨ mortal(V₂)
%    ̂= { ¬ human(X), mortal(X) }
% 2. { human(sokrates) }
% 3. { human(plato) }
% 4. { human(aristotle) }
%
% Resolution:
%
% { ¬ mortal(V₁) } + { ¬ human(V₂), mortal(V₂) }  [ V₂ / V₁ ] ⇒ { ¬ human(V₂) }
% { ¬ human(V₂) } + { human(sokrates) }       [ sokrates / V₂ ] ⇒ ∅
%
% At this point, Prolog presents us with a satisfying substitution, namely
% X = sokrates.
%
% If we force backtracking, we get all other satisfying substitutions:
% { ¬ human(V₂) } + { human(plato) }          [ plato / V₂ ] ⇒ ∅
% { ¬ human(V₂) } + { human(aristotle) }  [ aristotle / V₂ ] ⇒ ∅
%
% If we backtrack again we are left with a set of clauses that doesn't
% allow us to derive the empty clause.
%
% { ¬ human(X) }
%
% Since nothing can be resolved, Prolog tells us that our goal is not satisfiable:
% false.