• English only

# Differences

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

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.