A Prolog Technology Theorem Prover: Implementation By An Extended, Prolog Compiler
by Stickel, Mark E.
Technical Note 382
Institution: AI Center, SRI International
Address: 333 Ravenswood Ave., Menlo Park, CA 94025
Note: Originally published April 1986. Revised November 1987.
A Prolog technology theorem prover (PTTP) is an extension of Prolog that is complete for the full first-order predicate calculus. It differs from Prolog in its use of unification with the occurs check for soundness, the model-elimination reduction rule that is added to Prolog inferences to make the inference system complete, and depth-first iterative-deepening search instead of unbounded depth-first search to make the search strategy complete. A Prolog technology theorem prover has been implemented by an extended Prolog-to-LISP compiler that supports these additional features. It is capable of proving theorems in the full first-order predicate calculus at a rate of thousands of inferences per second.
|Stickel, Mark E||Principal Scientist|