Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:idea_of_quantifier-free_combination [2008/04/23 15:41] vkuncak |
sav08:idea_of_quantifier-free_combination [2008/04/24 13:50] vkuncak |
||
|---|---|---|---|
| Line 14: | Line 14: | ||
| * if one of the $C_i$ is unsatisfiable, then $C$ is unsatisfiable | * if one of the $C_i$ is unsatisfiable, then $C$ is unsatisfiable | ||
| - | 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 each $C_i$ using a specialized decision procedure $P_i$ |
| 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. | 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. | ||