;;;
;;; Solution for A3 question #5
;;;
;;; By Philip W. L. Fong
;;;
(defun prove (gamma alpha strategy)
"Prove that wff ALPHA follows from wff GAMMA using search strategy STRATEGY."
(let ((L-gamma (preprocess gamma))
(L-alpha (preprocess (make-negation alpha))))
(refute (append L-alpha L-gamma) strategy)))