Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:a_simple_sound_combination_method [2009/05/13 10:38] vkuncak |
sav08:a_simple_sound_combination_method [2009/05/13 11:25] 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. | ||
+ | |||
===== Defining Approximations ===== | ===== Defining Approximations ===== | ||
Line 31: | Line 32: | ||
$\alpha^p(\forall x.F) = \forall x. \alpha^p(F)$ | $\alpha^p(\forall x.F) = \forall x. \alpha^p(F)$ | ||
- | $\alpha^p(\exists x.F) = \forall x. \alpha^p(F)$ | + | $\alpha^p(\exists x.F) = \exists x. \alpha^p(F)$ |
$\alpha^p(A) = A$ for any supported atomic formula | $\alpha^p(A) = A$ for any supported atomic formula |