A Prolog technology theorem prover: Implementation by an extended Prolog compiler
type: Item
instance of: scholarly article
title: A Prolog technology theorem prover: Implementation by an extended Prolog compiler
zbMATH Open document ID: 0662.68104
DOI: 10.1007/BF00297245
author: Mark E. Stickel
published in: Journal of Automated Reasoning
publication date: 1988-01-01T00:00:00Z
review text: The author exposes interesting ideas and experiments concerning a Prolog technology theorem prover (PTTP). The goal and the author's option are to ``establish a new standard of performance for theorem proving programs''. The PTTP implementation is an extended Prolog-to-Lisp compiler, written in Common Lisp for Symbolics 3600 LISP machine. In order to obtain a complete theorem prover there are examined the extensions of the classical Prolog features towards: (1) a sound (occurs check) unification; (2) a complete inference system, by adding the reduction rule to the model elimination procedure; (3) a complete search strategy, extending the unbounded depth-first search to the depth-first iterative- deepening search (which, among the advantages, can be naturally parallelized). Current and forthcoming PTTP refinements are discussed. The behaviour of the PTTP compiler when running some concrete examples is exposed. The (very promising) performances of PTTP on a set of 95 problems are presented in detail on a two pages tableau (containing the number of clauses, depth of proof, number of inferences, run time). Important similar approaches are compared and referred. The paper represents a guiding report on outstanding work and results.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68T20
Mathematics Subject Classification ID: 68N01
zbMATH DE Number: 4083033
zbMATH Keywords: automated theorem proving
zbMATH Keywords: Prolog
zbMATH Keywords: compiler
zbMATH Keywords: model elimination procedure
zbMATH Keywords: depth-first search
Wikidata QID: Q56059054
reviewed by: Neculai Curteanu
MaRDI profile type: Publication
cites work: Theorem Proving via General Matings
cites work: Q3954845
cites work: Q3750137
cites work: Q5663380
cites work: Q5679729
cites work: An Implementation of the Model Elimination Proof Procedure
cites work: Depth-first iterative-deepening: An optimal admissible tree search
cites work: Linear resolution with selection function
cites work: Experimental tests of resolution-based theorem-proving strategies
cites work: A Simplified Format for the Model Elimination Theorem-Proving Procedure
cites work: Q4139711
cites work: A Hole in Goal Trees: Some Guidance from Resolution Theory
cites work: Q5672217
cites work: Q3856120
cites work: A simplified problem reduction format
cites work: Non-Horn clause logic programming without contrapositives
cites work: Refutation graphs
cites work: Resolution, Refinements, and Search Strategies: A Comparative Study
DBLP publication ID: journals/jar/Stickel88
Recommended article: Q3750142
Recommended article: A Prolog technology theorem prover: A new exposition and implementation in Prolog
Recommended article: An examination of the prolog technology theorem-prover
Recommended article: Prolog technology for default reasoning: proof theory and compilation techniques
Recommended article: Extensions to logic programming motivated by the construction of a generic theorem prover
Recommended article: An Improved Proof-Theoretic Compilation of Logic Programs
Recommended article: Q3732983
Recommended article: Q3789101
Recommended article: Q4945207
Recommended article: Proof-Theoretic and Higher-Order Extensions of Logic Programming
description: scientific article; zbMATH DE number 4083033