• English only

# Differences

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

 sav08:a_simple_sound_combination_method [2009/05/13 10:38]vkuncak sav08:a_simple_sound_combination_method [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2009/05/13 11:25 vkuncak 2009/05/13 10:38 vkuncak 2009/05/12 22:52 vkuncak 2009/05/12 22:50 vkuncak 2009/05/12 22:41 vkuncak 2008/04/28 09:57 thomas.geek 2008/04/28 09:57 thomas.geek 2008/04/24 11:05 vkuncak 2008/04/24 11:04 vkuncak 2008/04/24 11:03 vkuncak 2008/04/24 11:01 vkuncak 2008/04/24 10:59 vkuncak 2008/04/24 10:59 vkuncak 2008/04/24 10:58 vkuncak 2008/04/24 10:57 vkuncak 2008/04/24 10:56 vkuncak 2008/04/24 10:55 vkuncak 2008/04/23 20:44 vkuncak 2008/04/23 20:43 vkuncak 2008/04/23 20:42 vkuncak created Next revision Previous revision 2009/05/13 11:25 vkuncak 2009/05/13 10:38 vkuncak 2009/05/12 22:52 vkuncak 2009/05/12 22:50 vkuncak 2009/05/12 22:41 vkuncak 2008/04/28 09:57 thomas.geek 2008/04/28 09:57 thomas.geek 2008/04/24 11:05 vkuncak 2008/04/24 11:04 vkuncak 2008/04/24 11:03 vkuncak 2008/04/24 11:01 vkuncak 2008/04/24 10:59 vkuncak 2008/04/24 10:59 vkuncak 2008/04/24 10:58 vkuncak 2008/04/24 10:57 vkuncak 2008/04/24 10:56 vkuncak 2008/04/24 10:55 vkuncak 2008/04/23 20:44 vkuncak 2008/04/23 20:43 vkuncak 2008/04/23 20:42 vkuncak created 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