Clause trees: A tool for understanding and implementing resolution in automated reasoning

DOI10.1016/S0004-3702(96)00046-XzbMath1017.03506OpenAlexW1970444992MaRDI QIDQ1402732

J. D. Horton, Bruce D. Spencer

Publication date: 28 August 2003

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0004-3702(96)00046-x

zbMATH Keywords

RedundancyMinimalityAutomated theorem provingProof procedures

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Uses Software

• SETHEO
• OTTER
• TPTP
• METEOR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Short proofs of the pigeonhole formulas based on the connection method
• The intractability of resolution
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• An extension to linear resolution with selection function
• SETHEO: A high-performance theorem prover
• A Prolog technology theorem prover: A new exposition and implementation in Prolog
• Refutation graphs
• 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
• The use of lemmas in the model elimination procedure
• Avoiding duplicate proofs with the foothold refinement
• Linear resolution with selection function
• Dissolution
• Many hard examples for resolution
• Refutations by Matings
• The relative efficiency of propositional proof systems
• The TPTP problem library
• A Machine-Oriented Logic Based on the Resolution Principle
• Mechanical Theorem-Proving by Model Elimination
• Two Results on Ordering for Resolution with Merging and Linear Format