Differences

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

--- sav08:combining_fol_models [2009/05/13 10:57]
vkuncak
+++ sav08:combining_fol_models [2015/04/21 17:30] (current)
@@ Line 1: / Line 1: @@
 ====== Combining Decision Procedures =====
 ===== Merging Models of Theories with Disjoint Languages (Signatures) =====
 **Theorem:** Let ${\cal L}$ be a finite language ${\cal L} = {\cal L}_1 \cup {\cal L}_2$ where ${\cal L}_1 \cap {\cal L}_2 = \emptyset$.  Let $C$ be a conjunction in language ${\cal L}$, and for $i\in \{1,2\}$ let $C_i$ be those literals from $C$ whose symbols appear only in ${\cal L}_i$, as well as equality and disequality literals.  Suppose further that if variables $x,y \in FV(C_1)\cap FV(C_2)$ then either $x=y$ appears in $C$ or $x \neq y$ appears in $C$ (thus they also appear in $C_1$ and $C_2$).  Let $Ax_i$ be a set of sentences in language ${\cal L}_i$ for $i\in\{1,2\}$.  Suppose there exists a model for $Ax_i \cup C_i$ for $i\in\{1,2\}$ and that **these models have domains of same cardinality**.  Then there exists a model for $C \cup Ax_1 \cup Ax_2$.
+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.
-**Proof:** There exists an isomorphism of interpretation $I_2$ such that the resulting structure $I'_2$ agrees with $I_1$ on the common variables.  Extending $I_1$ with interpratation of symbols in $I'_2$ we obtain the desired model. **End.**
+**Proof (using merging of models):** There exists an isomorphism of interpretation $I_2$ such that the resulting structure $I'_2$ agrees with $I_1$ on the common variables.  Extending $I_1$ with interpratation of symbols in $I'_2$ we obtain the desired model. **End.**
-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.
+**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 C_2 \cup Ax_1 \cup Ax_2$. By compactness for first-order logic there exists a finite subset that is contradictory. By interpolation there exists an interpolant $I$ that is, say, implied by $C_1 \cup Ax_1$ and contradictory with $C_2 \cup Ax_2$. The interpolant is in the common language, so it contains only equalities. It can be quantified, but over infinite domains quantifiers can be eliminated in a very simple way (and in any case, it is a fragment of BAPA that has QE). So, the result is a disjunction of conjunctions of equalities and disequalities among the common variables. But because $C_1$ and $C_2$ contain a complete atomic type, they either imply or are contradictory with $I$, depending on whether the atomic diagram normal form contains the atomic type present in $C_1,C_2$ or not. Note that $I \cup C_2 \cup Ax_2$ is contradictory since $I$ is interpolant, so each conjunct in its DNF is contradictory. Therefore, $I$ does not have as a disjunct the atomic diagram present in $C_2$ or $C_1$. Then $I$ is contradictory with $C_1$ as well. Since $I$ is a consequence of $C_1 \cup Ax_1$, it follows that $C_1 \cup Ax_1$ is contradictory. But we assumed it is satisfiable. **End**
 **Example:** Take formula
-\[
+\begin{equation*}
-    x=1 \land f(x)=y \land \land z=y+y \land f(z)=x \land y \neq x \land x \le 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.
+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.
 ===== Stable Infiniteness =====
@@ Line 51: / Line 52: @@
   * if all conjuncts are UNSAT (for all arrangements, for all SAT disjuncts), the problem is UNSAT
   * if some conjunct, for some arrangement, is SAT for all decision procedures, then the Theorem above says that the entire conjunction is SAT, so problem is SAT
 ===== Convex Theories =====
@@ Line 60: / Line 60: @@
 In some cases there is no single equality that follows, but only a disjunction can be derived:
-\[
+\begin{equation*}
 \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//.