Previous: TR 94-04 Next: TR 94-07

Intellektik: Technical report 94-05

Decomposition of Tautologies into Regular Formulas and Strong Completeness of Connection-Graph Resolution

W. Bibel and E. Eder

This paper addresses and answers a fundamental question about (ground) 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 novel 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 novel technique for establishing completeness proofs for refinements of resolution. As a first application, connection-graph resolution is shown to be strongly complete on the ground level. The result (as well as the aforementioned answer) can be lifted to the first-order level the way briefly outlined in the paper. This settles a problem which remained open for two decades despite many proof 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.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry