```;;;
;;; Wang Algorithm
;;; programmed by Stuart C. Shapiro [shapiro@cs.buffalo.edu]
;;;               July 8, 1994
;;; predicate-wang added August 29, 1995
;;;
;;; Use and redistribution is unlimited
;;; as long as these comments are retained.
;;;
;;;  <logical connectives>:  -  &  or  =>  <=>
;;;  <quantifiers>: all exists
;;;  <variables>: determined by use in quantifier clause
;;;
;;; External functions: (wang TrueWffs FalseWffs)
;;;                     (predicate-wang TrueWffs FalseWffs Terms)
;;;
;;; Syntax of wffs:
;;;
;;; wff ::= atomic-wff |
;;;         (~ wff) |
;;;         (wff & wff)
;;;         (wff or wff)
;;;         (wff => wff)
;;;         (wff <=> wff)
;;;         (all variable wff)
;;;         (exists variable wff)
;;; atomic-wff ::= any Lisp form not of any of the above formats
;;; variable ::= any Lisp symbol not also used for another purpose
;;; term ::= any Lisp symbol
;;;
(defpackage wang

(in-package wang)

(defun unary-operator (wff)
(first wff))

(defun operator (wff)
(second wff))

(defun unary-operand (wff)
(second wff))

(defun first-operand (wff)
(first wff))

(defun second-operand (wff)
(third wff))

(defun quantifier (wff)
(first wff))

(defun variable (wff)
(second wff))

(defun scope (wff)
(third wff))

(defun has-symbol-name (symbol name)
(and (symbolp symbol)
(string-equal (symbol-name symbol) name)))

(defun negation (wff)
(has-symbol-name (unary-operator wff) "~"))

(defun conjunction (wff)
(has-symbol-name (operator wff) "&"))

(defun disjunction (wff)
(has-symbol-name (operator wff) "or"))

(defun implication (wff)
(has-symbol-name (operator wff) "=>"))

(defun biconditional (wff)
(has-symbol-name (operator wff) "<=>"))

(defun u-quantified-wff (wff)
(has-symbol-name (quantifier wff) "all"))

(defun e-quantified-wff (wff)
(has-symbol-name (quantifier wff) "exists"))

(defun unary-opd (wff)
(negation wff))

(defun binary-opd (wff)
(or (conjunction wff) (disjunction wff)
(implication wff) (biconditional wff)))

(defun quantified (wff)
(or (u-quantified-wff wff) (e-quantified-wff wff)))

(defun atomic (wff)
(or (atom wff)
(not (or (unary-opd wff) (binary-opd wff) (quantified wff)))))

(defun predicate-wang (TrueWffs FalseWffs Terms)
"Returns True if no way to make consistent truth value assignments.
Calls wang after expanding all universally quantified wffs into
conjunctions of all ground instances, and expanding all existentially
quantified wffs into disjunctions of all ground instances."
(wang (mapcar #'(lambda (wff) (expand wff Terms)) TrueWffs)
(mapcar #'(lambda (wff) (expand wff Terms)) FalseWffs)))

(defun expand (wff Terms)
"Expands all quantified subformulas of wff into conjunctions or
disjunctions of all ground instances."
(cond ((atom wff) wff)
((unary-opd wff)
(list (unary-operator wff)
(expand (unary-operand wff) Terms)))
((binary-opd wff)
(list (expand (first-operand wff) Terms)
(operator wff)
(expand (second-operand wff) Terms)))
((quantified wff)
(make-ground-wffs (expand (scope wff) Terms)
(variable wff)
Terms
(if (u-quantified-wff wff) '& 'or)))
(t (mapcar #'(lambda (wff) (expand wff Terms)) wff))))

(defun make-ground-wffs (wff variable Terms con-or-dis-junction)
"Returns a conjunction or disjunction, using con-or-dis-junction,
of all ground instances of the open wff."
(let ((result (subst (first Terms) variable wff)))
(dolist (term (rest Terms) result)
(setf result (list (subst term variable wff)
con-or-dis-junction
result)))))

(defun wang (TrueWffs FalseWffs)
"Returns True if no way to make consistent truth value assignments."
(if (intersection TrueWffs FalseWffs :test #'equal) t
(let (wff)
(cond ((setf wff (find-if-not #'atomic TrueWffs))
(cond ((negation wff)
(wang (remove wff TrueWffs)
((conjunction wff)
(remove wff TrueWffs)))
FalseWffs))
((disjunction wff)
(remove wff TrueWffs))
FalseWffs)
(remove wff TrueWffs))
FalseWffs)))
((implication wff)
(remove wff TrueWffs))
FalseWffs)
(wang (remove wff TrueWffs)
((biconditional wff)
(remove wff TrueWffs)))
FalseWffs)
(wang (remove wff TrueWffs)
(remove wff FalseWffs))))))
))
((setf wff (find-if-not #'atomic FalseWffs))
(cond ((negation wff)
(remove wff FalseWffs)))
((conjunction wff)
(and (wang Truewffs (addwff (first-operand wff)
(remove wff Falsewffs)))
(remove wff Falsewffs)))))
((disjunction wff)
(wang TrueWffs
(remove wff FalseWffs)))))
((implication wff)