• English only

QBF and Quantifier Elimination

Quantified Propositional Formula Syntax

We extend the definition of formulas with quantifiers and where : Eliminating quantifiers by expansion

We can apply the following rules to eliminate propositional quantifiers:  Note that the expansion can produce exponentially larger formula.

Notion of quantifier elimination applies to other logic as well.

Definition: A logic has quantifier elimination if for every formula in the logic, there exists an equivalent formula without quantifiers.

Definition: A quantifier elimination algorithm is an algorithm that takes a formula in a logic and converts it into an equivalent formula without quantifiers.

Observation: Formula is valid iff is true.

Observation: Formula is satisfiable iff is true.

In general QBF formulas can have alternations between and quantifiers: Quantified Propositional Formula Semantics

We can similarly provide recursive semantic function definition for propositional logic.

Summary of Computational Complexity of Problems

• checking satisfiability of propositional formula is NP-complete
• checking validity of propositional formula is coNP-complete
• checking truth value of arbitrary QBF formula is PSPACE-complete 