COSC 159 - Artificial Intelligence
                   Assignment #5

             Due: Monday, March 23

In class we've been discussing how the propositional logic theorem
prover (theorem) could be enhanced to handle predicate calculus
proofs.  In this assignment, you're asked to provide one of the
missing pieces (in the book's presentation) for that PC theorem
prover.

GOAL: Write a function called rewrite which takes
a proposition and a list of bindings and replaces each variable
in the proposition with the corresponding new variable from the
list of bindings.  The list of bindings is a list
of (old-var new-var) pairs.
 So

> (rewrite '(drives (? x) (transport (? y) (? x)))
                     '(((? x)(? v1)) ((? y)(? v2))) )

would give

(DRIVES (? V1) (TRANSPORT (? V2) (? V1)))

This type of substitution (for one variable at a time) is already
used in the function aux-unify in the text, so you might get some
ideas from there.

HAND-IN:  You should hand in sample runs showing how your
function rewrite works on some assorted
propositions.  The testfile mentioned below is a good source of
fairly complicated propositions (rules) which you might use in
these demos.

 I'd also like you to run the full predicate calculus version of
theorem using your function.  This code can be found in the file
~mikes/159/assign5dir/theorem2.lisp  on studsys.  This version
of theorem expects that you have defined functions rename and
rewrite (as described above).  So, load in your functions and
load this file and you should have a working theorem prover.
The file ~mikes/159/assign5dir/testfile  contains a few sets of
rules and statements to try and prove.  You'll probably need
to load this file in (to define the rule sets) and then type
the various calls to theorem2 by hand (or cut and paste) to
see what they do.
 This last piece is intended to be fun and gratifying (to see that
your rewrite code can do something non-trivial).  If your function
performs as described above, you shouldn't have any trouble running
the theorem proofs.  If you do have trouble, please let me know.