Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:quantifier_elimination_definition [2011/04/05 16:02] vkuncak |
sav08:quantifier_elimination_definition [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 6: | Line 6: | ||
As a special case, we can have | As a special case, we can have | ||
- | \[ | + | \begin{equation*} |
T = \{ F \mid \forall I \in {\cal I}. e_F(F)(I) \} | T = \{ F \mid \forall I \in {\cal I}. e_F(F)(I) \} | ||
- | \] | + | \end{equation*} |
where ${\cal I}$ is a set of interpretations of interest. | where ${\cal I}$ is a set of interpretations of interest. | ||
Then $\models F$ reduces to $\forall I \in {\cal I}. e_F(F)(I)$. | Then $\models F$ reduces to $\forall I \in {\cal I}. e_F(F)(I)$. | ||
Line 36: | Line 36: | ||
Example: in language ${\cal L} = \{0,1,+\}$ where $0,1$ are constants and $+$ is a binary operation, an example of a ground formula is | Example: in language ${\cal L} = \{0,1,+\}$ where $0,1$ are constants and $+$ is a binary operation, an example of a ground formula is | ||
- | \[ | + | \begin{equation*} |
\lnot (0 = 1) \rightarrow \lnot (0 + 1 = 1 + 1) | \lnot (0 = 1) \rightarrow \lnot (0 + 1 = 1 + 1) | ||
- | \] | + | \end{equation*} |
**Lemma:** Suppose that | **Lemma:** Suppose that |