REFUTATION GRAPHS AND RESOLUTION THEOREM PROVING
Original Publication Date: 1974-Jan-31
Included in the Prior Art Database: 2007-Mar-29
Software Patent Institute
Shostak, Robert E.: AUTHOR [+2]
REFUTATION GRAPHS AND ELSOLUTION THEORAY PROVIZJG~
REFUTATION GRAPHS AND
ELSOLUTION THEORAY PROVIZJG~
Robert 3. Shostak
Center for Research in Computing Technology
Cambridge, Massachusetts 02138
?This work was supported in part by the Advanced Research Projects Agency under Contract F19628-71-C-0174.
A new graph-theoretic characterization of propositional unaat- isfiability i s introduced providing a lucid perspective on resolution and the relationship among various resolution strategies. The new characterization is used to provide intuitive analyses of the defects
in these strategies, and a new theorem-proving algorithm, called Graph Construction, is put forward which seeks to correct the faults without introducing new ones.
Much of the research conducted in resolution theory has been directed toward the development of refinement strategies , some restricting the order in which literals or clauaes may be used, some relating deductions to models of the axioms, almost all attempting to carve away portions of the unrestrict- ed resolution search apace. A proponent of a new such strategy w i l l typical- ly offer an arcane completeness proof, some select examples demanstrating the ostensible improvement of the proposed system over some other, and a verbal assurrance of general virtue. Frequently, it is apparent from the restric- tion that the new strategy narrows the breadth of the search space, but almost never are there given guarantees against increased depth of search.
The reader, who is generally given no intuitive idea of what makes the restriction complete, let alone better, faces an impossible task in attempt- ing to evaluate the merits of the new strategy.
In the following a new graph-theoretic characterization of propositional msatisfiability l a developed, providing a lucid perspective on resolution, and on the relationship among various resolution strategies. The new characteri- zation is exploited to provide intuitive exposes of the defects in the best
of theee strategies, and a new theorem proving algorithm for first-order logic ir introduced which seeks to correct the faults without introducing new ones.
The paper divides into three parts. In the first se~tion, structures called clause g~aphs are defiued for sets of ground clauses, and unsatisfia- bility l a related to cycles in these graphs. A correspondance between reso- lution refutations and graphs for unsatisfiable sets is established and
shown to provide simple completeness proofs fox various resolution restriction
In the second section, the t-linear and SL refutations of Kowalaki and Kuehner , as well as the Model Elimination (PIE) refutations of Lov...