Refutations by Matings
- 1 August 1976
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computers
- Vol. C-25 (8), 801-807
- https://doi.org/10.1109/tc.1976.1674698
Abstract
Occurrences of literals in the initial clauses of a refutation by resolution (with each clause-occurrence used only once) are mated iff their descendants are resolved with each other. This leads to an abstract notion of a mating as a relation between: occurrences of literals in a set of clause-occurrences. The existence of many refutations with the same mating leads to wasteful redundancy in the search for a refutation, so it is natural to focus on the essential problem of finding appropriate matings.Keywords
This publication has 8 references indexed in Scilit:
- Eliminating the Irrelevant from Mechanical ProofsPublished by Springer Nature ,1983
- Refutation graphsArtificial Intelligence, 1976
- Resolution graphsArtificial Intelligence, 1970
- Resolution With MergingJournal of the ACM, 1968
- Mechanical Theorem-Proving by Model EliminationJournal of the ACM, 1968
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965
- The unit preference strategy in theorem provingPublished by Association for Computing Machinery (ACM) ,1964
- A proof procedure for quantification theoryThe Journal of Symbolic Logic, 1955