COSC 387: Artificial Intelligence

Project 3
Fall 2000

Due: Nov 8 @ 5 P.M.
10 points

1. Write a set of Lisp functions that converts a set of propositional logic clauses into clausal form. For example:

   >(rewrite-clause '(cond q r))
   ((NOT Q) R)
   
   >(rewrite-clause '(cond (not (and brd (not w))) hf))
   ((BRD HF) ((NOT W) HF))
   
   >(rewrite-clauses '((cond p q) (cond q r) ((not r)) (p)))
   (((NOT P) Q) ((NOT Q) R) ((NOT R)) (P))
   

   Hint: Realize that each clause is a tree with parent node of COND, BICOND, AND, OR, and NOT. First write a Lisp function that traverses this expression tree. Then insert calls to the match function from match.lisp to find the pattern you want to rewrite. Here is a function that rewrites the biconditional operator:

   ;;;
   ;;; rewrite-biconds
   ;;;
   ;;; Rewrites (bicond p q) as (and (or (not p) q) (or (not q) p))
   ;;;
   
   (defun rewrite-biconds (clause)
     (cond
       ((atom clause) clause)
       ((= 1 (length clause)) clause)
       (t (let ((bindings (match clause '(bicond (? x) (? y)))))
            (cond ((not (null bindings))
                   (let ((phi (rewrite-biconds (second (first bindings))))
                         (psi (rewrite-biconds (second (second bindings)))))
                     (list 'and (list 'or (list 'not phi) psi)
                                (list 'or (list 'not psi) phi))))
                  ((eq 'not (car clause))
                   (list (car clause) (rewrite-biconds (second clause))))
                  (t (list (car clause)
                           (rewrite-biconds (second clause))
                           (rewrite-biconds (third clause)))))))))
   

2. Write a set of Lisp functions that implements a resolution theorem prover. Given a set of clauses in conjunctive normal form, the primary function should return true if it can derive the empty set from the clauses. For example:

   >(prove '(((NOT P) Q) ((NOT Q) R) ((NOT R)) (P)))
   T
   

   Hint: A useful Lisp function that we did not cover in class is the remove function, which simply removes an element from a list. For example:

   >(remove 'a '(b c d a e f g))
   (B C D E F G)
   

   The default test for this function is #'eq, so, in the default mode, you can't remove lists from lists:

   >(remove '(a b) '(b c (a b) e f g))
   (B C (A B) E F G)
   

   You can, however, supply another test for the remove function. Recall that we can use #'equal to compare lists, so we can type:

   >(remove '(a b) '(b c (a b) e f g) :test #'equal)
   (B C E F G)
   

3. Use the following two functions to test your code. They are for the two propositional logic problems presented in lecture.

   (defun example1 ()
     (let* ((wffs '((cond p q)
                    (cond q r)
                    ((not r))
                    (p)))       ; negated conclusion
            (clauses (rewrite-clauses wffs)))
       (format t "Original statements: ~a~%" wffs)
       (format t "Clauses in CNF: ~a~%" clauses)
       (prove clauses)))
   
   (defun example2 ()
     (let* ((wffs '((cond (not hf) w)
                    (cond (not w) (not brd))
                    (cond (not (and brd (not w))) hf)
                    (cond (not (or (not hf) (not brd))) (not brch))
                    (brd)
                    (brch)))    ; negated conclusion
            (clauses (rewrite-clauses wffs)))
       (format t "Original clauses: ~a~%" wffs)
       (format t "Clauses in CNF: ~a~%" clauses)
       (prove clauses)))
   

Instructions for Submission: Although you can use any Common Lisp environment, all programs must run under GNU gcl. When you are ready to submit your program for grading, e-mail it as one file to the TA using the last four digits of your student ID and the suffix ``.lisp'' as the subject line.

For example, if the last four digits of your student ID is 1234, the name of your source file is proj1.lisp, and your TA's e-mail address is ``imagoodtamaloof@cs'', then you would type at the UNIX prompt:

gusun% mailx -s "1234.lisp" imagoodtamaloof@cs < proj1.lisp

Once you submit your project, it is important to keep an electronic copy that preserves the modification date and time. If we lose your project or the e-mail system breaks, then we will need to look at the modification date and time of your project to ensure that you submitted it before it was due.

Finally, when storing source code on university machines, it is important to set file permissions so others cannot read the file. To turn off such read/write permissions type at the UNIX prompt chmod og-rw <file>, where <file> is the name of your source file.