Uwe Egly
(Vienna University of Technology - TU Wien)
Quantifier Handling in Different Calculi for Quantified Boolean Formulas

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 Q-resolution and a sequent system with different quantifier rules. I show that the resolution calculi for QBFs do not polynomially simulate cut-free 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 first-order predicate logic where formulas are interpreted only over a two element domain, I will discuss translations of QBFs to first-order formulas and equip first-order resolution with such translations. I will extend the comparison between calculi and investigate whether different translations have different proof-theoretical 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.