LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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