Clause trees: A tool for understanding and implementing resolution in automated reasoning
From MaRDI portal
Publication:1402732
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
Uses Software
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
