Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:combining_fol_models [2012/05/21 20:09] vkuncak |
sav08:combining_fol_models [2015/04/21 17:30] (current) |
||
|---|---|---|---|
| Line 14: | Line 14: | ||
| **Example:** Take formula | **Example:** Take formula | ||
| - | \[ | + | \begin{equation*} |
| x=1 \land f(x)=y \land z=y+y \land f(z)=x \land y \neq x | x=1 \land f(x)=y \land z=y+y \land f(z)=x \land y \neq x | ||
| - | \] | + | \end{equation*} |
| 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 with the model for integers. | 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 with the model for integers. | ||
| Line 60: | Line 60: | ||
| In some cases there is no single equality that follows, but only a disjunction can be derived: | In some cases there is no single equality that follows, but only a disjunction can be derived: | ||
| - | \[ | + | \begin{equation*} |
| 1 \le x \land x \le 2 \land y = 1 \land z = 2 | 1 \le x \land x \le 2 \land y = 1 \land z = 2 | ||
| - | \] | + | \end{equation*} |
| implies $x=y \lor x=z$ but not any other non-trivial equality between variables. We say integer linear arithmetic is a //non-convex theory//. | implies $x=y \lor x=z$ but not any other non-trivial equality between variables. We say integer linear arithmetic is a //non-convex theory//. | ||