Refutation graphs
From MaRDI portal
Publication:1226867
DOI10.1016/0004-3702(76)90021-7zbMath0328.68080OpenAlexW2914936697MaRDI QIDQ1226867
Publication date: 1976
Published in: Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: http://www.sciencedirect.com/science/journal/00043702
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (20)
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 ⋮ A Prolog technology theorem prover: Implementation by an extended Prolog compiler ⋮ The disconnection tableau calculus ⋮ Using rewriting rules for connection graphs to prove theorems ⋮ Clause trees: A tool for understanding and implementing resolution in automated reasoning ⋮ On connections and higher-order logic ⋮ Subgoal alternation in model elimination ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ Linear resolution for consequence finding ⋮ Controlled use of clausal lemmas in connection tableau calculi ⋮ Semantic tableaux with ordering restrictions ⋮ Paramodulated connection graphs ⋮ Presenting inequations in mathematical proofs ⋮ Prolog technology for default reasoning: proof theory and compilation techniques ⋮ Lemma matching for a PTTP-based top-down theorem prover ⋮ A comparative study of several proof procedures ⋮ The linked conjunct method for automatic deduction and related search techniques
Cites Work
- Unnamed Item
- Unnamed Item
- Resolution graphs
- Linear resolution with selection function
- An Implementation of the Model Elimination Proof Procedure
- A Machine-Oriented Logic Based on the Resolution Principle
- Mechanical Theorem-Proving by Model Elimination
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- A Unifying View of Some Linear Herbrand Procedures
This page was built for publication: Refutation graphs
