[Back]

U. Egly:
"On Sequent Systems and Resolution for QBFs";
Talk: International Conference on the Theory and Applications of Satisfiability Testing, Trento, Italien; 2012-06-17 - 2012-06-20; in: "Theory and Applications of Satisfiability Testing - SAT 2012", Lecture Notes in Computer Science, Springer Berlin Heidelberg, 7317 (2012), ISBN: 978-3-642-31611-1; 100 - 113.

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.

Sequent calculus, Resolution, Quantified boolean formula,

http://dx.doi.org/10.1007/978-3-642-31612-8_9

http://publik.tuwien.ac.at/files/PubDat_214419.pdf

Project Head Uwe Egly:
Quantified Boolean Formulas