Uwe Egly

Quantified Boolean formulas (QBFs) generalize propositional formulas by admitting quantifications over propositional variables. In this talk, I will discuss the handling of quantifiers in different calculi for QBFs. The considered calculi are various versions of Qresolution and a sequent system with different quantifier rules. I show that the resolution calculi for QBFs do not polynomially simulate cutfree sequent systems where weak quantifiers introduce propositional atoms or truth constants and the proofs are restricted to tree form. Since QBFs can be considered as a restriction of firstorder predicate logic where formulas are interpreted only over a two element domain, I will discuss translations of QBFs to firstorder formulas and equip firstorder resolution with such translations. I will extend the comparison between calculi and investigate whether different translations have different prooftheoretical strength. The key feature which enables short proofs is formula instantiation, a technique which is currently not available in implemented deduction systems for QBFs. The results show that this technique has the potential to simplify proofs and hopefully the automated search for them. 