Clause trees: a tool for understanding and implementing resolution in automated reasoning
- 31 May 1997
- journal article
- Published by Elsevier in Artificial Intelligence
- Vol. 92 (1-2) , 25-89
- https://doi.org/10.1016/s0004-3702(96)00046-x
Abstract
No abstract availableKeywords
This publication has 23 references indexed in Scilit:
- DissolutionJournal of the ACM, 1993
- A Prolog technology theorem prover: a new exposition and implementation in PrologTheoretical Computer Science, 1992
- Many hard examples for resolutionJournal of the ACM, 1988
- An extension to linear resolution with selection functionInformation Processing Letters, 1982
- The relative efficiency of propositional proof systemsThe Journal of Symbolic Logic, 1979
- Refutation graphsArtificial Intelligence, 1976
- Linear resolution with selection functionArtificial Intelligence, 1972
- Two Results on Ordering for Resolution with Merging and Linear FormatJournal of the ACM, 1971
- Mechanical Theorem-Proving by Model EliminationJournal of the ACM, 1968
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965