Differences
This shows you the differences between two versions of the page.
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)$) |