• English only

# Differences

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

sav08:combining_fol_models [2012/05/21 19:48]
vkuncak
sav08:combining_fol_models [2015/04/21 17:30] (current)
Line 11: Line 11:
**Proof (using interpolation):​** First-order logic has interpolation property, by Craig'​s interpolation theorem. Suppose we have models for  **Proof (using interpolation):​** First-order logic has interpolation property, by Craig'​s interpolation theorem. Suppose we have models for
\$C_1 \cup Ax_1\$ and \$C_2 \cup Ax_2\$, but that there is no model for \$C_1 \cup Ax_1\$ and \$C_2 \cup Ax_2\$, but that there is no model for

**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//.