Differences

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

--- sav08:a_simple_sound_combination_method [2009/05/12 22:52]
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.
-===== Examples =====
-Consider decision procedure $P_U$ for uninterpreted symbols and $P_A$ for Presburger arithmetic.  Let approximation $\alpha_U$ convert formula to negation normal form, and then drop all literals that contain arithmetic elements.  Similarly, $\alpha_A$ converts to NNF, then drops all literlas that contain symbols not presented in Presburger arithmetic (e.g. uninterpreted function symbols).
-**Example** (from [[Calculus of Computation Textbook]], page 210, Example 10.1): Let $F$ be
-\[
-\le x \land x \le 2 \land f(x) \neq f(1) \land f(x) \neq f(2)
-\]
-This formula is unsatisfiable.  However,
-\[
-   \alpha_U(F) = true
-\]
-\[
-   \alpha_A(F) = 1 \le x \land x \le 2
-\]
-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:
-\[
-\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)
-\]
-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''$
-\[
-\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
-\]
-We have
-\[
-   \alpha_U(F'') = f(x) \neq f(y_1) \land f(x) \neq f(y_2) \land x=y_1
-\]
-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
-\[
-   \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
-\]
-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)$)
-  * doing case analysis on equality of variables
-These are the key techniques that we use in methods that are complete for quantifier-free combinations of procedures that reason about disjoint function and predicate symbols.
@@ Line 70: / Line 32: @@
 $\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
@@ Line 81: / Line 43: @@
 What does $\alpha^1$ do on a conjunction of flat literals?
+===== Examples =====
+Consider decision procedure $P_U$ for uninterpreted symbols and $P_A$ for Presburger arithmetic.  Let approximation $\alpha_U$ convert formula to negation normal form, and then drop all literals that contain arithmetic elements.  Similarly, $\alpha_A$ converts to NNF, then drops all literlas that contain symbols not presented in Presburger arithmetic (e.g. uninterpreted function symbols).
+**Example** (from [[Calculus of Computation Textbook]], page 210, Example 10.1): Let $F$ be
+\begin{equation*}
+\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,
+\begin{equation*}
+   \alpha_U(F) = true
+\end{equation*}
+\begin{equation*}
+   \alpha_A(F) = 1 \le x \land x \le 2
+\end{equation*}
+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:
+\begin{equation*}
+\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''$
+\begin{equation*}
+\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
+\begin{equation*}
+   \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
+\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
+\end{equation*}
+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)$)
+  * doing case analysis on equality of variables
+These are the key techniques that we use in methods that are complete for quantifier-free combinations of procedures that reason about disjoint function and predicate symbols.
 ===== References =====
   * [[http://lara.epfl.ch/~kuncak/papers/ZeeETAL08FullFunctionalVerificationofLinkedDataStructures.html|Full Functional Verification of Linked Data Structures]]