;;;
;;; Solution for A3 question #1
;;;
;;; Philip W. L. Fong
;;;
;;
;; Skolemize
;;
(defun skolemize (wff)
"Skolemize formula WFF."
(skolemize-aux wff nil))
(defun skolemize-aux (wff var-list)
"Skolemize formula WFF, assuming that the variables in the list
VAR-LIST are implicitly quantified universally."
(cond
((universal-p wff)
(make-universal (universal-var wff)
(skolemize-aux (universal-wff wff)
(cons (universal-var wff) var-list))))
((existential-p wff)
(skolemize-aux (wff-substitute (existential-wff wff)
(existential-var wff)
(generate-skolem-function var-list))
var-list))
(t wff)))
;;
;; Preprocess
;;
(defun preprocess (wff &optional (debug t))
"Preprocess formula WFF. Set the optional argument DEBUG to NIL for
silent mode."
(if debug
(format t "Preprocess Formula:~%~S~%" wff))
(setf wff (eliminate-implications wff))
(if debug
(format t "Eliminate Implications:~%~S~%" wff))
(setf wff (move-negations-inwards wff))
(if debug
(format t "Move Negations Inwards:~%~S~%" wff))
(setf wff (standardize-variables wff))
(if debug
(format t "Standardize Variables:~%~S~%" wff))
(setf wff (move-quantifiers-left wff))
(if debug
(format t "Move Quantifiers Left:~%~S~%" wff))
(setf wff (skolemize wff))
(if debug
(format t "Skolemize:~%~S~%" wff))
(setf wff (distribute-disj-over-conj wff))
(if debug
(format t "Distribute Disjunction Over Conjunction:~%~S~%" wff))
(setf wff (clausal-form wff))
(if debug
(format t "Convert to Clausal Form:~%~S~%" wff))
wff)