Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:combining_fol_models [2009/05/13 10:48] vkuncak |
sav08:combining_fol_models [2009/05/13 10:57] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Combining Decision Procedures ===== | ====== Combining Decision Procedures ===== | ||
| + | |||
| Line 11: | Line 12: | ||
| Note: for $C$ to satisfy the condition, it suffices for it to be flat and to contain equality or disequality for all common variables. One possible way to achieve this is [[Atomic Diagram Normal Form]] but there is no need to do case analysis on literals other than equality literals. | Note: for $C$ to satisfy the condition, it suffices for it to be flat and to contain equality or disequality for all common variables. One possible way to achieve this is [[Atomic Diagram Normal Form]] but there is no need to do case analysis on literals other than equality literals. | ||
| + | **Example:** Take formula | ||
| + | \[ | ||
| + | x=1 \land f(x)=y \land \land z=y+y \land f(z)=x \land y \neq x \land x \le x | ||
| + | \] | ||
| + | If we take a finite model for uninterpreted functions, we cannot merge it with the model for addition. But there is an infinite model for uninterpreted functions as well, and we can merge this model. | ||
| ===== Stable Infiniteness ===== | ===== Stable Infiniteness ===== | ||