PTTP - Prolog Technology Theorem Prover (original) (raw)

Overview

Despite Prolog's logic heritage and its use of theorem-proving unification and resolution operations, Prolog fails to qualify as a full general-purpose theorem-proving system. There are three main reasons: (1) many Prolog systems use an unsound unification algorithm, (2) Prolog's unbounded depth-first search strategy is incomplete, and (3) Prolog's inference system is not complete for non-Horn clauses. Nevertheless, Prolog is quite interesting from a theorem-proving standpoint because of its very high inference rate as compared to conventional theorem-proving programs. The objective of the Prolog Technology Theorem Prover (PTTP) is to overcome the deficiencies while retaining as fully as possible the high performance of well-engineered Prolog systems. PTTP is an implementation of the model elimination theorem-proving procedure that extends Prolog to the full first-order predicate calculus. PTTP differs from Prolog in its use of (1) unification with the occurs check for soundness, (2) depth-first iterative deepening search instead of unbounded depth-first search to make the search strategy complete, and (3) the model elimination inference rule that is added to Prolog inferences to make the inference system complete. PTTP also extends Prolog by providing the capability of printing the proofs it finds. Because PTTP compiles the clauses of a problem, its inference rate is very high. Because PTTP uses depth-first search, its storage requirements are low and term size need not be limited to reduce memory usage at the expense of completeness. PTTP's simple architecture facilitates its adaptation and use in applications. Two versions of PTTP are available: one is written in Common Lisp and compiles clauses into Common Lisp; the other is written in Prolog and compiles clauses into Prolog. The Lisp version is faster than the Prolog version, but the Prolog version is easier to read and modify. The Lisp version can print the proofs it finds only if Symbolics Common Lisp is used. Caveat: PTTP's high inference rate is achieved at the cost of not allowing more flexible search strategies or elimination of redundancy in the search space by subsumption. Although PTTP is one of the fastest theorem provers available when evaluated by its inference rate and performance on easy problems and it has been used to solve reasoning problems in planning and natural-language-understanding systems effectively, its high inference rate can be overwhelmed by its exponential search space and it is unsuitable for many difficult theorems. The Ottertheorem prover developed at Argonne National Laboratory has been quite successful at proving difficult theorems that are intractable for PTTP. Subsumption, demodulation, and weighting, all incompatible with PTTP, are crucial contributors to Otter's performance on difficult theorems. PTTP was used in Stanford'sLogic-Based Subsumption Architectureproject.

Selected Publications

Downloads

Mark E. Stickel (stickel_a_t_ai.sri.com)

2006-10-04