### COSC 387: Artificial Intelligence

Project 3
Fall 2004

Due: Nov 5 @ 5 P.M.
13 points

1. 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
```

2. 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)
```
3. 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 Submission

```;;;;
;;;; COSC [187|387] Project 3
;;;; Name
;;;; Platform: Windows, Linux, Solaris (gusun, daruma)
;;;; Lisp Environment: gcl, clisp, cmucl
;;;; Mail Client: mailx, pine, GUMail, Netscape, Yahoo!, etc.
;;;;
;;;; 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.
;;;;
```
Submit your project as a single file as an attachment to an e-mail. Send the e-mail to me. The attachment should be named so that the file stem is your NetID and the extension is .lisp.

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

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.