A Prolog technology theorem prover: A new exposition and implementation in Prolog
A Prolog technology theorem prover (PTTP) [\textit{M. E. Stickel}, J. Autom. Reasoning 4, No. 4, 353-380 (1988; Zbl 0662.68104)] is an extension of Prolog that is complete for the full first-order predicate calculus. This is achieved through 3 strategic changes: \(\bullet\) A unification algorithm is used with the occur check, \(\bullet\) unbounded depth-first search is replaced by depth-first iterative deepening search, and \(\bullet\) the model elimination reduction rule is added to Prolog inferences. The paper offers a concise and readable description of the PTTP implementation in Prolog. The performance of the resulting logic program is approaching that of Lisp PTTP implementations. Special attention is given to suggestions of possible extensions to Prolog that would enable a higher performance of PTTP logic programs.
- A logical framework for default reasoning
- A note on linear resolution strategies in consequence-finding
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation
- A sequent-style model elimination strategy and a positive refinement
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- An algorithm to compute circumscription
- An examination of the prolog technology theorem-prover
- An Implementation of the Model Elimination Proof Procedure
- Automated deduction by theory resolution
- Depth-first iterative-deepening: An optimal admissible tree search
- scientific article; zbMATH DE number 4180829 (Why is no real title available?)
- scientific article; zbMATH DE number 4164124 (Why is no real title available?)
- scientific article; zbMATH DE number 4164187 (Why is no real title available?)
- scientific article; zbMATH DE number 3978351 (Why is no real title available?)
- scientific article; zbMATH DE number 4049120 (Why is no real title available?)
- scientific article; zbMATH DE number 67457 (Why is no real title available?)
- scientific article; zbMATH DE number 192840 (Why is no real title available?)
- scientific article; zbMATH DE number 3568056 (Why is no real title available?)
- Linear resolution with selection function
- Non-Horn clause logic programming without contrapositives
- SETHEO: A high-performance theorem prover
- The Specialization of Programs by Theorem Proving
- The technology chess program
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- A Prolog technology theorem prover: A new exposition and implementation in Prolog
- Prolog technology for default reasoning: proof theory and compilation techniques
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- Non-Horn clause logic programming
- IeanCOP: lean connection-based theorem proving
- Practically useful variants of definitional translations to normal form
- Linear and unit-resulting refutations for Horn theories
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- Partition-based logical reasoning for first-order and propositional theories
- Mark Stickel: his earliest work
- Semantically-guided goal-sensitive reasoning: model representation
- Logic programming as a basis for lean automated deduction
- Efficient description logic reasoning in Prolog: The DLog system
- scientific article; zbMATH DE number 3986671 (Why is no real title available?)
- scientific article; zbMATH DE number 4094866 (Why is no real title available?)
- IMPLEMENTING COMPLEX DOMAINS OF APPLICATION IN AN EXTENDED PROLOG SYSTEM
- A new term representation method for prolog
- The theoretical foundations of LPTP (a logic program theorem prover)
- \(\mathsf{XRay}\): a Prolog technology theorem prover for default reasoning: a system description
- On the practical value of different definitional translations to normal form
- Extensions to logic programming motivated by the construction of a generic theorem prover
- Logistica 2.0: a technology for implementing automatic deduction systems
- Building Theorem Provers
- Lemma matching for a PTTP-based top-down theorem prover
- Mode-Directed Inverse Entailment for Full Clausal Theories
- Prolog Based Description Logic Reasoning
- Fifty Years of Prolog and Beyond
- An examination of the prolog technology theorem-prover
- Compiling a default reasoning system into Prolog
- Logic-based subsumption architecture
This page was built for publication: A Prolog technology theorem prover: A new exposition and implementation in Prolog
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1199932)
