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

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Nov 01, 1987
Accession Number
ADA461775

Entities

People

  • Mark E. Stickel

Organizations

  • SRI International

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Artificial Intelligence Computing
  • Availability
  • Calculus
  • Classification
  • Compilers
  • Contracts
  • Elimination
  • Information Operations
  • Instructions
  • Monitoring
  • Reasoning
  • Security
  • Standards

Fields of Study

  • Computer science

Readers

  • Computational Linguistics

Technology Areas

  • AI & ML
  • AI & ML - Machine Learning Algorithms