Differences

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

--- sav07_lecture_6 [2007/04/15 23:43]
mirco.dotta
+++ sav07_lecture_6 [2007/04/16 01:12]
mirco.dotta
@@ Line 63: / Line 63: @@
 Therefore, formula is satisfiable iff it has a term model.
@@ Line 71: / Line 72: @@
    ¬F1 | R(x,f(g(y)))    (1)
-   ¬R(h(u),f(v)) | F2   (2)
+   ¬R(h(u),f(v)) | F2    (2)
 that is
@@ Line 124: / Line 125: @@
 \end{equation*}
 where $\theta$ is the most general unifier of $A_1$ and $A_2$.
@@ Line 135: / Line 140: @@
-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)) \\
@@ Line 159: / Line 165: @@
   by: ¬(∃x.F) <=> ∀x.¬F   and   ¬(∀x.F) <=> ∃x.¬F
 ∀x.∃y.R(x,y) ∧ ∀y.∃x.¬R(x,y)\\
-  by: Skolenization
+  by: Skolemization
 {R(x, s1(x)), ¬R(s2(y),y)}\\
   by: Unification   s1(x)=y  and  x=s2(y) then s1(s2(y))=y
   by: Adding a constant 'a'
 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)\\
@@ Line 175: / Line 183: @@
 ∀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], Vtx
 \\
 Consider case where R denotes less than relation on integers and Ev denotes that integer is even