Differences

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

--- sav08:combining_fol_models [2009/05/12 23:55]
vkuncak
+++ sav08:combining_fol_models [2009/05/13 10:48]
vkuncak
@@ Line 4: / Line 4: @@
 ===== 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 88: / Line 88: @@
 Recent approach - try to propagate candidate equalities (even if they are not implied)
   * [[http://research.microsoft.com/projects/z3/smt07.pdf|Model-based Theory Combination]], Leonardo de Moura and Nikolaj Bjørner, Workshop on Satisfiability Modulo Theories (SMT), Berlin, Germany, 2007.
+===== Complexity =====
+  * if each theory is convex and polynomial time (e.g. congruence closure + real linear arithmetic), then conjunctions can be decided in PTIME
+  * if each theory is NP (e.g. we also allow integer linear programming), then (even for non-convex theories), any quantifier-free combination is in NP
 ===== Theories with Non-Disjoint Languages =====
@@ Line 97: / Line 102: @@
 Proof idea:
   * FOL has interpolation property
-  * if the formula is unsatisfiable, there exists an interpolant, which generalizes the notion of arrangement of equalities
+  * if the formula is unsatisfiable, there exists an interpolant in language ${\cal L}_1 \cap {\cal L}_2$, which generalizes the notion of //arrangement// for equalities
   * if we have quantifier elimination for formulas in ${\cal L}_1 \cap {\cal L}_2$ with respect to $T_1 \cup T_2$, then arrangements are quantifier-free
-Alternative proof: existential quantification over relation symbols of individual theories
+Alternative method:
+  * [[http://lara.epfl.ch/~kuncak/papers/WiesETAL09CombiningTheorieswithSharedSetOperations.html|On Combining Theories with Shared Set Operations]]
-===== Complexity =====
-  * if each theory is convex and polynomial time (e.g. congruence closure + real linear arithmetic), then conjunctions can be decided in PTIME
-  * if each theory is NP (e.g. we also allow integer linear programming), then (even for non-convex theories), any quantifier-free combination is in NP
 ===== References =====