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