Thumbnail
Access Restriction
Subscribed

Author Bibel, W. ♦ Eder, E.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1997
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Connection-graph resolution ♦ Decomposition of unsatisfiable formulas ♦ Regular graphs ♦ Semantic trees ♦ Strong completeness
Abstract This paper addresses and answers a fundamental question about resolution. Informally, what is gained with respect to the search for a proof by performing a single resolution step? It is first shown that any unsatisfiable formula may be decomposed into regular formulas provable in linear time (by resolution). A relevant resolution step strictly reduces at least one of the formulas in the decomposition while an irrelevant one does not contribute to the proof in any way. the relevance of this insight into the nature of resolution and of the unsatisfiability problem for the development of proof strategies and for complexity considerations are briefly discussed.The decomposition also provides a technique for establishing completeness proofs for refinements of resolution. As a first application, connection-graph resolution is shown to be strongly complete. This settles a problem that remained open for two decades despite many proff attempts. The result is relevant for theorem proving because without strong completeness a connection graph resolution prover might run into an infinite loop even on the ground level.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1997-03-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 44
Issue Number 2
Page Count 25
Starting Page 320
Ending Page 344


Open content in new tab

   Open content in new tab
Source: ACM Digital Library