This is an old revision of the document!

QBF and Quantifier Elimination

Quantified Propositional Formulas: syntax and semantics.

Eliminating quantifiers by expansion: \[

  \exists p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \land subst(\{p \mapsto {\it false}\},F)

Note that the expansion can produce exponentially larger formula.

Notion of quantifier elimination applies to other logic as well.

Formula $F$ is valid iff $\forall p_1,\ldots,p_n. F$ is true.

Formula $F$ is satisfiable iff $\exists p_1,\ldots,p_n. F$ is true.

In general QBF formulas can have alternations between $\forall$ and $\exists$ quantifiers: \[

 \forall p. \exists q. ((p \rightarrow q) \land (q \rightarrow r))

Note: