Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:combining_fol_models [2009/05/13 00:09] vkuncak |
sav08:combining_fol_models [2009/05/13 10:48] vkuncak |
||
|---|---|---|---|
| Line 4: | Line 4: | ||
| ===== Merging Models of Theories with Disjoint Languages (Signatures) ===== | ===== 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 89: | Line 89: | ||
| * [[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. | * [[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 ===== | ===== Theories with Non-Disjoint Languages ===== | ||
| Line 103: | Line 107: | ||
| Alternative method: | Alternative method: | ||
| * [[http://lara.epfl.ch/~kuncak/papers/WiesETAL09CombiningTheorieswithSharedSetOperations.html|On Combining Theories with Shared Set Operations]] | * [[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 ===== | ===== References ===== | ||