Egly, U. (2012). On Sequent Systems and Resolution for QBFs. In Theory and Applications of Satisfiability Testing – SAT 2012 (pp. 100–113). Lecture Notes in Computer Science, Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-31612-8_9
E192-03 - Forschungsbereich Knowledge Based Systems
Theory and Applications of Satisfiability Testing – SAT 2012
International Conference on the Theory and Applications of Satisfiability Testing
17-Jun-2012 - 20-Jun-2012
Trento, Italien, EU
Number of Pages:
Lecture Notes in Computer Science, Springer Berlin Heidelberg, 7317
Resolution; Sequent calculus; Quantified boolean formula
Quantified Boolean formulas generalize propositional formulas by admitting quantifications over propositional variables. We compare proof systems with different quantifier handling paradigms for quantified Boolean formulas (QBFs) with respect to their ability to allow succinct proofs. We analyze cut-free sequent systems extended by different quantifier rules and show that some rules are better than some others.
Q-resolution is an elegant extension of propositional resolution to QBFs and is applicable to formulas in prenex conjunctive normal form. In Q-resolution, there is no explicit handling of quantifiers by specific rules. Instead the forall reduction rule which operates on single clauses inspects the global quantifier prefix. We show that there are classes of formulas for which there are short cut-free tree proofs in a sequent system, but any Q-resolution refutation of the negation of the formula is exponential.
Quantified Boolean Formulas: S 11409-N23 (Fonds zur Förderung der wissenschaftlichen Forschung (FWF))