LARA

Interpolation

Interpolation is one of the main methods to find predicates in predicate abstraction, and, more generally, to perform counterexample-based refinement of abstractions.

Definition of Interpolant: Given two formulas $F$ and $G$, such that $\models F \rightarrow G$, an interpolant for $(F,G)$ is a formula $H$ such that:
1) $\models F \rightarrow H$
2) $\models H \rightarrow G$
3) $FV(H)\subseteq FV(F) \cap FV(G)$

Paper on Interpolation in Verification

Here are two simple ways to construct an interpolant:

  • We can quantify existentially all variables in $F$ that are not in $G$.

$H_{min} \equiv elim(\exists p_1, p_2, ..., p_n.\ F)$ where $\{p_1, p_2, ..., p_n \}\ = FV(F)\backslash FV(G)$

  • We can quantify universally all variables in $G$ that are not in $F$.

$H_{max} \equiv elim(\forall q_1, q_2, ..., q_m.\ G)$ where $\{q_1, q_2, ..., q_m \}\ = FV(G)\backslash FV(F)$

Definition: ${\cal I}(F,G)$ denote the set of all interpolants for $(F,G)$, that is,

\begin{equation*} {\cal I}(F,G) = \{ H \mid H \mbox{ is interpolant for $(F,G)$ \} \end{equation*}

Theorem: The following properties hold for $H_{min}$, $H_{max}$, ${\cal I}(F,G)$ defined above:

  1. $H_{min} \in {\cal I}(F,G)$
  2. $\forall H \in {\cal I}(F,G).\ \models (H_{min} \rightarrow H)$
  3. $H_{max} \in {\cal I}(F,G)$
  4. $\forall H \in {\cal I}(F,G).\ \models (H \rightarrow H_{max})$

We have observed before that, if a theory has quantifier elimination, then it also has interpolants.

Therefore, all theories in the List of Theories Admitting QE have interpolants. (But interpolants may exist even if there is no quantifier elimination.)

Interpolants from Resolution Proofs

Interpolants in resolution: instead of validity of implication, we look at unsatisfiability.

Let $A$, $B$ be sets of clauses such that $A \land B$ is not satisfiable. An interpolant is a formula $H$ such that

  • $\models (A \rightarrow H)$ and $H \land B$ is not satisfiable and
  • $FV(H) \subseteq FV(A) \cap FV(B)$

Construct resolution tree that derives a contradiction from $A \cup B$. The tree has elements of $A \cup B$ as leaves and results of application of resolution as nodes. For each clause $C$ in resolution tree we define recursively formula $I(C)$ and show that $I(C)$ is interpolant for these two formulas:

  • $A \land ((\lnot C)|_A)$
  • $B \land ((\lnot C)|_B)$

where $(\lnot C)|_A$ denotes the conjunction of those literals from $C$ whose propositional variables belong to $FV(A)$, similarly for $(\lnot C)|_B$.

It follows that for empty clause the $I(\emptyset)$ is the interpolant for $(A,B)$.

Construction of $I(C)$:

  • if $C \in A \cup B$ then
    • if $C \in A$ then $I(C) = {\it false}$
    • if $C \in B$ then $I(C) = {\it true}$
  • if $C$ is result of applying resolution to $C_1$, $C_2$ along propositional variable $q$ where $\lnot q \in C_1$, and $q \in C_2$, then
    • if $q \in FV(A) \setminus FV(B)$ then $I(C) = I(C_1) \lor I(C_2)$
    • if $q \in FV(B) \setminus FV(A)$ then $I(C) = I(C_1) \land I(C_2)$
    • if $q \in FV(A) \cap FV(B)$ then $I(C) = ite(q,I(C_1),I(C_2))$

We prove that $I(C)$ has the desired property by induction on the structure of the resolution proof tree.

More information in e.g.