Differences
This shows you the differences between two versions of the page.
| Next revision Both sides next revision | |||
|
sav08:idea_of_quantifier-free_combination [2008/04/23 10:13] vkuncak created |
sav08:idea_of_quantifier-free_combination [2008/04/23 15:41] vkuncak |
||
|---|---|---|---|
| Line 16: | Line 16: | ||
| The idea is to separate conjuncts into those specific to individual theories, and then solve them using specialized decision procedures. | The idea is to separate conjuncts into those specific to individual theories, and then solve them using specialized decision procedures. | ||
| - | An important question is completeness: if each $C_i$ is satisfiable, is $C_1 \land \ldots C_n$ satisfiable? We will show that, under certain conditions, this holds. | + | An important question is completeness: if each $C_i$ is satisfiable, is $C_1 \land \ldots \land C_n$ satisfiable? We will show that, under certain conditions, this holds. |