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:21] vkuncak |
||
|---|---|---|---|
| Line 88: | Line 88: | ||
| 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 102: | ||
| 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 ===== | ||