A Prolog technology theorem prover: A new exposition and implementation in Prolog

DOI10.1016/0304-3975(92)90168-FzbMath0771.68096MaRDI QIDQ1199932

Mark E. Stickel

Publication date: 17 January 1993

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

search strategiesmodel elimination

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Logic programming (68N17)

Related Items (21)

Mark Stickel: his earliest work ⋮ Semantically-guided goal-sensitive reasoning: model representation ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Fifty Years of Prolog and Beyond ⋮ Clause trees: A tool for understanding and implementing resolution in automated reasoning ⋮ Non-Horn clause logic programming ⋮ IeanCOP: lean connection-based theorem proving ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ Partition-based logical reasoning for first-order and propositional theories ⋮ XRay: A prolog technology theorem prover for default reasoning: A system description ⋮ On the practical value of different definitional translations to normal form ⋮ A Prolog technology theorem prover: A new exposition and implementation in Prolog ⋮ Building Theorem Provers ⋮ Mode-Directed Inverse Entailment for Full Clausal Theories ⋮ Compiling a default reasoning system into Prolog ⋮ Efficient description logic reasoning in Prolog: The DLog system ⋮ Prolog technology for default reasoning: proof theory and compilation techniques ⋮ Lemma matching for a PTTP-based top-down theorem prover ⋮ Prolog Based Description Logic Reasoning ⋮ Practically useful variants of definitional translations to normal form ⋮ Logic-based subsumption architecture

Uses Software

• SETHEO
• PARTHEO
• PARTHENON
• METEOR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Depth-first iterative-deepening: An optimal admissible tree search
• A logical framework for default reasoning
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• An algorithm to compute circumscription
• Non-Horn clause logic programming without contrapositives
• SETHEO: A high-performance theorem prover
• A Prolog technology theorem prover: A new exposition and implementation in Prolog
• A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation
• Automated deduction by theory resolution
• Linear resolution with selection function
• The technology chess program
• A note on linear resolution strategies in consequence-finding
• A sequent-style model elimination strategy and a positive refinement
• An Implementation of the Model Elimination Proof Procedure
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• The Specialization of Programs by Theorem Proving

This page was built for publication: A Prolog technology theorem prover: A new exposition and implementation in Prolog