Differences

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

--- sav08:combining_fol_models [2009/05/13 10:21]
vkuncak
+++ sav08:combining_fol_models [2009/05/13 10:57]
vkuncak
@@ 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$.
+**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$.
@@ 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.
+**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 =====