Differences

This shows you the differences between two versions of the page.

--- sav08:qbf_and_quantifier_elimination [2008/03/11 16:14]
vkuncak
+++ sav08:qbf_and_quantifier_elimination [2015/04/21 17:30] (current)
@@ Line 4: / Line 4: @@
 We extend the definition of formulas with quantifiers $\forall p.F$ and $\exists p.F$ where $p \in V$:
-\[\begin{array}{rcl}
+\begin{equation*}\begin{array}{rcl}
    F  & ::= & V \mid {\it false} \mid {\it true} \mid (F \land F) \mid (F \lor F) \mid (\lnot F) \mid (F \rightarrow F) \mid (F \leftrightarrow F) \\
       & \mid & \forall V. F\ \mid\ \exists V. F
 \end{array}
-\]
+\end{equation*}
 ===== Eliminating quantifiers by expansion =====
 We can apply the following rules to eliminate propositional quantifiers:
-\[
+\begin{equation*}
     \exists p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \lor subst(\{p \mapsto {\it true}\},F)
-\]
+\end{equation*}
-\[
+\begin{equation*}
     \forall p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \land subst(\{p \mapsto {\it true}\},F)
-\]
+\end{equation*}
 Note that the expansion can produce exponentially larger formula.
@@ Line 32: / Line 32: @@
 In general QBF formulas can have alternations between $\forall$ and $\exists$ quantifiers:
-\[
+\begin{equation*}
    \forall p. \exists q. ((p \rightarrow q) \land (q \rightarrow r))
-\]
+\end{equation*}
 ===== Quantified Propositional Formula Semantics =====