;;;; Rebecca Orton
;;;; COSC 387: Artificial Intelligence
;;;; Project 3
;;;; Fall 2000
;;;; Due: Nov 8 @ 5 P.M.
;;;; 10 points
;;;; Number 1 - Write a set of Lisp functions that converts 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 node of COND, BICOND,
;;;; AND, OR, and NOT. First write a Lisp function that traverses this
;;;; expression tree. Then insert calls to the match function from match.txt to
;;;; find the pattern you want to rewrite.
(load "match.txt")
;;;
;;; Step 1
;;;
;;; 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)))))))))
;(rewrite-conds '(cond x y))
; result = (OR (NOT X) Y)
;;;
;;; Step 2
;;;
;;; rewrite-biconds
;;;
;;; Rewrites (bicond p q) as (and (or (not p) q) (or (not q) p))
;;;
(defun rewrite-biconds (clause)
(cond
((atom clause) clause)
((= 1 (length clause)) clause)
(t (let ((bindings (match clause '(bicond (? x) (? y)))))
(cond ((not (null bindings))
(let ((phi (rewrite-biconds (second (first bindings))))
(psi (rewrite-biconds (second (second bindings)))))
(list 'and (list 'or (list 'not phi) psi)
(list 'or (list 'not psi) phi))))
((eq 'not (car clause))
(list (car clause) (rewrite-biconds (second clause))))
(t (list (car clause)
(rewrite-biconds (second clause))
(rewrite-biconds (third clause)))))))))
;(rewrite-biconds '(bicond x y))
;result = (AND (OR (NOT X) Y) (OR (NOT Y) X))
;;;
;;; Step 3
;;;
;;; rewrite-ands
;;;
;;; Rewrites (not (and p q)) as (or (not p) (not q))
;;;
(defun rewrite-ands (clause)
(cond
((atom clause) clause)
((= 1 (length clause)) clause)
(t (let ((bindings (match clause '(not (and (? x) (? y))))))
(cond ((not (null bindings))
(let ((phi (rewrite-ands (second (first bindings))))
(psi (rewrite-ands (second (second bindings)))))
(list 'or (list 'not phi)
(list 'not psi))))
((eq 'not (car clause))
(list (car clause) (rewrite-ands (second clause))))
(t (list (car clause)
(rewrite-ands (second clause))
(rewrite-ands (third clause)))))))))
;(rewrite-ands '(not (and x y)))
;result = (OR (NOT X) (NOT Y))
;;;
;;; rewrite-ors
;;;
;;; Rewrites (not (or p q)) as (and (not p) (not q))
;;;
(defun rewrite-ors (clause)
(cond
((atom clause) clause)
((= 1 (length clause)) clause)
(t (let ((bindings (match clause '(not (or (? x) (? y))))))
(cond ((not (null bindings))
(let ((phi (rewrite-ors (second (first bindings))))
(psi (rewrite-ors (second (second bindings)))))
(list 'and (list 'not phi)
(list 'not psi))))
((eq 'not (car clause))
(list (car clause) (rewrite-ors (second clause))))
(t (list (car clause)
(rewrite-ors (second clause))
(rewrite-ors (third clause)))))))))
;(rewrite-ors '(not (or x y)))
;result = (AND (NOT X) (NOT Y))
;;;
;;; rewrite-nots
;;;
;;; Rewrites (not (not p)) as p
;;;
(defun rewrite-nots (clause)
(cond
((atom clause) clause)
((= 1 (length clause)) clause)
(t (let ((bindings (match clause '(not (not (? x))))))
(cond ((not (null bindings))
(let ((phi (rewrite-nots (second (first bindings)))))
phi))
((eq 'not (car clause))
(list (car clause) (rewrite-nots (second clause))))
(t (list (car clause)
(rewrite-nots (second clause))
(rewrite-nots (third clause)))))))))
;(rewrite-nots '(not (not x)))
;result = X
;;;
;;; Step 4a
;;;
;;; rewrite-disjcts1
;;;
;;; Rewrites (or x (and y z)) as (and (or x y) (or x z))
;;;
(defun rewrite-disjcts1 (clause)
(cond
((atom clause) clause)
((= 1 (length clause)) clause)
(t (let ((bindings (match clause '(or (? x) (and (? y) (? z))))))
(cond ((not (null bindings))
(let ((x (rewrite-disjcts1 (second (first bindings))))
(y (rewrite-disjcts1 (second (second bindings))))
(z (rewrite-disjcts1 (second (third bindings)))))
(list 'and (list 'or x y)
(list 'or x z))))
((eq 'not (car clause))
(list (car clause) (rewrite-disjcts1 (second clause))))
(t (list (car clause)
(rewrite-disjcts1 (second clause))
(rewrite-disjcts1 (third clause)))))))))
; (rewrite-disjcts1 '(or x (and y z)))
;result = (AND (OR X Y) (OR X Z))
;;;
;;; Step 4b
;;;
;;; rewrite-disjcts2
;;;
;;; Rewrites (or (and x y) z) as (and (or x z) (or y z))
;;;
(defun rewrite-disjcts2 (clause)
(cond
((atom clause) clause)
((= 1 (length clause)) clause)
(t (let ((bindings (match clause '(or (and (? x) (? y)) (? z)))))
(cond ((not (null bindings))
(let ((x (rewrite-disjcts2 (second (first bindings))))
(y (rewrite-disjcts2 (second (second bindings))))
(z (rewrite-disjcts2 (second (third bindings)))))
(list 'and (list 'or x z)
(list 'or y z))))
((eq 'not (car clause))
(list (car clause) (rewrite-disjcts2 (second clause))))
(t (list (car clause)
(rewrite-disjcts2 (second clause))
(rewrite-disjcts2 (third clause)))))))))
; (rewrite-disjcts2 '(or (and x y) z))
; result = (AND (OR X Z) (OR Y Z))
;;;
;;; Step 5
;;;
;;; rewrite-andors
;;;
;;; Rewrites (and x y) as (x y)
;;; and rewrites (or x y) as (x y)
;;;
(defun rewrite-andors (clause)
(cond
((atom clause) clause)
((= 1 (length clause)) clause)
(t (let ((bindings (or (match clause '(and (? x) (? y)))
(match clause '(or (? x) (? y))))))
(cond ((not (null bindings))
(let ((x (rewrite-andors (second (first bindings))))
(y (rewrite-andors (second (second bindings)))))
(list x y)))
((eq 'not (car clause))
(list (car clause) (rewrite-andors (second clause))))
(t (list (car clause)
(rewrite-andors (second clause))
(rewrite-andors (third clause)))))))))
; (rewrite-andors '(and (or x y) (or x z)))
; result = ((Y X) (Y Z))
; (rewrite-andors '(not (and (or x y) (or x z))))
; result (NOT ((Y X) (Y Z)))
; (rewrite-andors '(and (or (not x) (not y)) (or (not x) (not z))))
; result = (((NOT Y) (NOT X)) ((NOT Y) (NOT Z)))
;(rewrite-andors '(and (or (and x p) (and y q)) (or (and x p) (and z r))))
;result = (((AND Y Q) (AND X P)) ((AND Y Q) (AND Z R)))
(defun rewrite-clause-aux (clause)
(cond ((null clause) nil)
((atom clause) clause)
(t(progn
(setq step1 (rewrite-conds clause))
(setq step2 (rewrite-biconds step1))
(setq old-clause step2)
(setq new-clause nil)
(setq exit-loop-t 'f)
(loop
(setq step3a (rewrite-nots old-clause))
(setq step3b (rewrite-ands step3a))
(setq step3c (rewrite-ors step3b))
(setq new-clause step3c)
(if (equal old-clause new-clause)
(setq exit-loop-t 't)
(setq old-clause new-clause)
)
(when (equal 't exit-loop-t) (return))
)
(setq old-clause step3c)
(setq new-clause nil)
(setq exit-loop-t 'f)
(loop
(setq step4a (rewrite-disjcts1 old-clause))
(setq step4b (rewrite-disjcts2 step4a))
(setq step4c (rewrite-nots step4b))
(setq new-clause step4c)
(if (equal old-clause new-clause)
(setq exit-loop-t 't)
(setq old-clause new-clause)
)
(when (equal 't exit-loop-t) (return))
)
(setq step5 (rewrite-andors step4c))
)
)))
; (rewrite-clause-aux '(cond q r))
; (rewrite-clause-aux '(cond (not (and brd (not w))) hf))
; (rewrite-clause-aux '(not (and brd (not w))))
; (rewrite-clause-aux '(and brd (not w)))
; (rewrite-clause-aux '(or (not (and brd (not w))) p))
; (rewrite-clause-aux '(cond (not (not (and p q))) r))
; (rewrite-clause-aux '(cond (not (and p q)) r))
; (rewrite-clause-aux '(cond (cond p q) r))
; (rewrite-clause-aux '(cond (not p) (not (not q))))
; (rewrite-clause-aux '(bicond (not (and p q)) r))
; (rewrite-clause-aux '(bicond (not (and p q)) (not r)))
; (rewrite-clause-aux '(bicond (not (and p q)) (not (and r s))))
; (rewrite-clause-aux '(bicond (and p q) (and r s)))
; (rewrite-clause-aux '(bicond (and p q) (not (and r s))))
(defun rewrite-clauses (clauses)
(cond ((null clauses) nil)
((atom clauses) clauses)
(t(cons (rewrite-clause-aux (car clauses))
(rewrite-clauses (cdr clauses))))))
; (rewrite-clauses '((cond p q) (cond q r) ((not r)) (p)))
; result = (((NOT P) Q) ((NOT Q) R) ((NOT R)) (P))
;;;; Number 2
;;;; Write a set of Lisp functions that implements a resolution theorem prover.
;;;; Given a set of clauses in conjunctive normal 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)
(defun return-p-from-notp (clause)
(cond
((atom clause) nil)
((= 1 (length clause)) nil)
(t (let ((bindings (match clause '(not (? x)))))
(cond ((not (null bindings))
(let ((x (second (first bindings))))
(list x))))))))
(defun return-p-from-notq-p (clause)
(cond
((atom clause) nil)
((= 1 (length clause)) nil)
(t (let ((bindings (match clause '((not (? x)) (? y)))))
(cond ((not (null bindings))
(let ((y (second (second bindings))))
(list y))))))))
(defun return-p-from-p-notq (clause)
(cond
((atom clause) nil)
((= 1 (length clause)) nil)
(t (let ((bindings (match clause '((? x) (not (? y))))))
(cond ((not (null bindings))
(let ((x (second (first bindings))))
(list x))))))))
(defun return-notq-from-notq-p (clause)
(cond
((atom clause) nil)
((= 1 (length clause)) nil)
(t (let ((bindings (match clause '((not (? x)) (? y)))))
(cond ((not (null bindings))
(let ((x (second (first bindings))))
(list 'not x))))))))
(defun return-notq-from-p-notq (clause)
(cond
((atom clause) nil)
((= 1 (length clause)) nil)
(t (let ((bindings (match clause '((? x) (not (? y))))))
(cond ((not (null bindings))
(let ((y (second (second bindings))))
(list 'not y))))))))
; (return-p-from-notp '(not p))
; (return-p-from-notp '(p))
; (return-p-from-notq-p '((not q) p))
; (return-p-from-notq-p '(p))
; (return-p-from-p-notq '(p (not q)))
; (return-p-from-p-notq '(p))
; (return-notq-from-notq-p '((not q) p))
; (return-notq-from-notq-p '(p))
; (return-notq-from-p-notq '(p (not q)))
; (return-notq-from-p-notq '(p))
(defun find-clause (target sentence)
(cond ((null target) nil)
((null sentence) nil)
((atom sentence) nil)
((null (car sentence)) nil)
((and (equal 'not (first sentence))
(equal target (second sentence))) nil)
((equal target (car sentence)) t)
(t(or (find-clause target (car sentence))
(find-clause target (cdr sentence))))))
; (find-clause 'q '(q))
; (find-clause 'q '((o) (not q)))
; (find-clause 'q '((o)((not p) q)))
; (find-clause 'q '((not (not q)))) ; don't work
; (find-clause 'q '((o)(q (not p))))
; (find-clause '(not q) '((not q)))
; (find-clause '(not q) '((o) (not (not q))))
; (find-clause '(not q) '((o) ((not p) (not q))))
; (find-clause '(not q) '((o) ((not q) (not p))))
; (find-clause 'q '(((not p) q)))
; (find-clause 'q '(((not q) p)))
; (find-clause '(not q) '(((not p) (not q))))
; (find-clause '(not q) '(((not (not q)) p)))
(defun find-not-clause (target sentence)
(cond ((null target) nil)
((null sentence) nil)
((atom sentence) nil)
((null (car sentence)) nil)
((equal target (car sentence)) nil)
((and (equal 'not (first sentence))
(equal target (second sentence))) t)
(t(or (find-not-clause target (car sentence))
(find-not-clause target (cdr sentence))))))
; (find-not-clause 'q '(q))
; (find-not-clause 'q '((o) (not q)))
; (find-not-clause 'q '((o)((not p) (not q))))
; (find-not-clause 'q '((not (not q)))) ;don't work
; (find-not-clause 'q '(((not (not (not q)))))) ;shouldn't work
; (find-not-clause 'q '((o)(p (not q))))
; (find-not-clause 'q '((o)(q (not p))))
; (find-not-clause '(not q) '((not q)))
; (find-not-clause '(not q) '((o) (not (not q)))) ;don't work
; (find-not-clause '(not q) '((o) ((not p) (not (not q))))) ;don't work
; (find-not-clause '(not q) '(((not (not q)) p))) ;don't work
(defun test-clause (clause sentence)
(cond ((null clause) nil)
((atom clause) (find-not-clause clause sentence))
((null (second clause)) (find-not-clause (car clause) sentence))
((eq (first clause) 'not)
(or (find-clause (second clause) sentence)
(find-clause (list (second (second clause))
(first (second clause))
)
sentence)
)
)
(t(or (find-not-clause clause sentence)
(find-not-clause (list (second clause)(first clause))
sentence))
)))
; (test-clause 'q '((not q)))
; (test-clause 'q '((q)))
; (test-clause '(q) '((not q)))
; (test-clause '(q) '((q)))
; (test-clause '(not q) '((not q)))
; (test-clause '(not q) '((q)))
; (test-clause '(not q) '((not (not q)))) ;don't work
; (test-clause 'q '((not (not q)))) ;don't work
; (test-clause 'q '((not p) q))
; (test-clause 'q '(p (not q)))
; (test-clause '(not q) '((not p) q))
; (test-clause '(not q) '(p (not q)))
; (test-clause '(q r) '((not (q r))))
; (test-clause '(q r) '((q r)))
; (test-clause '(q r) '((not (r q))))
; (test-clause '(q r) '((r q)))
; (test-clause '(not (q r)) '((not (q r))))
; (test-clause '(not (q r)) '((q r)))
; (test-clause '(not (q r)) '((not (r q))))
; (test-clause '(not (q r)) '((r q)))
(defun process-clause (target sentence)
(cond ((null target) nil)
((null sentence) nil)
((atom sentence) nil)
((atom target) nil)
((null (car target)) nil)
((return-p-from-notp target)
(test-clause target sentence))
((return-p-from-notq-p target)
(and (test-clause (return-p-from-notq-p target) sentence)
(test-clause (return-notq-from-notq-p target) sentence)))
((return-p-from-p-notq target)
(and (test-clause (return-p-from-p-notq target) sentence)
(test-clause (return-notq-from-p-notq target) sentence)))
(t(test-clause (car target) sentence))
))
; (setq sentence '((a) (not a) ((not b) c) (b (not c))))
; (process-clause '(a) sentence)
; (process-clause '(not a) sentence)
; (process-clause '((not b) c) sentence)
; (process-clause '(b (not c)) sentence)
; (setq sentence '((a) (not a) ((not b) c)(o) (b (not c))))
; (process-clause '(o) sentence)
; (setq sentence '((a) (not a) ((not b) c)(not o) (b (not c))))
; (process-clause '(not o) sentence)
; (setq sentence '((a) (not a) ((not b) c)((not o) x) (b (not c))))
; (process-clause '((not o) x) sentence)
; (setq sentence '((a) (not a) ((not b) c)(x (not o)) (b (not c))))
; (process-clause '(x (not o)) sentence)
; (setq sentence '((a) (not a) ((not b) c)(x (not o)) (not x) (b (not c))))
; (process-clause '(x (not o)) sentence)
; (process-clause '(not x) sentence)
(defun process-clauses (target sentence)
(cond ((null target) nil)
((null sentence) nil)
((atom sentence) nil)
((atom target) nil)
((null (car target)) nil)
((null (cdr target)) (process-clause (car target) sentence))
((process-clause (car target) sentence)
(process-clauses (cdr target) sentence))))
; (process-clauses '((a)(not a)(b)(not b)) '((a)(not a)(b)(not b)))
; (process-clauses '((a (not b))(b (not a))) '((a (not b))(b (not a))))
; (process-clauses '((a (not b))(not a) (b)) '((a (not b))(not a) (b)))
; (process-clauses '((a)(not a)(b)(o)(not b)) '((a)(not a)(b)(o)(not b)))
; (process-clauses '((a (not b))(not o)(b (not a)))
; '((a (not b))(not o)(b (not a))))
; (process-clauses '((a (not b))((not a) o) (b))
; '((a (not b))((not a) o)(b)))
; (process-clauses '((a (not b))((not a) o)(not o) (b))
; '((a (not b))((not a) o)(not o) (b)))
(defun prove (sentence)
(cond ((null sentence) nil)
((atom sentence) nil)
(t (process-clauses sentence sentence))))
; (prove '(((NOT P) Q) ((NOT Q) R) ((NOT R)) (P)))
;;;;
;;;; Number 3 - Use the following two functions to test your code.
;;;; They are for the two propositional logic problems presented in lecture.
;;;;
(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)))
; (example1)
(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)))
; (example2)
