Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction

DOI10.1007/BF00881955zbMath0819.68113MaRDI QIDQ1344881

Mark E. Stickel

Publication date: 22 February 1995

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

Horn clausesbottom-up reasoning systemsforward-chaining reasoning systems

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Mechanization of proofs and logical operations (03B35)

Related Items

SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy, SATCHMORE: SATCHMO with RElevancy, Linear and unit-resulting refutations for Horn theories, Clause trees: A tool for understanding and implementing resolution in automated reasoning, \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE, Incorporating top-down information into bottom-up hypothetical reasoning, The TPTP problem library, Blocking and other enhancements for bottom-up model generation methods, Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving

Uses Software

• OTTER
• SATCHMO

Cites Work

• An efficient strategy for non-Horn deductive databases
• Generating relevant models
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• An algorithm to compute circumscription
• Non-Horn clause logic programming without contrapositives
• Linear resolution for consequence finding
• Refutation graphs
• A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation
• The Alexander Method - a technique for the processing of recursive axioms in deductive databases
• A sequent-style model elimination strategy and a positive refinement
• Refutation search for Horn sets by a subgoal-extraction method
• A Probabilistic Causal Model for Diagnostic Problem Solving Part I: Integrating Symbolic Causal Inference with Numeric Probabilistic Inference
• A Probabilistic Causal Model for Diagnostic Problem Solving Part II: Diagnostic Strategy
• Efficient bottom-up computation of queries on stratified databases
• Proving Theorems with the Modification Method
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item