This is an old revision of the document!
QBF and Quantifier Elimination
Quantified Propositional Formulas: syntax and semantics.
Eliminating quantifiers by expansion. The cost of expansion.
Notion of quantifier elimination applies to other logic as well.
Formula is valid iff is true.
Formula is satisfiable iff is true.
In general QBF formulas can have alternations between and quantifiers: \[
\forall p. \exists q. ((p \rightarrow q) \land (q \rightarrow r))
\]
Note:
- 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