Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:a_simple_sound_combination_method [2009/05/12 22:52] vkuncak |
sav08:a_simple_sound_combination_method [2009/05/13 10:38] vkuncak |
||
|---|---|---|---|
| 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 ===== | ||
| + | |||
| + | 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 ===== | ===== Examples ===== | ||
| Line 54: | Line 80: | ||
| * doing case analysis on equality of variables | * 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. | 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. | ||
| - | |||
| - | |||
| - | ===== 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? | ||
| ===== References ===== | ===== References ===== | ||
| * [[http://lara.epfl.ch/~kuncak/papers/ZeeETAL08FullFunctionalVerificationofLinkedDataStructures.html|Full Functional Verification of Linked Data Structures]] | * [[http://lara.epfl.ch/~kuncak/papers/ZeeETAL08FullFunctionalVerificationofLinkedDataStructures.html|Full Functional Verification of Linked Data Structures]] | ||