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:a_simple_sound_combination_method [2009/05/12 22:41] vkuncak |
sav08:a_simple_sound_combination_method [2009/05/12 22:52] vkuncak |
||
---|---|---|---|
Line 16: | Line 16: | ||
Improvement of precision: if $F$ is equivalent to disjunction $\vee_{j=1}^m D_j$ then to prove $F$ unsatisfiable, for each $1 \le j \le m$ check that $D_j$ is unsatisfiable by applying each of the provers. | Improvement of precision: if $F$ is equivalent to disjunction $\vee_{j=1}^m D_j$ then to prove $F$ unsatisfiable, for each $1 \le j \le m$ check that $D_j$ is unsatisfiable by applying each of the provers. | ||
- | |||
- | In particular, we may transform $F$ into [[Atomic Diagram Normal Form]]. | ||
===== Examples ===== | ===== Examples ===== | ||
Line 56: | 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. |