Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:a_simple_sound_combination_method [2009/05/13 10:38]
vkuncak
sav08:a_simple_sound_combination_method [2015/04/21 17:30] (current)
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
Line 48: Line 49:
  
 **Example** (from [[Calculus of Computation Textbook]], page 210, Example 10.1): Let $F$ be **Example** (from [[Calculus of Computation Textbook]], page 210, Example 10.1): Let $F$ be
-\[+\begin{equation*}
     1 \le x \land x \le 2 \land f(x) \neq f(1) \land f(x) \neq f(2)     1 \le x \land x \le 2 \land f(x) \neq f(1) \land f(x) \neq f(2)
-\]+\end{equation*}
 This formula is unsatisfiable. ​ However, This formula is unsatisfiable. ​ However,
-\[+\begin{equation*}
    ​\alpha_U(F) = true    ​\alpha_U(F) = true
-\] +\end{equation*} 
-\[+\begin{equation*}
    ​\alpha_A(F) = 1 \le x \land x \le 2    ​\alpha_A(F) = 1 \le x \land x \le 2
-\]+\end{equation*}
 and both approximations are satisfiable in resulting theories. and both approximations are satisfiable in resulting theories.
  
 Instead of doing approximation directly, let us transform the original formula into formula $F'$ where function application and arithmetic are separated: Instead of doing approximation directly, let us transform the original formula into formula $F'$ where function application and arithmetic are separated:
-\[+\begin{equation*}
    1 \le x \land x \le 2 \land y_1=1 \land f(x) \neq f(y_1) \land y_2=2 \land f(x) \neq f(y_2)    1 \le x \land x \le 2 \land y_1=1 \land f(x) \neq f(y_1) \land y_2=2 \land f(x) \neq f(y_2)
-\]+\end{equation*}
 Variables $x$ and $y_1$ both appear in the formula, so let us convert $F'$ into disjunction of $(F' \land x=y_1) \lor (F' \land x \neq y_1)$. ​ We then check satisfiability for each of the disjuncts. ​ Consider, for example, $F' \land x = y_1$, which is formula $F''​$ Variables $x$ and $y_1$ both appear in the formula, so let us convert $F'$ into disjunction of $(F' \land x=y_1) \lor (F' \land x \neq y_1)$. ​ We then check satisfiability for each of the disjuncts. ​ Consider, for example, $F' \land x = y_1$, which is formula $F''​$
-\[+\begin{equation*}
    1 \le x \land x \le 2 \land y_1=1 \land f(x) \neq f(y_1) \land y_2=2 \land f(x) \neq f(y_2) \land x = y_1    1 \le x \land x \le 2 \land y_1=1 \land f(x) \neq f(y_1) \land y_2=2 \land f(x) \neq f(y_2) \land x = y_1
-\]+\end{equation*}
 We have We have
-\[+\begin{equation*}
    ​\alpha_U(F''​) = f(x) \neq f(y_1) \land f(x) \neq f(y_2) \land x=y_1    ​\alpha_U(F''​) = f(x) \neq f(y_1) \land f(x) \neq f(y_2) \land x=y_1
-\]+\end{equation*}
 which is unsatisfiable. ​ Then, considering formula $F' \land x=y_1$, we can do further case analysis on equality of two variables, say $x=y_2$. ​ For $F' \land x \neq y_1 \land x = y_2$ we similarly obtain unsatisfiability of $\alpha_U$-approximation. ​ The remaining case is $F' \land x \neq y_1 \land x \neq y_2$.  For this formula, denoted $F'''​$,​ we have which is unsatisfiable. ​ Then, considering formula $F' \land x=y_1$, we can do further case analysis on equality of two variables, say $x=y_2$. ​ For $F' \land x \neq y_1 \land x = y_2$ we similarly obtain unsatisfiability of $\alpha_U$-approximation. ​ The remaining case is $F' \land x \neq y_1 \land x \neq y_2$.  For this formula, denoted $F'''​$,​ we have
-\[+\begin{equation*}
    ​\alpha_A(F'''​) = 1 \le x \land x \le 2 \land y_1=1 \land y_2=2 \land x \neq y_1 \land x \neq y_2    ​\alpha_A(F'''​) = 1 \le x \land x \le 2 \land y_1=1 \land y_2=2 \land x \neq y_1 \land x \neq y_2
-\]+\end{equation*}
 which is unsatisfiable. ​ Therefore, by transforming formula into disjunction of formulas, we were able to prove unsatisfiability. ​ Two things helped precision which is unsatisfiable. ​ Therefore, by transforming formula into disjunction of formulas, we were able to prove unsatisfiability. ​ Two things helped precision
   * separating literals into literals understood by individual theories (unlike mixed literals $f(x) \neq f(1)$)   * separating literals into literals understood by individual theories (unlike mixed literals $f(x) \neq f(1)$)
 
sav08/a_simple_sound_combination_method.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice