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/12 23:55] vkuncak |
sav08:combining_fol_models [2009/05/13 10:57] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Combining Decision Procedures ===== | ====== Combining Decision Procedures ===== | ||
| + | |||
| ===== 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 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. | 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 ===== | ===== Stable Infiniteness ===== | ||
| Line 88: | Line 93: | ||
| Recent approach - try to propagate candidate equalities (even if they are not implied) | 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. | * [[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 97: | Line 107: | ||
| Proof idea: | Proof idea: | ||
| * FOL has interpolation property | * 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 | * 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 ===== | ===== References ===== | ||