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 [2008/04/28 09:57] thomas.geek |
sav08:a_simple_sound_combination_method [2009/05/12 22:50] vkuncak |
||
---|---|---|---|
Line 9: | Line 9: | ||
* $F \models \alpha_i(F)$ | * $F \models \alpha_i(F)$ | ||
In other words, $\alpha_i$ approximates an arbitrary formula with a weaker formula in language understood by $P_i$. | In other words, $\alpha_i$ approximates an arbitrary formula with a weaker formula in language understood by $P_i$. | ||
- | FIXME: insert diagram | + | |
To prove formula $F$, for each $i$, apply $P_i$ to check satisfiability of $\alpha_i(F)$. | To prove formula $F$, for each $i$, apply $P_i$ to check satisfiability of $\alpha_i(F)$. | ||
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 ===== |