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 === | ||