Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:qbf_and_quantifier_elimination [2008/03/10 11:14] vkuncak |
sav08:qbf_and_quantifier_elimination [2008/03/10 11:17] vkuncak |
||
---|---|---|---|
Line 3: | Line 3: | ||
=== Quantified Propositional Formula Syntax === | === Quantified Propositional Formula Syntax === | ||
+ | We extend the definition of formulas with quantifiers $\forall p.F$ and $\exists p.F$ where $p \in V$: | ||
+ | \[\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} | ||
+ | \] | ||
=== Eliminating quantifiers by expansion === | === Eliminating quantifiers by expansion === | ||
Line 29: | Line 35: | ||
\forall p. \exists q. ((p \rightarrow q) \land (q \rightarrow r)) | \forall p. \exists q. ((p \rightarrow q) \land (q \rightarrow r)) | ||
\] | \] | ||
+ | |||
+ | === Quantified Propositional Formula Semantics === | ||
+ | |||
+ | We can similarly provide recursive semantic function definition for propositional logic. | ||
=== Notes on Computational Complexity === | === Notes on Computational Complexity === |