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/15 23:43] mirco.dotta |
sav07_lecture_6 [2007/04/16 00:08] mirco.dotta |
||
---|---|---|---|
Line 63: | Line 63: | ||
Therefore, formula is satisfiable iff it has a term model. | Therefore, formula is satisfiable iff it has a term model. | ||
+ | |||
Line 71: | Line 72: | ||
¬F1 | R(x,f(g(y))) (1) | ¬F1 | R(x,f(g(y))) (1) | ||
- | ¬R(h(u),f(v)) | F2 (2) | + | ¬R(h(u),f(v)) | F2 (2) |
that is | that is | ||
Line 124: | 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 135: | Line 139: | ||
- | Proof that the formula(1) is valid, by proving that the negation of the formula does not end with a counter-example. | + | Proof that the formula(1) is valid, by proving that the negation of the formula does not end with a counter-example |
+ | (same principle seen in lecture 5 to prove validity of loop invariant). | ||
¬(∃y.∀x.R(x,y) => ∀x.∃y.R(x,y)) \\ | ¬(∃y.∀x.R(x,y) => ∀x.∃y.R(x,y)) \\ | ||
Line 159: | Line 164: | ||
by: ¬(∃x.F) <=> ∀x.¬F and ¬(∀x.F) <=> ∃x.¬F | by: ¬(∃x.F) <=> ∀x.¬F and ¬(∀x.F) <=> ∃x.¬F | ||
∀x.∃y.R(x,y) ∧ ∀y.∃x.¬R(x,y)\\ | ∀x.∃y.R(x,y) ∧ ∀y.∃x.¬R(x,y)\\ | ||
- | by: Skolenization | + | by: Skolemization |
{R(x, s1(x)), ¬R(s2(y),y)}\\ | {R(x, s1(x)), ¬R(s2(y),y)}\\ | ||
by: Unification s1(x)=y and x=s2(y) then s1(s2(y))=y | by: Unification s1(x)=y and x=s2(y) then s1(s2(y))=y | ||
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)\\ |