A Prolog technology theorem prover: A new exposition and implementation in Prolog (Q1199932)

A Prolog technology theorem prover (PTTP) [\textit{M. E. Stickel}, J. Autom. Reasoning 4, No. 4, 353-380 (1988; Zbl 0662.68104)] is an extension of Prolog that is complete for the full first-order predicate calculus. This is achieved through 3 strategic changes: \(\bullet\) A unification algorithm is used with the occur check, \(\bullet\) unbounded depth-first search is replaced by depth-first iterative deepening search, and \(\bullet\) the model elimination reduction rule is added to Prolog inferences. The paper offers a concise and readable description of the PTTP implementation in Prolog. The performance of the resulting logic program is approaching that of Lisp PTTP implementations. Special attention is given to suggestions of possible extensions to Prolog that would enable a higher performance of PTTP logic programs.