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:a_simple_sound_combination_method [2009/05/12 22:50] vkuncak |
sav08:a_simple_sound_combination_method [2009/05/12 22:52] vkuncak |
||
|---|---|---|---|
| Line 54: | Line 54: | ||
| * doing case analysis on equality of variables | * doing case analysis on equality of variables | ||
| These are the key techniques that we use in methods that are complete for quantifier-free combinations of procedures that reason about disjoint function and predicate symbols. | These are the key techniques that we use in methods that are complete for quantifier-free combinations of procedures that reason about disjoint function and predicate symbols. | ||
| + | |||
| ===== Defining Approximations ===== | ===== Defining Approximations ===== | ||
| + | |||
| + | We can define approximation for arbitrary first-order formulas. | ||
| Start with $\alpha^1$, flip on negation. | Start with $\alpha^1$, flip on negation. | ||