LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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