Differences
This shows you the differences between two versions of the page.
| Both sides previous 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:16] 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) \\ | ||
| + | & & \forall V. F\ \mid\ \exists V. F | ||
| + | \end{array} | ||
| + | \] | ||
| === Eliminating quantifiers by expansion === | === Eliminating quantifiers by expansion === | ||