A Prolog technology theorem prover: Implementation by an extended Prolog compiler (Q1114446)

The author exposes interesting ideas and experiments concerning a Prolog technology theorem prover (PTTP). The goal and the author's option are to ``establish a new standard of performance for theorem proving programs''. The PTTP implementation is an extended Prolog-to-Lisp compiler, written in Common Lisp for Symbolics 3600 LISP machine. In order to obtain a complete theorem prover there are examined the extensions of the classical Prolog features towards: (1) a sound (occurs check) unification; (2) a complete inference system, by adding the reduction rule to the model elimination procedure; (3) a complete search strategy, extending the unbounded depth-first search to the depth-first iterative- deepening search (which, among the advantages, can be naturally parallelized). Current and forthcoming PTTP refinements are discussed. The behaviour of the PTTP compiler when running some concrete examples is exposed. The (very promising) performances of PTTP on a set of 95 problems are presented in detail on a two pages tableau (containing the number of clauses, depth of proof, number of inferences, run time). Important similar approaches are compared and referred. The paper represents a guiding report on outstanding work and results.