Search |  Contact |  SRI Home Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap.A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A ASRI International.  333 Ravenswood Avenue.  Menlo Park, CA 94025-3493. SRI International is a nonprofit corporation.

Publication in BibTeX Format

@TECHREPORT{AICPub577:1987, AUTHOR={Stickel, Mark E.}, TITLE={A Prolog Technology Theorem Prover: Implementation By An Extended, Prolog Compiler}, ADDRESS={333 Ravenswood Ave., Menlo Park, CA 94025}, INSTITUTION={AI Center, SRI International}, MONTH={Nov}, NUMBER={382}, YEAR={1987}, KEYWORDS={Deduction!PTTP, PTTP, Prolog}, ABSTRACT={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.}, NOTE={Originally published April 1986. Revised November 1987.} }

SRI International
©2014 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy