burke@pollux.usc.edu (Sean Burke) (11/26/89)
A while back someone posted looking for logic programming stuff in LISP. I have some Common Lisp code which does resolution theorem-proving in first-order predicate logic. Not only that, it comes with _extensive_ documentation! That's because the program is based on the example given in Appendix A of "Symbolic Logic and Mechanical Theorem Proving", by Chin-Liang Chang and Richard Lee, (Academic Press 1973), one of the best references on the subject. I have converted the original PDP-10 LISP 1.6 into Common Lisp, pretty much faithfully (in fact, too faithfully). Chang and Lee gives theory and and a bunch of test problems. The code occupies 22K, and runs real snappy on my 2Mbyte Mac+ under MACL 1.2.1. This is not to say that it could not run much snappier, of course. You should check out Chang and Lee just to chuckle at LISP coding style circa 1973. Sadly, much of this funkiness is retained in my transposition. Sean "The nice thing about true hopelessness is that you don't have to try again" - Jules Shear