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.}
}