@TechReport{AIDA-94-05,
author = "W.~Bibel and E.~Eder",
title = "Decomposition of {T}autologies into {R}egular
{F}ormulas and {S}trong {C}ompleteness of
{C}onnection-{G}raph {R}esolution",
institution = "FG Intellektik, FB Informatik, TH Darmstadt",
year = "1994",
OPTtype = "",
number = "AIDA--94--05",
OPTaddress = "",
month = aug,
OPTnote = "",
abstract = "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."
}