COSC-270 Project 3

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.

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

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

When you are ready to submit your project, create the zip file for uploading by typing:

$ zip submit.zip main.lisp HONOR

Upload submit.zip to Autolab. You can submit to the compile check p3c seven times. You can submit your assignment p3 twice, but you won't see the output from the autograder until I review, grade, and return your project.

Plan B

If Autolab is down, upload your zip file to Canvas.