Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
U. Egly:
"On Sequent Systems and Resolution for QBFs";
Vortrag: International Conference on the Theory and Applications of Satisfiability Testing,
Trento, Italien;
17.06.2012
- 20.06.2012; 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;
S. 100
- 113.
Kurzfassung englisch:
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.
Schlagworte:
Sequent calculus, Resolution, Quantified boolean formula,
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-642-31612-8_9
Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/PubDat_214419.pdf
Zugeordnete Projekte:
Projektleitung Uwe Egly:
Quantified Boolean Formulas
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.