A Prolog technology theorem prover: Implementation by an extended Prolog compiler
From MaRDI portal
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.
Recommendations
- scientific article; zbMATH DE number 3986671
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- An examination of the prolog technology theorem-prover
- Prolog technology for default reasoning: proof theory and compilation techniques
- Extensions to logic programming motivated by the construction of a generic theorem prover
- An improved proof-theoretic compilation of logic programs
- scientific article; zbMATH DE number 3965464
- scientific article; zbMATH DE number 4053062
- scientific article; zbMATH DE number 1424017
- Proof-theoretic and higher-order extensions of logic programming
Cites work
- A Hole in Goal Trees: Some Guidance from Resolution Theory
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- A simplified problem reduction format
- An Implementation of the Model Elimination Proof Procedure
- Depth-first iterative-deepening: An optimal admissible tree search
- Experimental tests of resolution-based theorem-proving strategies
- scientific article; zbMATH DE number 3986666 (Why is no real title available?)
- scientific article; zbMATH DE number 3657150 (Why is no real title available?)
- scientific article; zbMATH DE number 3774914 (Why is no real title available?)
- scientific article; zbMATH DE number 3568056 (Why is no real title available?)
- scientific article; zbMATH DE number 3395362 (Why is no real title available?)
- scientific article; zbMATH DE number 3407199 (Why is no real title available?)
- scientific article; zbMATH DE number 3415409 (Why is no real title available?)
- Linear resolution with selection function
- Non-Horn clause logic programming without contrapositives
- Refutation graphs
- Resolution, Refinements, and Search Strategies: A Comparative Study
- Theorem Proving via General Matings
Cited in
(68)- Unrestricted resolution versus N-resolution
- SETHEO: A high-performance theorem prover
- A semantic backward chaining proof system
- Linear resolution for consequence finding
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- SET-VAR
- IDNAF Prolog
- Problem solving by searching for models with a theorem prover
- Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures
- Controlled integration of the cut rule into connection tableau calculi
- Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
- The application of automated reasoning to questions in mathematics and logic
- A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation
- Validation and verification of decision making rules
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- Non-Horn clause logic programming
- Computing answers with model elimination
- IeanCOP: lean connection-based theorem proving
- Efficient model generation through compilation.
- lean\(T^ AP\): Lean tableau-based deduction
- The anatomy of vampire. Implementing bottom-up procedures with code trees
- Avoiding duplicate proofs with the foothold refinement
- Craig interpolation with clausal first-order tableaux
- scientific article; zbMATH DE number 1614712 (Why is no real title available?)
- Improving the time efficiency of proving theorems using a learning mechanism
- nanoCoP: a non-clausal connection prover
- Mark Stickel: his earliest work
- Semantically-guided goal-sensitive reasoning: model representation
- The BinProlog experience: architecture and implementation choices for continuation passing Prolog and first-class logic engines
- Tabling, rational terms, and coinduction finally together!
- History and prospects for first-order automated deduction
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- scientific article; zbMATH DE number 3965464 (Why is no real title available?)
- scientific article; zbMATH DE number 3986671 (Why is no real title available?)
- scientific article; zbMATH DE number 4094866 (Why is no real title available?)
- The theoretical foundations of LPTP (a logic program theorem prover)
- scientific article; zbMATH DE number 1552514 (Why is no real title available?)
- Subgoal alternation in model elimination
- Optimizing proof search in model elimination
- Efficient model generation through compilation
- Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology
- From Schütte’s Formal Systems to Modern Automated Deduction
- Prolog Technology Reinforcement Learning Prover
- Building Theorem Provers
- A novel asynchronous parallelism scheme for first-order logic
- Lemma matching for a PTTP-based top-down theorem prover
- Closures and Modules Within Linear Logic Concurrent Constraint Programming
- α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic
- Refinements to depth-first iterative-deepening search in automatic theorem proving
- Controlled use of clausal lemmas in connection tableau calculi
- Automated generation of readable proofs with geometric invariants. I: Multiple and shortest proof generation
- Automated generation of readable proofs with geometric invariants. II: Theorem proving with full-angles
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- Abductive reasoning with a large knowledge base for discourse processing
- A Prolog assisted search for new simple Lie algebras
- A complete semantic back chaining proof system
- Partheo: A high-performance parallel theorem prover
- An examination of the prolog technology theorem-prover
- Range-restricted and Horn interpolation through clausal tableaux
- Lemmas: generation, selection, application
- A Mizar mode for HOL
- Investigations into proof structures
- Peano arithmetic and MALL
- A semantics for probabilistic hybrid knowledge bases with function symbols
- Synthesizing strongly equivalent logic programs: Beth definability for answer set programs via Craig interpolation in first-order logic
- Compiling a default reasoning system into Prolog
- Logic-based subsumption architecture
This page was built for publication: A Prolog technology theorem prover: Implementation by an extended Prolog compiler
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1114446)
