plaisted@unc.UUCP (David Plaisted) (11/04/86)
I have recently programmed a theorem prover in C Prolog that Prolog programmers may find useful. This prover may be viewed as an extension of Prolog to full first order logic, that is, non-Horn clauses. Negation is treated as in first-order logic, not as in negation by failure. The input syntax is much the same as the syntax of Prolog. The prover uses Prolog style depth-first search with a gradually increasing depth bound (this is therefore depth-first iterative deepening). Also, solutions to subgoals are "cached" so that if a subgoal is seen more than once, work is not repeated. The prover has a convenient interface to Prolog source code for predicates whose solutions may be found more efficiently in Prolog itself than by the theorem prover. This also permits interaction with the user to obtain the values of variables, for example. The prover is capable of general term rewriting to replace subexpressions by equivalent ones. This prover has been run on a wide variety of problems and generally obtains simple proofs in 10 or 20 seconds in C Prolog on a VAX 780. The listing is about 15 pages long. This makes the prover relatively easy to understand, so it may be possible to adapt it to various applications by direct modification of the source code. The prover has been designed for use with as little user guidance as possible, for users who know nothing about theorem proving. It is based on a modification of the theorem proving strategy described in Plaisted, D., A simplified problem reduction format, Artificial Intelligence 18 (1982) 227-261, and has been distributed to several sites. If you are interested, send e-mail to plaisted@unc on the csnet and I will e-mail you the entire source code, together with a file of examples that have been run on it. The source code contains information about how to use the prover. This prover is similar to Stickel's prolog technology theorem prover, but does not use contrapositives of clauses as his does. Also, it is much slower than his, but does not require the axioms to be compiled. Of course, using a compiled Prolog would speed up my prover by a large factor. Don Loveland of Duke has recently developed an extension of Prolog which is intended for "near-Horn" clauses and which may also be of interest to readers of this newsgroup. David Plaisted University of North Carolina at Chapel Hill