### COSC 270: Artificial Intelligence

Project 3
Spring 2015

Due: Sun, Mar 1 @ 11:59 P.M.
13 points

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

```cs-class% cp ~maloofm/cosc270/p3.lisp ./
```
It contains example1, example2, rewrite-conds, and match.

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

In the header comments of the primary file, provide the following information:
```;;;;
;;;; COSC 270 Project 3
;;;; Name