Accession Number:

ADA461775

Title:

A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler

Descriptive Note:

Journal article

Corporate Author:

SRI INTERNATIONAL MENLO PARK CA ARTIFICIAL INTELLIGENCE CENTER

Personal Author(s):

Report Date:

1987-11-01

Pagination or Media Count:

39.0

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.

Subject Categories:

  • Theoretical Mathematics
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE