Refutation graphs

DOI10.1016/0004-3702(76)90021-7MaRDI QIDQ1226867zbMATH OpenOpenAlexFDO

Authors Robert E. Shostak

Publication date 1976

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL http://www.sciencedirect.com/science/journal/00043702

Mathematics Subject Classification ID

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• A Unifying View of Some Linear Herbrand Procedures
• An Implementation of the Model Elimination Proof Procedure
• scientific article; zbMATH DE number 3320385 (Why is no real title available?)
• scientific article; zbMATH DE number 3407196 (Why is no real title available?)
• Linear resolution with selection function
• Mechanical Theorem-Proving by Model Elimination
• Resolution graphs

Cited in

(20)

• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• Using rewriting rules for connection graphs to prove theorems
• Linear resolution for consequence finding
• Paramodulated connection graphs
• Prolog technology for default reasoning: proof theory and compilation techniques
• 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
• On the termination of clause graph resolution
• A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation
• Clause trees: A tool for understanding and implementing resolution in automated reasoning
• Presenting inequations in mathematical proofs
• A comparative study of several proof procedures
• The linked conjunct method for automatic deduction and related search techniques
• Towards a unified model of search in theorem-proving: subgoal-reduction strategies
• Subgoal alternation in model elimination
• Semantic tableaux with ordering restrictions
• Lemma matching for a PTTP-based top-down theorem prover
• Controlled use of clausal lemmas in connection tableau calculi
• The disconnection tableau calculus
• On connections and higher-order logic

This page was built for publication: Refutation graphs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1226867)