LARA

Differences

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

Link to this comparison view

sav08:a_simple_sound_combination_method [2009/05/13 10:38]
vkuncak
sav08:a_simple_sound_combination_method [2015/04/21 17:30]
Line 1: Line 1:
-====== A Simple Sound Combination Method ====== 
  
-The following method need not be complete, but applies to any formulas, not just quantifier-free formulas. 
- 
-Suppose we wish to unsatisfiability of a class of formulas ${\cal F}$ and we have provers $P_i$ which can prove formulas in language ${\cal L}_i$ for $1 \le i \le n$. 
- 
-Suppose each prover has approximation function $\alpha_i : {\cal F} \to {\cal F}_i$ such that  
-  * $\alpha_i(F) \in {\cal L}_i$ 
-  * $F \models \alpha_i(F)$ 
-In other words, $\alpha_i$ approximates an arbitrary formula with a weaker formula in language understood by $P_i$. 
- 
- 
-To prove formula $F$, for each $i$, apply $P_i$ to check satisfiability of $\alpha_i(F)$.  ​ 
-  * If any of the provers concludes that formula is unsatisfiable,​ then $F$ is unsatisfiable (soundness) 
-  * If no prover finds unsatisfiability,​ we cannot say much in general, depending on the approximation functions 
- 
-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 ===== 
- 
-We can define approximation for arbitrary first-order formulas. 
- 
-Start with $\alpha^1$, flip on negation. 
- 
-$\alpha^p(F_1 \land F_2) = \alpha^p(F_1) \land \alpha^p(F_2)$ 
- 
-$\alpha^p(F_1 \lor F_2) = \alpha^p(F_1) \lor \alpha^p(F_2)$ 
- 
-$\alpha^p(\lnot F) = \lnot \alpha^{1-p}(F)$ 
- 
-$\alpha^p(\forall x.F) = \forall x. \alpha^p(F)$ 
- 
-$\alpha^p(\exists x.F) = \forall x. \alpha^p(F)$ 
- 
-$\alpha^p(A) = A$ for any supported atomic formula 
- 
-$\alpha^1(A) = true$ for unsupported atomic formula 
- 
-$\alpha^0(A) = false$ for unsupported atomic formula 
- 
-**Lemma:** $\alpha^0(F) \models F \models \alpha^1(F)$ 
- 
-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 
-\[ 
-    1 \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: 
-\[ 
-   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) 
-\] 
-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''​$ 
-\[ 
-   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 
-\] 
-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. 
- 
-===== References ===== 
- 
-  * [[http://​lara.epfl.ch/​~kuncak/​papers/​ZeeETAL08FullFunctionalVerificationofLinkedDataStructures.html|Full Functional Verification of Linked Data Structures]]