Kluger.PA@PARC-MAXC.ARPA (03/01/84)
[Forwarded from the SRI-AI bboard by Laws@SRI-AI.]
Mark E. Stickel
SRI International
A Prolog Technology Theorem Prover
An extension of Prolog, based on the model elimination theorem-proving
procedure, would permit production of a Prolog technology theorem prover
(PTTP). This would be a complete theorem prover for the full first-order
predicate calculus, not just Horn clauses, and provide capabilities for
full handling of logical negation and indefinite answers. It would be
capable of performing inference operations at a rate approaching that of
Prolog itself--substantially faster than conventional theorem-proving
systems.
PTTP differs from Prolog in its use of unification with the "occurs
check" for soundness, the complete model elimination input inference
procedure, and a complete staged depth-first search strategy. The use of
an input inference procedure and depth-first search minimize the
differences between this theorem-proving method and Prolog and permit the
use of highly efficient Prolog implementation techniques.
Thursday, March 8, 1984 4:00 pm
Hewlett Packard
Stanford Division
5M Conference room
1501 Page Mill Rd
Palo Alto
*** Be sure to arrive at the building's lobby on time, so that you may
be escorted to the meeting room.