Title: An Achilles' Heel of Term-Resolution,
Abstract: Term-resolution provides an elegant mechanism to prove that a quantified
Boolean formula (QBF) is true. It is a dual to Q-resolution (also referred to
as clause-resolution) and is practically highly important as it enables
certifying answers of DPLL-based QBF solvers. While term-resolution and
Q-resolution are very similar, they're not completely symmetric. In particular,
Q-resolution operates on clauses and term-resolution operates on models of the
matrix. This paper investigates what impact this asymmetry has. We'll see that
there is a large class of formulas (formulas with "big models") whose
term-resolution proofs are exponential. As a possible remedy, the paper
suggests to prove true QBFs by refuting their negation ({\em negate-refute}),
rather than proving them by term-resolution. The paper shows that from the
theoretical perspective this is indeed a favorable approach. In particular,
negation-refutation can p-simulates term-resolution and there is an exponential
separation between the two calculi. These observations further our
understanding of proof systems for QBFs and provide a strong theoretical
underpinning for the effort towards non-CNF QBF solvers.