Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav07_lecture_5 [2007/04/03 17:40] 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. |