Fundamentals of Logic Programming (Summary Notes)

Topics:

• Sample logic program
• Process of goal satisfaction
• Unification
• List processing using terms of predicate logic

Sample Logic Program

; Here X Y and Z are variables,
; GRANDMOTHER, MOTHER, PARENT, and FATHER are predicate symbols,
; MARY, JOHN, BILL, PETER, and JAMES are constants.

The clauses above, when translated into a more English-like form, are represented by the following:

X is a grandmother of Z provided there is some Y such that X is the mother of Y and Y is a parent of Z.
X is a parent of Y provided X is the mother of Y.
X is a parent of Y provided X is the father of Y.
Mary is the mother of John.
John is the father of Bill.
Peter is the father of James.

Process of Goal Satisfaction

The interpreter for a logic programming language processes this query as follows.  It puts the query on a list called the subgoal list.  This is a list of goals that it is trying to prove.  At this point, the query is the only goal on the subgoal list.

In general the interpreter takes the next goal on the subgoal list and tries to prove it using one of two approaches:
1. matching it to a unit clause (a fact) in the database of clauses.  If it matches exactly, then this goal is proved directly.  If it matches, but requires making some substitutions of terms for variables (i.e., unification), then the unifier is recorded and applied not only to the literals being matched but to all other goals on the subgoal list, if they contain that variable.
2. matching it to the head (first literal) of a clause (possibly with a unifier, which in turn is applied to the remaining literals in the clause to obtain a new set of subgoals) and then recursively proving the new subgoals by putting them onto the subgoal list and proceeding.

Each time a rule is used, however, a copy of it is made with a new set of variables, so that the names of the variables will not possibly conflict with any existing variables.

For the query (GRANDMOTHER X BILL), let's consider what the interpreter will do.  It will start at the top of the list of rules and facts and try to match this to the first literal in each Horn clause.  Since the very first clause in the list starts with (GRANDMOTHER X Z), we get a match between first literal in a substitution instance of the first clause, e.g.,
((GRANDMOTHER X109 Z23) (MOTHER X109 Y17) (PARENT Y17 Z23))
and the query.  In this case, the unifier is ((X109 X)(BILL Z23)) which means that X109 is substituted for X and BILL is substituted for Z23.  This generates two new subgoals:  (MOTHER X109 Y17) and (PARENT Y17 BILL).  So the previous subgoal, (GRANDMOTHER X BILL) is removed from the subgoal list, and these two new subgoals are placed on the list.

Now the interpreter tries to prove (MOTHER X109 Y17) is similar fashion.  It starts at the top of the list and finds that MOTHER does not match GRANDMOTHER at all, so it moves to the next clause.  The next two clauses also fail, because MOTHER does not match PARENT.  The head of the fourth clause, however, is (MOTHER MARY JOHN). With the unifier ((MARY X109) (JOHN Y17)) the interpreter gets a match.  This unifier is applied to the remaining subgoal changing it to (PARENT JOHN BILL), and the current subgoal is removed leaving only this one to be proved.

Two more steps are needed to solve this subgoal.  (PARENT JOHN BILL) after failing to match the GRANDMOTHER literal in the first clause is matched to the head of the second rule.  This leads to a new subgoal being put on the subgoal list:  (MOTHER JOHN BILL).  When proving this is attempted, the interpreter goes through the entire list of clauses without being able to match it to any fact or the head of any rule.  This leads to backtracking.  The subgoal (MOTHER JOHN BILL) is retracted, and an alternative method of proving (PARENT JOHN BILL) is sought.  The very next clause (after the first PARENT rule) leads to another match, and this time the subgoal (FATHER JOHN BILL) is put on the subgoal list.  Fortunately, this goal is proved because it exactly matches the second to last fact in the list of clauses.

The answer to the original query is reported by looking up the term that was substituted for the X of the original query.  This term was obtained during the course of the proof by one or more instances of the process of unification.

Unification

List Processing Using Terms of Predicate Logic

By using the convention that a two-argument function CONS has roughly the meaning here that it does in Lisp, we can use logic programs to manipulate lists.  Also, we will use NILL to represent the empty list.  We avoid using NIL because of its special significance in Lisp.

Here is a predicate that is true provided its argument is a list of length 3:
(LENGTH-IS-3 (CONS X (CONS Y (CONS Z NILL))))
Here X, Y, and Z are variables while NIL is a constant.

Here is a definition of APPEND given using Horn clauses:

;;; (APPEND L1 L2 L3) is true provided L3 is the result of appending L1 and L2.
((APPEND NILL  L  L))
((APPEND L  NILL  L))
((APPEND (CONS X L1) L2 (CONS X L3)) (APPEND L1 L2 L3))

Then you can use this definition to compute the result of appending two lists by entering
a query such as
((APPEND  (CONS X (CONS Y NILL))  (CONS Z (CONS W NILL)) L))
And the result will be
L = (CONS X (CONS Y (CONS Z (CONS W NILL))))

You can also run a function such as APPEND "in reverse" with a query such as this:
((APPEND  L  (CONS Z (CONS W NILL))  (CONS X (CONS Y (CONS Z (CONS W NILL)))) ))
which leads to the result:
L = (CONS X (CONS Y NILL))
 

In order to run these examples using the Mock Prolog interpreter, do the following:
Make a copy of the file PROLOG.CL and make these changes:
Find the form that sets up the global variable *KNOWN-VARIABLES* and add into the list
of variables the ones you need here, such as L, L1, L2, and L3.
Find the code near the end of the file that sets up DATABASE1 and DATABASE2.
Using the same format, set a variable DATABASE3 to contain the definition of APPEND above.
Put in the form (SETF  *DATABASE*  DATABASE3)
Comment out the queries for DATABASE1 and DATABASE2 and create a new query:
(QUERY '((APPEND ((CONS X (CONS Y NILL))  (CONS Z (CONS W NILL)) L)))
Then load the program into Lisp and examine the trace of execution for a line of the form,
SOLUTION: L=(CONS X (CONS Y (CONS Z (CONS W NILL))))
If you prefer, you can turn off the tracing of PROLOG-UNIFY.
Or alternatively, you can turn on more tracing by entering the form (TRACE PROLOG-UNIFY1).