Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:herbrand_universe_for_equality [2008/04/02 22:58] vkuncak |
sav08:herbrand_universe_for_equality [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 2: | Line 2: | ||
Recall example of formula $F$: | Recall example of formula $F$: | ||
- | \[ | + | \begin{equation*} |
P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. x=a \lor x=b) | P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. x=a \lor x=b) | ||
- | \] | + | \end{equation*} |
Replace '=' with 'eq': | Replace '=' with 'eq': | ||
- | \[ | + | \begin{equation*} |
P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. eq(x,a) \lor eq(x,b)) | P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. eq(x,a) \lor eq(x,b)) | ||
- | \] | + | \end{equation*} |
call the resulting formula $F'$. | call the resulting formula $F'$. | ||
Line 24: | Line 24: | ||
- $S$ has a model; | - $S$ has a model; | ||
- $S' \cup AxEq$ has a model (where $AxEq$ are [[Axioms for Equality]] and $S'$ is result of replacing '=' with 'eq' in $S$); | - $S' \cup AxEq$ has a model (where $AxEq$ are [[Axioms for Equality]] and $S'$ is result of replacing '=' with 'eq' in $S$); | ||
- | - $S$ has a model whose domain is the quotient $[GT]$ of ground terms under some congruence. | + | - $S$ has a model whose domain is the quotient $[GT]$ of the set of ground terms under some congruence. |