PTTP - Prolog Technology Theorem Prover
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 Otter
theorem 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.
Selected Publications
- Stickel, M.E.
A Prolog technology theorem prover: implementation by an extended Prolog compiler.
Journal of Automated Reasoning 4, 4 (December 1988), 353-380.
- Stickel, M.E.
A Prolog technology theorem prover: a new exposition and implementation in Prolog.
Theoretical Computer Science 104 (1992), 109-128.
- Stickel, M.E.
A Prolog technology theorem prover: a new exposition and implementation in Prolog.
Technical Note 464, Artificial Intelligence Center, SRI International,
Menlo Park, California, June 1989. (longer version of above reference that includes
annotated code)
- Stickel, M.E.
A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation.
Annals of Mathematics and Artificial Intelligence 4 (1991), 89-106.
- Hobbs, J.R., M.E. Stickel, D.E. Appelt, and P. Martin.
Interpretation as abduction.
Artificial Intelligence 63, 1-2 (1993), 69-142.
Some Related Systems
Downloads
Mark E. Stickel (stickelai.sri.com)
2006-10-04