Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav07_lecture_6 [2007/04/16 00:05] mirco.dotta |
sav07_lecture_6 [2007/04/16 01:13] mirco.dotta |
||
---|---|---|---|
Line 125: | Line 125: | ||
\end{equation*} | \end{equation*} | ||
where $\theta$ is the most general unifier of $A_1$ and $A_2$. | where $\theta$ is the most general unifier of $A_1$ and $A_2$. | ||
+ | |||
+ | |||
+ | |||
Line 168: | Line 171: | ||
by: Adding a constant 'a' | by: Adding a constant 'a' | ||
R.{s1,s2,a} = L \\ | R.{s1,s2,a} = L \\ | ||
+ | \\ | ||
+ | Term(L) = {a, s1(a), s2(a), s1(s1(a)), ...} \\ | ||
\\ | \\ | ||
[R]e<sub>T</sub> = {(t,s1(t)) | t ∈ Term(L)} where e<sub>T</sub>: F => {true, false} and T => Term(L)\\ | [R]e<sub>T</sub> = {(t,s1(t)) | t ∈ Term(L)} where e<sub>T</sub>: F => {true, false} and T => Term(L)\\ | ||
Line 179: | Line 184: | ||
∀t ∈ Term(L) ¬[R(s2(y),y) ] R(s2(y),y)]e<sub>T[y:=t]</sub> \\ | ∀t ∈ Term(L) ¬[R(s2(y),y) ] R(s2(y),y)]e<sub>T[y:=t]</sub> \\ | ||
\\ | \\ | ||
+ | [R]e<sub>T</sub> = {(a,s1(a)), (s1(a),s1(s1(a))), (s2(a), s2(s2(a))), ...} \\ | ||
\\ | \\ | ||
+ | Then we should find a pair (tx,ty) s.t. (tx,ty) ∉ [R]. A possible counter-example is (tx,a) ∉ [R], ∀tx | ||
\\ | \\ | ||
Consider case where R denotes less than relation on integers and Ev denotes that integer is even | Consider case where R denotes less than relation on integers and Ev denotes that integer is even |