• 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) Both sides previous revision Previous revision 2008/04/02 22:59 vkuncak 2008/04/02 22:58 vkuncak 2008/04/02 21:49 vkuncak 2008/04/02 21:49 vkuncak 2008/04/02 21:43 vkuncak 2008/04/02 21:05 vkuncak 2008/04/02 20:45 vkuncak 2008/04/02 20:40 vkuncak 2008/04/02 20:40 vkuncak 2008/04/02 20:36 vkuncak 2008/04/02 16:08 vkuncak 2008/04/02 15:51 vkuncak 2008/04/02 14:08 vkuncak 2008/04/02 01:04 vkuncak 2008/04/02 01:04 vkuncak 2008/04/02 01:03 vkuncak 2008/04/02 00:59 vkuncak 2008/04/01 23:57 vkuncak 2008/03/20 18:09 vkuncak created Next revision Previous revision 2008/04/02 22:59 vkuncak 2008/04/02 22:58 vkuncak 2008/04/02 21:49 vkuncak 2008/04/02 21:49 vkuncak 2008/04/02 21:43 vkuncak 2008/04/02 21:05 vkuncak 2008/04/02 20:45 vkuncak 2008/04/02 20:40 vkuncak 2008/04/02 20:40 vkuncak 2008/04/02 20:36 vkuncak 2008/04/02 16:08 vkuncak 2008/04/02 15:51 vkuncak 2008/04/02 14:08 vkuncak 2008/04/02 01:04 vkuncak 2008/04/02 01:04 vkuncak 2008/04/02 01:03 vkuncak 2008/04/02 00:59 vkuncak 2008/04/01 23:57 vkuncak 2008/03/20 18:09 vkuncak created 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.

sav08/herbrand_universe_for_equality.txt · Last modified: 2015/04/21 17:30 (external edit)

© EPFL 2018 - Legal notice 