COSC 387 Project 3

COSC 387: Artificial Intelligence

Project 3
Spring 2008

Due: Wed, Mar 19 @ 5 P.M.
13 points

I have taken the liberty of putting the code on this page in a file on seva, which you can retrieve using the command:

seva% cp ~maloofm/cosc387/p3.lisp ./

It contains example1, example2, rewrite-conds, and match.

Write Lisp functions that convert 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 nodes of COND, 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 conditional operators in a clause:

;;;
;;; rewrite-conds
;;;
;;; Rewrites (cond p q) as (or (not p) q)
;;;

(defun rewrite-conds (clause)
  (cond
    ((atom clause) clause)
    ((= 1 (length clause)) clause)
    (t (let ((bindings (match clause '(cond (? x) (? y)))))
         (cond ((not (null bindings))
                (let ((phi (rewrite-conds (second (first bindings))))
                      (psi (rewrite-conds (second (second bindings)))))
                  (list 'or (list 'not phi) psi)))
               ((eq 'not (car clause))
                (list (car clause) (rewrite-conds (second clause))))
               (t (list (car clause)
                        (rewrite-conds (second clause))
                        (rewrite-conds (third clause)))))))))

The match function unifies two clauses and returns a binding list Use the question mark as the first element of a list to signify a variable. These should appear in the second clause. For example:

>(match '(f a) '(f (? x)))
(((? X) A) (MATCH T))

>(match '(f a) '(g (? x)))
NIL

>(match '(f a b) '(f (? x) (? y)))
(((? X) A) ((? Y) B) (MATCH T))

>(match '(f a b) '(f (? x) (? x)))
NIL

Write Lisp functions that implement a resolution theorem prover. Given a set of clauses in clausal 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)
```

Use the following two functions to test your code. They are for the two propositional logic problems presented in lecture. Include them when you submit your project.

(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 Electronic Submission

In the header comments of the primary file, provide the following information:

;;;;
;;;; COSC 387 Project 3
;;;; Name
;;;; E-mail Address
;;;; Platform: Windows, Linux (seva), etc.
;;;; Lisp Environment: clisp, gcl, cmucl
;;;;
;;;; In accordance with the class policies and Georgetown's Honor Code,
;;;; I certify that, with the exceptions of the course materials and those
;;;; items noted below, I have neither given nor received any assistance
;;;; on this project.
;;;;

If you need to submit a single file, assuming its name is p3.lisp, type

seva% java -jar submit.jar -a p3 -f p3.lisp

If you need to submit multiple files, if you haven't already, place all of your code in a subdirectory named p3. To create this subdirectory, type

seva% mkdir p3

To descend into the directory, type

seva% cd p3

All of the files for your project should be in this directory. The submit program should be above this directory:

seva% ls ..
p3/ submit.jar

If you need to include a message to me about your submission, then place the message in a file named README. Place the README file in the project's directory.

To move up from the p3 directory, type

seva% cd ..

You should be above the p3 directory:

seva% ls
p3/ submit.jar

(Additional useful Unix commands)

When you're ready to submit, change the name of the directory to your netid. For example, if your netid is maloofm, then rename the directory p3 by typing

seva% mv p3 maloofm

Create a zip file of the directory and its contents by typing

seva% zip -r p3.zip maloofm/*

This command creates a zip file named p3.zip by recursively (-r) copying all of the files (*) from the directory maloofm/.

To submit the zip file type

seva% java -jar submit.jar -a p3 -f p3.zip

p3 is the name of the assignment (-a) and p3.zip is the file (-f) to be submitted for that assignment.

If the program submits the file successfully, you will receive a receipt by e-mail at the address <netid>@georgetown.edu.

Submit your project only once.

Once you've submitted your project, it is important to keep an electronic copy on a university machine (e.g., seva) that preserves the modification date and time. If we lose your project or the submission 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.

You can also change the directory's name back to the original name. For example,

seva% mv maloofm p3

Note that changing the name of the directory does not change the dates of the files in the directory. You can also remove the zip file from your directory:

seva% rm p3.zip

You must submit your project before 5 PM on the due date.

Plan B

If something goes wrong with submit, then send your project as an attachment to an e-mail to me. Remember that UIS strips zip files from e-mails, so rename your zip from p3.zip to p3.piz, or something like that.