Browse Prior Art Database

REFUTATION GRAPHS AND RESOLUTION THEOREM PROVING

IP.com Disclosure Number: IPCOM000148411D
Original Publication Date: 1974-Jan-31
Included in the Prior Art Database: 2007-Mar-29
Document File: 91 page(s) / 3M

Publishing Venue

Software Patent Institute

Related People

Shostak, Robert E.: AUTHOR [+2]

Abstract

REFUTATION GRAPHS AND ELSOLUTION THEORAY PROVIZJG~ Robert 3. Shostak Center for Research in Computing Technology Harvard University Cambridge, Massachusetts 02138 ?This work was supported in part by the Advanced Research Projects Agency under Contract F19628-71-C-0174. Abstract 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.

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 4% of the total text.

Page 1 of 91

REFUTATION GRAPHS AND

ELSOLUTION THEORAY PROVIZJG~

Robert 3. Shostak

Center for Research in Computing Technology

     Harvard University
Cambridge, Massachusetts 02138

   ?This work was supported in part by the Advanced Research Projects Agency under Contract F19628-71-C-0174.

[This page contains 1 picture or other non-text object]

Page 2 of 91

Abstract

   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.

[This page contains 1 picture or other non-text object]

Page 3 of 91

    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

[This page contains 1 picture or other non-text object]

Page 4 of 91

e trategies.

    In the second section, the t-linear and SL refutations of Kowalaki and Kuehner [7], as well as the Model Elimination (PIE) refutations of Lov...