Horn Clauses and Prolog

Proof by resolution involved finding the conjunctive normal form, which comprised conjoined clauses, each of which was a disjunction of literals - ie,

L1 L2 L3 ...
A slightly form of this is a Horn Clause, where the restriction is that only one of the literals is un-negated. For example:
1. L1 L2 L3 ...
2. L1 L2 L3 ... M
3. M
4. L1
are all Horn Clauses. It is straightforward to show that, for example, (2) is equivalent to
L1 L2 L3 ...=> M
or in goal-directed form:
M Ü L1 L2 L3 ...

This is the typical form of a statement in the logic programming language Prolog. There are two modes in Prolog. In the consult mode, one supplies the system with axioms. (Note that the ``Ü'' is replaced by ``:-'', that capitalized symbols are variables, and that the ``.'' is important.) 

grandson(X,Y) :- son(X,Z),parent(Y,Z).
son(charles,elizabeth).
parent(george,elizabeth).
In query mode we might ask 
?- grandson(elizabeth,charles).
no
with Prolog telling us that there are no database facts to verify the statement. Or we might ask 
?- grandson(W,george).
Starting with this query, Prolog tries to justify each literal on the RHS by finding a matching literal in the LHS of another clause in the database. In our example, it would find dbase statement 1 and perform the unification (W/X, george/Y). So the RHS becomes son(X,Z),parent(george,Z). It then uses dbase statement 2 to perform the unification (X/charles, Z/elizabeth), leaving parent(george,elizabeth) to be verified. Obviously, dbase statement 3 does this with no unification. The system returns the unification for W which is (W/X/charles), ie charles. 
?- grandson(W,george).
W = charles ?
yes
<<<Previous Next>>>