# 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