Differences

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

--- sav08:qbf_and_quantifier_elimination [2008/03/10 11:11]
vkuncak
+++ sav08:qbf_and_quantifier_elimination [2008/03/10 11:17]
vkuncak
@@ Line 1: / Line 1: @@
 ====== QBF and Quantifier Elimination ======
-Quantified Propositional Formulas: syntax and semantics.
+=== Quantified Propositional Formula Syntax ===
-Eliminating quantifiers by expansion:
+We extend the definition of formulas with quantifiers $\forall p.F$ and $\exists p.F$ where $p \in V$:
-\[
+\[\begin{array}{rcl}
-    \exists p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \land subst(\{p \mapsto {\it false}\},F)
+   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}
 \]
+=== Eliminating quantifiers by expansion ===
+We can apply the following rules to eliminate propositional quantifiers:
+\[
+    \exists p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \lor subst(\{p \mapsto {\it true}\},F)
+\]
+\[
+    \forall p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \land subst(\{p \mapsto {\it true}\},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.
+Definition: A logic has //quantifier elimination// if for every formula in the logic, there exists an equivalent formula without quantifiers.
-Formula $F$ is satisfiable iff $\exists p_1,\ldots,p_n. F$ is true.
+Definition: A quantifier elimination algorithm is an algorithm that takes a formula in a logic and converts it into an equivalent formula without quantifiers.
+Note: Formula $F$ is valid iff $\forall p_1,\ldots,p_n. F$ is true.
+Note: 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:
@@ Line 21: / Line 36: @@
 \]
-Note:
+=== Quantified Propositional Formula Semantics ===
+We can similarly provide recursive semantic function definition for propositional logic.
+=== Notes on Computational Complexity ===
   * checking satisfiability of propositional formula $F$ is NP-complete
   * checking validity of propositional formula $F$ is coNP-complete
   * checking truth value of arbitrary QBF formula is PSPACE-complete