### COSC-270: Artificial Intelligence

Project 3
Fall 2017

Due: T 11/7 W 11/8 @ 5 PM
13 points

For this project, you will write a theorem prover for propositional logic.

1. Write Lisp functions that convert a set of propositional logic formulas to clausal form. For example:
```> (rewrite-formula '(cond q r))
(((NOT Q) R))

> (rewrite-formula '(cond (not (and brd (not w))) hf))
((BRD HF) ((NOT W) HF))

> (rewrite-formulas '((cond p q) (cond q r) ((not r)) (p)))
(((NOT P) Q) ((NOT Q) R) ((NOT R)) (P))
```

Hint: Realize that each formula 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 formula:

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

(defun rewrite-conds (formula)
(cond
((atom formula) formula)
((= 1 (length formula)) formula)
(t (let ((bindings (match formula '(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 formula))
(list (car formula) (rewrite-conds (second formula))))
(t (list (car formula)
(rewrite-conds (second formula))
(rewrite-conds (third formula)))))))))
```

The match function unifies two expressions 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 formula. 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-formulas wffs)))
(format t "Original formulas: ~a~%" wffs)
(format t "Formulas 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-formulas wffs)))
(format t "Original formulas: ~a~%" wffs)
(format t "Formulas in CNF: ~a~%" clauses)
(prove clauses)))
```

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.

For grading, you must implement rewrite-formula and prove using the specifications:

• rewrite-formula formula((clause)+ ), and
• prove clauses[ t | nil ].

#### Instructions for Electronic Submission

The name of the file containing your Lisp functions must be named main.lisp. In a file named HONOR, provide the following information:
```Name
NetID

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

```\$ zip submit.zip main.lisp HONOR