LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
sav07_lecture_5 [2007/04/03 17:37]
vaibhav.rajan 		sav07_lecture_5 [2007/04/03 23:19]
vkuncak
Line 1: Line 1:
-====== Lecture 5 Skeleton ​======+====== Lecture 5 ======
  
 Two important techniques: Two important techniques:
   * Nelson-Oppen combination method   * Nelson-Oppen combination method
   * Proof search   * Proof search
 +
  
 ===== Basic idea of Nelson-Oppen combination ===== ===== Basic idea of Nelson-Oppen combination =====
Line 87: Line 88:
 The models can be merged if \\ The models can be merged if \\
 (1)the domains are of the same size, and \\ (1)the domains are of the same size, and \\
-(2)[x = y]_m1 --> [f(x) = f(y]_m2, where f is an isomorphism from one model to the other.+(2)[x = y]_m1 --> [f(x) = f(y)]_m2, where f is an isomorphism from one model to the other.
  
  
Line 143: Line 144:
  
   * Basic idea, and in the above example (name i from the ∃i as i0, then instantiate ∀i also with i=i0)   * Basic idea, and in the above example (name i from the ∃i as i0, then instantiate ∀i also with i=i0)
-  * examples of incompleteness:+  * example:
  
 Given: f(0) > 0 & ∀x:x > 0. (f(x)>0) --> f(x+1)>0 Given: f(0) > 0 & ∀x:x > 0. (f(x)>0) --> f(x+1)>0
 +
 Prove: ∀x. (x >= 0) --> f(x+1)>0 Prove: ∀x. (x >= 0) --> f(x+1)>0
 +
 Proof: Proof:
-  * f(5) > 0+  * f(5) > 0\\
    f(5): can be derived by deriving f(1), f(2), f(3) and f(4).    f(5): can be derived by deriving f(1), f(2), f(3) and f(4).
   * Then its straightforward to use ∀x:x > 0. (f(x)>0) --> f(x+1)>0 and arrive at the proof.   * Then its straightforward to use ∀x:x > 0. (f(x)>0) --> f(x+1)>0 and arrive at the proof.
  
 For formulas with quantifiers,​ example: (∀x.F1) & F2, substitute values for x in F1. For formulas with quantifiers,​ example: (∀x.F1) & F2, substitute values for x in F1.
 +
 A heuristic that could be used is: Look at constants in F2 and try substituting them. A heuristic that could be used is: Look at constants in F2 and try substituting them.