plaisted@unc.cs.unc.edu (David Plaisted) (07/13/87)
Prolog Theorem Prover In response to a recent query, a full first-order logic theorem prover in C Prolog is available from me via e-mail. It is about 35,000 bytes long. This prover was advertised in Prolog Digest volume 4 # 67 (November 1986) and was sent by e-mail to 60 or 70 people, and was placed in Stanford's Prolog library. The prover has been updated since the last distribution and some bugs in a couple of distributed versions have been fixed. If there is sufficient interest I will attempt to have an updated version placed in the Prolog library. Until then contact me by e-mail for Prolog source code, documentation, and examples. This prover uses depth-first iterative deepening with caching of solutions to subgoals, and uses true unification. The equality mechanism is now fairly sophisticated. The prover has been modified by several students and is convenient for research and instructional purposes. It has obtained automatic proofs of many theorems, including theorems in implicational logic, simple set theory, ternary Boolean algebra, Smullyan's book To Mock a Mockingbird (combinatory logic), the intermediate value theorem, two versions of the Monkey and Bananas problem, and puzzles such as those in the newsletter of the Association for Automated Reasoning. A student recently obtained a fairly automated proof that the composition of two homomorphisms is a homomorphism, for example. I have written a preliminary paper describing the implementation techniques used and giving a formal proof of completeness of the strategy. I would be happy to mail this paper to interested persons. Dave Plaisted Department of Computer Science University of North Carolina at Chapel Hill Chapel Hill, NC 27514 plaisted@unc (CSNET) ...!mcnc!unc!plaisted (UUCP) plaisted@cs.unc.edu (ARPA)