Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Last revision Both sides next revision | ||
sav07_lecture_5 [2007/04/03 17:40] vaibhav.rajan |
sav07_lecture_5 [2007/04/03 23:18] vkuncak |
||
---|---|---|---|
Line 4: | Line 4: | ||
* 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. |