%We can add more facts by consulting the special program user
% ?- [user].
% | eats(tom,jerry).
% | ^D (or ^C or nothing if Windows :-()

%LAYER 3: COMPLEX FORMULAE
%These are formed by combining simpler formulae.  Only a few kinds of
%combination will be discussed right now:

%- and: in Prolog, this looks like ','
%- or: in Prolog, this looks like ';'

%Both of these combinations can be used as queries, but NOT as facts.
%(Using multiple facts in a program file is taken to mean that all of
% them are true, so that's a kind of implicit 'and'.)

:- cat(X),mouse(Y),eats(X,Y).

%Again, variables are interpreted existentially.

:- cat(X), mouse(Y), (eats(X,Y) ; chases(X,Y)).

%Note also:
:- chases(fido,X).

%has more than one solution, even though it does not use
%';'.

%Another combination:
%- implication: in Prolog, these are very special.  They are
%written backwards (conclusion first), and the conclusion must
%be an atomic formula.  This backwards implication is written as
%':-', and is called a *rule*.

%Rules can be used in programs to assert implications, but NOT
%in queries.

%Examples:
eats(X,Y) :- cat(X), mouse(Y).

%The consequent, eat(X,Y), comes first.  This is called the *head*.
%The antecedent comes second.  It is called the *body*, and each
%conjunct is called a *goal*.  Queries also consist of goals.

%Prolog interprets free variables in the head of a rule UNIVERSALLY.
%So this rule means, "For all X, for all Y, if X is a cat, and Y is a
%mouse, then X eats Y."

eat(fido,X). % in a program

%This means "For all X, Fido eats X."  Because of Prolog's typing,
%Fido even eats Fido!

%Facts in programs are really rules with trivial bodies:

eat(fido,X) :- true.

%'true' is a 0-ary predicate that is always true.

%Free variables in the body that do not appear in the head are still
%quantified EXISTENTIALLY. Example:

ancestor(X,Y) :- parent(X,Y).
ancestor(X,Y) :- parent(X,Z), ancestor(Z,Y).

%The second rule means:
%"For all X, for all Y, if there exists Z such that X is Z's parent, and
%Z is an ancestor of Y, then X is an ancestor of Y."

%If these are also in our program
parent(george,jeb).
parent(george,w).
parent(herbert,george).
parent(satan,herbert).

%If we begin with the query:
:- ancestor(satan,w).

%then we can prove the truth of this query by *reduction*.
%Reduction of goal G by program P is the replacement of G
%by the body of a rule in P, whose head matches G.

%_ancestor(satan,w)_
% => _parent(satan,herbert)_, ancestor(herbert,w)
% => (true,) _ancestor(herbert,w)_
% => _parent(herbert,george)_, ancestor(george,w)
% => (true,) _ancestor(george,w)_
% => _parent(george,w)_
% => true

%HORN CLAUSES
%Prolog is a *declarative* programming language:
%  - programmer declares knowledge about the world,
%  - Prolog's built-in reduction procedure performs search relative to
%    this declarative knowledge, given a query.

%*Horn Clause*:
%forall X1...Xk. [A <- B1 & B2 & ... & Bj], k,j>=0,
%  where A is an atomic formula.

%A *logic program* is a collection of horn clauses.
%Each clause can be regarded as a kind of procedure definition, e.g.:
p(X) :- q(X,Y), r(X,Y).

%p/1 is the name of the procedure  (head predicate)
%X is the formal parameter to p/1  (head variable - these are universally
%  quantified)
%Y is a local variable (free body goal variable - these are existentially
%  quantified)
%q/2, r/2 are subroutines called by p/1

%Why are these not Horn clauses?
% exists X. [a(X) <- b(X)]
% forall X. exists Y. [wife(X) <- married(X,Y)]

%Why are these not well-formed Prolog rules/facts?
% ~b :- a.
% a ; b.
% a;b :- c.
% a :- (b :- c).
% red(X) ; white(X) :- flag(X).

%Inference with non-Horn formulae is much more difficult, e.g.:
% a :- b.
% a :- c.
% b ; c.

%?- a.
%a is actually true, even though we don't know whether b or c is.
%Prolog can't do this kind of reasoning.

%On the other hand, many non-Horn formulae can be converted into
%logically equivalent Horn-formulae, using:
%  - propositional tautologies, e.g.:
%        ~~a LEQV a                 (double negation)
%   ~(a v b) LEQV ~a & ~b           (DeMorgan)
%a v (b & c) LEQV (a v b) & (a v c) (distributivity)
%     a <- b LEQV a v ~b            (implication)

%Examples:
%1)
%~b <- ~a => ~~a v ~b
%         => a v ~b
%         => ~b v a
%         => a <- b
%How do we express this in a Prolog program?

%2)
%a <- (b v c) => a v ~(b v c)
%             => a v (~b & ~c)
%             => (a v ~b) & (a v ~c)
%             => (a <- b) & (a <- c)
%How do we express this in a Prolog program?

%3)
%a v b <- b => (a v b) v ~b
%           => a v (b v ~b)
%           => a v true
%           => true
%How do we express this in a Prolog program?

%  - Skolemization: the elimination of existential
%    quantifiers through the introduction of new
%    functions or constants, e.g.:

%1)  exists X. parent(X,john) => parent(p,john) [p/0 new]

%2)  forall X. person(X) <- exists Y. parent(Y,X)
%   => forall X. person(X) <- parent(p(X),X) [p/1 new]

%How do we express these in Prolog?
person(X) :- parent(Y,X).
person(X) :- parent(p(X),X).

%In (1), p is called a *Skolem constant*.
%In (2), p(X) is called a *Skolem function*.
%In general, the Skolem function/constant is dependent
%  on the universally quantified variables within whose scope
%  it is used.