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:41] vkuncak |
sav08:a_simple_sound_combination_method [2009/05/12 22:50] 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 ===== | ||