;;; PROVER.CL
;;; A verifier for propositions using Wang's algorithm.
;;; (C) Copyright 1995 by Steven L. Tanimoto.
;;; This program is described in Chapter 6 ("Logical Reasoning") of
;;; "The Elements of Artificial Intelligence Using Common Lisp," 2nd ed.,
;;; published by W. H. Freeman, 41 Madison Ave., New York, NY 10010.
;;; Permission is granted for noncommercial use and modification of
;;; this program, provided that this copyright notice is retained
;;; and followed by a notice of any modifications made to the program.
;;; PROVER is the interactive top-level shell.
(defun prover ()
"Top-level loop for a propositional validator using Wang's algorithm."
(let (s)
(loop
(format t "~%Please enter proposition or HELP or RETURN.~%")
(setf s (read))
(cond ((eql s 'help)
(format t "Here's an example: ")
(format t "((a and (not b)) implies a) ~%") )
((eql s 'return) (return))
((setf s (catch 'syntax-error (reformat s)))
(if (valid nil (list s))
(format t " is valid. ~%")
(format t " is NOT valid. ~%") ) )
(t (format t ": Syntax error ~%"))
) ) ) )
;;; VALID is the main recursive workhorse that verifies
;;; the propositional logic "theorems" with Wang's rules.
;;; Pattern-matching results are passed back as and stored
;;; locally as the value of B -- the "bindings".
;;; Arguments L and R are the left and right sides of a sequent.
(defun valid (l r)
"Returns T if the conjunction of the formulas in L implies
any of the formulas in R."
(let (b)
(cond
; Test for axiom:
((intersection l r) t)
; NOT on the left:
((setf b (match '((* x) (not-wff y) (* z)) l))
(valid (append (val 'x b) (val 'z b))
(append r (rest (val 'y b))) ) )
; NOT on the right:
((setf b (match '((* x) (not-wff y) (* z)) r))
(valid (append l (rest (val 'y b)))
(append (val 'x b) (val 'z b)) ) )
; OR on the right:
((setf b (match '((* x) (or-wff y) (* z)) r))
(valid l
(append (val 'x b)
(list (first (val 'y b)))
(rest (rest (val 'y b)))
(val 'z b) ) ) )
; AND on the left:
((setf b (match '((* x) (and-wff y) (* z)) l))
(valid (append (val 'x b)
(list (first (val 'y b)))
(rest (rest (val 'y b)))
(val 'z b) )
r) )
; OR on the left:
((setf b (match '((* x) (or-wff y) (* z)) l))
(and (valid (append (val 'x b)
(list (first (val 'y b)))
(val 'z b) )
r)
(valid (append (val 'x b)
(rest (rest (val 'y b)))
(val 'z b) )
r) ) )
; AND on the right:
((setf b (match '((* x) (and-wff y) (* z)) r))
(and (valid l
(append (val 'x b)
(list (first (val 'y b)))
(val 'z b) ) )
(valid l
(append (val 'x b)
(rest (rest (val 'y b)))
(val 'z b) ) ) ) ) ) ) )
(defun or-wff (x)
"Returns T if X if of the form (f1 OR f2)."
(cond ((atom x) nil)
(t (eql (second x) 'or)) ) )
(defun and-wff (x)
"Returns T if X is of the form (f1 AND f2)."
(cond ((atom x) nil)
(t (eql (second x) 'and)) ) )
(defun not-wff (x)
"Returns T if X is of the form (NOT f)."
(cond ((atom x) nil)
(t (eql (first x) 'not)) ) )
(defun wff (x)
"Returns T if X is a well-formed formula."
(cond ((atom x) t)
((match '(not (wff dum)) x) t)
((match '((wff dum) (op dum) (wff dum)) x) t)
(t nil) ) )
(defun op (x)
"Returns T if X is a recognized logical operator."
(member x '(and or implies)) )
;;; REFORMAT checks syntax and eliminates IMPLIES.
(defun reformat (x)
"Either returns the formula X with all occurrences
of IMPLIES eliminated, or performs a THROW with the
indication of a syntax-error."
(cond ((atom x) x)
((null (wff x)) (throw 'syntax-error nil))
((not-wff x) (list 'not (reformat (second x))))
((equal (second x) 'implies)
(list (list 'not (reformat (first x)))
'or
(reformat (third x)) ) )
(t (list (reformat (first x))
(second x)
(reformat (third x)) )) ) )
;;; The following code is from MATCH2.CL
(defun match (p s)
"Attempts to find a correspondence between P and S, utilizing
any special constructs appearing in P. Return an association
list of bindings if successful; NIL otherwise."
(cond
((handle-both-null p s))
((handle-normal-recursion p s))
((atom (first p)) nil)
((handle-? p s))
((handle-* p s))
((handle-restrict-pred p s))
(t nil) ) )
(defun handle-both-null (p s)
"Test for and handle case when both P and S are null."
(if (and (null p)(null s))
'((yes . yes)) ) )
(defun handle-normal-recursion (p s)
"Test for and handle case when the first elements of
P and S are EQL."
(if (atom (first p))
(if (eql (first p)(first s))
(match (rest p)(rest s)) ) ) )
(defun handle-? (p s)
"Test for and handle the case when (FIRST P) is of
the form (? X)."
(if s ; S must not be null
(if (eql (first (first p)) '?)
(let ((rest-match (match (rest p)(rest s))))
(if rest-match
(acons (first (rest (first p)))
(first s)
rest-match) ) ) ) ) )
(defun handle-* (p s)
"Test for and handle the case when (FIRST P) is of
the form (* X)."
(if (eql (first (first p)) '*)
(let ((pattern-variable (first (rest (first p))))
rest-match)
(cond ; subcase 1 --match one element of S:
((and s
(setf rest-match
(match (rest p)(rest s)) ) )
(acons pattern-variable
(list (first s))
rest-match) )
; subcase 2 --match no elements of S:
((setf rest-match (match (rest p) s))
(acons pattern-variable nil rest-match) )
; subcase 3 --match more than one element of S:
((and s
(setf rest-match
(match p (rest s)) ) )
(acons pattern-variable
(cons (first s)
(val pattern-variable
rest-match) )
(rest rest-match)) )
(t nil) ) ) ) )
(defun handle-restrict-pred (p s)
"Handle case when (FIRST P) is of the form (PREDICATE X)."
(if s ; S must not be null
(if (member (first (first p)) '(? *)) ; Don't apply '? or '*.
nil
(if (apply (caar p) (list (first s)))
(let ((rest-match (match (rest p) (rest s)))
(pattern-variable (first (rest (first p)))) )
(if rest-match
(acons pattern-variable
(first s)
rest-match) ) ) ) ) ) )
;;; The function VAL provides convenient access to
;;; something matched by a variable after matching with MATCH.
(defun val (variable alist)
"Returns the value associated with VARIABLE on ALIST."
(rest (assoc variable alist)) )
;;; end of code from MATCH2.CL
;;; Now invoke the program and provide test data...
(prover)
;(a or (not a))
;((a or (not a)) and (b or (not b)))
on-cutoff)
#+dtp-trace (declare (type integer subgoal-cutoff function-cutoff))
(if (and (= *last-sc* subgoal-cutoff)
(= *last-fc* function-cutoff) )
(return-from within-maxbounds-p nil)
(progn
(setq *last-sc* subgoal-cutoff)
(setq *last-fc* function-cutoff) ))
(or
(and (proof-subgoal-maximum-depth *proof*)
(<= subgoal-cutoff (proof-subgoal-maximum-depth *proof*)) )
(and (proof-function-maximum-depth *proof*)
(<= function-cutoff (proof-function-maximum-depth *proof*)) )
(and (null (proof-subgoal-maximum-depth *proof*))
(null (proof-function-maximum-depth *proof*)) )))
#+dtp-trace
(defun report-iteration (subgoal-bound function-bound)
(when (find :iteration *trace*)
(when (or *use-subgoal-cutoffs* *use-function-cutoffs*)
(format *debug-io* "~2&") )
(when *use-subgoal-cutoffs*
(format *debug-io* "Subgoal depth cutoff = ~D~%" subgoal-bound) )
(when *use-function-cutoffs*
(format *debug-io* "Function depth cutoff = ~D~%" function-bound) )))
;;;----------------------------------------------------------------------------
(defmethod reset ((proof proof) #+dtp-trace &key #+dtp-trace &allow-other-keys)
(setf (proof-query-conjunctions proof)
(mapcar #'list-to-conjunction (dnf (proof-query proof))) )
#+dtp-trace
(loop
for conj in (proof-query-conjunctions proof)
for count from 0
do (setf (slot-value conj 'order) count)
finally (setf (proof-conjunction-count proof) count) )
(when *use-negated-goal*
(let ((*goal-node-id-count* 0))
(setf (proof-goal-nodes proof)
(mapcar #'make-goal-node (proof-query-conjunctions proof)) )))
(setf (proof-blocked-conjunctions proof) nil)
(setf (proof-subgoal-index proof) (make-hash-table :test #'eq))
(setf (proof-subgoal-cutoff-occurred proof) nil)
(setf (proof-function-cutoff-occurred proof) nil)
#+dtp-trace (setf (proof-used-conjunctions proof) nil) )
;;;----------------------------------------------------------------------------
(defun prove-next-answer-internal ()
"Return or :NOT-AN-ANSWER"
#+dtp-trace
(when (find :solutions *trace*)
(format *debug-io* "Looking for next answer of ~A~%"
(proof-query *proof*) ))
(loop
for next-answer = (pop (proof-new-answers *proof*))
for next-subgoal = (agenda-best)
for next-conjunction = (first (proof-query-conjunctions *proof*))
while (or next-answer next-subgoal next-conjunction
(and *use-unblocking* (forkable-conjunctions?)) )
do
(when *timeout-maximum-seconds*
(incf *timeout-count*)
(when (> *timeout-count* *timeout-resolution*)
(setq *timeout-count* 0)
(let ((rt (get-internal-run-time)))
(when (> rt *timeout-end*)
(return :not-an-answer) )
#+dtp-trace
(when (find :timeout *trace*)
(let (secs)
(setq secs
(floor (- *timeout-end* rt)
internal-time-units-per-second ))
(if (find :proofs *trace*)
(format *debug-io* "~D seconds until timeout~%" secs)
(format *debug-io* "[~D]..." secs) )))
)))
(cond
(next-answer
(let ((valid (process-answer next-answer)))
(when valid (return valid)) ))
(next-subgoal
(process-subgoal next-subgoal) )
((and *use-unblocking* (forkable-conjunctions?))
(unblock-agenda) )
(t
(process-conjunction next-conjunction) ))
finally (return :not-an-answer) ))
;;;----------------------------------------------------------------------------
(defun process-answer (answer)
#+dtp-types (declare (type answer answer))
#+dtp-trace
(when (and (proof-sda *proof*)
(disjunctive-p answer)
(find :solutions *trace*) )
(format *debug-io* "Suppressing disjunctive answer ~A~%" answer) )
(unless (and (proof-sda *proof*) (disjunctive-p answer))
(add-to-end answer (proof-answers *proof*))
answer ))
;;;----------------------------------------------------------------------------
(defun process-subgoal (subgoal)
#+dtp-types (declare (type dtp-subgoal subgoal))
(cond
((null (slot-value subgoal 'conjuncts-to-propagate-to))
#+dtp-trace
(when (find :proofs *trace*)
(format *debug-io* "Subgoal ")
(print-literal-node (slot-value subgoal 'literal) :s *debug-io*)
(format *debug-io* " is irrelevant~%") )
(agenda-remove subgoal) )
((exhausted-p subgoal :ignore-blocked t)
#+dtp-trace
(when (find :proofs *trace*)
(format *debug-io* "Subgoal ")
(print-literal-node (slot-value subgoal 'literal) :s *debug-io*)
(format *debug-io* " is exhausted~%") )
(when (exhausted-p subgoal)
#+dtp-trace (incf *depth*)
(terminate subgoal)
#+dtp-trace (decf *depth*) )
(agenda-remove subgoal) )
(t
(expand subgoal) )))
;;;----------------------------------------------------------------------------
(defun process-conjunction (conjunction)
#+dtp-types (declare (type dtp-conjunction conjunction))
(if (exhausted-p conjunction)
(progn
#-dtp-trace (pop (proof-query-conjunctions *proof*))
#+dtp-trace
(add-to-end
(pop (proof-query-conjunctions *proof*))
(proof-used-conjunctions *proof*) ))
(expand conjunction) ))
;;;----------------------------------------------------------------------------
(defun prove-all-remaining-answers-internal (&optional (*proof* *proof*))
"Return list of all remaining "
(loop
for next-answer = (prove-next-answer-with-iteration *proof*)
until (eq next-answer :not-an-answer)
collect next-answer into answers
#+dtp-trace do
#+dtp-trace
(when (find :solutions *trace*)
(format *debug-io* "Found answer ~A~2%" next-answer) )
finally (return answers) ))
;;;----------------------------------------------------------------------------
(defun explode-answer (answer)
"Returns (1) bound query, (2) label, (3) residue, (4) ANSWER, (5) *PROOF*"
#+dtp-types (declare (type answer answer))
(if (answer-p answer)
(values (apply-answer answer) (extract-label answer)
(extract-residue answer) answer *proof* )
(values nil nil nil :not-an-answer *proof*) ))
;;;----------------------------------------------------------------------------
(defun extract-label (answer)
#+dtp-types (declare (type answer answer))
(let ((label (answer-label answer)))
(when label (label-value label)) ))
;;;----------------------------------------------------------------------------
(defun extract-residue (answer)
#+dtp-types (declare (type answer answer))
(mapcar #'literal-to-list (answer-residue answer)) )
;;;----------------------------------------------------------------------------
(defun make-goal-node (conjunction)
"Return clause corresponding to negated conjunction"
#+dtp-types (declare (type dtp-conjunction conjunction))
(with-slots (list) conjunction
(loop
for conjunct in list
for literal = (slot-value conjunct 'literal)
for new-literal = (copy-literal-node literal)
do (setf (literal-negated-p new-literal)
(not (literal-negated-p new-literal)) )
collect new-literal into literals
finally
(return
(make-kb-node
:id (make-new-id "GOAL" (incf *goal-node-id-count*))
:clause (make-clause-node :literals literals)) ))
))
;;;----------------------------------------------------------------------------