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:16] vkuncak |
sav08:qbf_and_quantifier_elimination [2008/03/10 11:17] vkuncak |
||
---|---|---|---|
Line 6: | Line 6: | ||
\[\begin{array}{rcl} | \[\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) \\ | 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) \\ | ||
- | & & \forall V. F\ \mid\ \exists V. F | + | & \mid & \forall V. F\ \mid\ \exists V. F |
\end{array} | \end{array} | ||
\] | \] | ||
Line 35: | 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 === |