Interpolation and Symbol Elimination

Vampire implements two new features: interpolation and symbol elimination described in the following papers.

Both features have been implemented using colored symbols and colored formulas, explained below.

Interpolation

In the original definition of Craig, an interpolant of two formulas L and R is any formula I such that

1. both ⊨ L ⊃ I and ⊨ I ⊃ R (that is, I is implied by L and implies R).
2. Every symbol occurring in I also occurs both in L and R.

Craig proved that, if R is implied by L, then such an interpolant exists.

However, for applications in verification and invariant generation this definition is too restrictive. Firstly, we are normally interested in reasoning modulo a theory T (for simplicity we assume that a theory any set of formulas). Secondly, we may allow theory symbols and some other symbols occur in the interpolant.

We capture this more general notion of interpolant by using logical consequence modulo theory and by coloring symbols. We assume to have two colors, the left and the right color. Some symbols may be colored in left and some in right (but not in both), and some symbols may be transparent, that is, have no color. We assume the following properties:

1. symbols colored in left may only occur in L;
2. symbols colored in right may only occur in R;
3. all symbols occurring in the theory are transparent

We call an interpolant of L and R any formula I such that

1. both ⊨_T L ⊃ I and ⊨_T I ⊃ R.
2. I is transparent, that is, consists only of transparent symbols.

It is easy to see that an interpolant in the sense of Craig is captured by this definition: to this end make the theory empty, color all symbols occurring in L in left and all symbols occurring in R in right.

There is a similar notion of reverse interpolant of L: it is any formula I such that

1. both ⊨_T L ⊃ I and ⊨_T I & R ⊃ ⊥.
2. I is transparent, that is, consists only of transparent symbols.

Closely related to our definitions is a concept of a well-colored derivation: this is a derivation in which no inference contains clauses of both colors. Paper [2] gives an algorithm for building an interpolant of L and R from a well-colored proof of L ⊃ R. Vampire implements well-colored proofs and generation of interpolants from such proofs.

To make Vampire generate a well-colored proof and compute an interpolant we should be able to define the following:

1. symbol colors
2. which part of the input relates respectively to L, R, and the theory T.

Example 1

The following examples shows how we can request Vampire generate well-colored proofs and interpolants using Vampire-specific extensions to the TPTP syntax. In this example we ask Vampire to generate an interpolant for q(f(a)) & ¬q(f(b)) ⊃ ∃v(v ≠ c). We use TPTP comments (beginning with the symbol "%") to explain the input.

Vampire outputs the following:

That is, it finds the interpolant ¬∀x∀y(x=y). Note that if we remove color declarations from the input, then Vampire will generate a different refutation:

Example 2

This example uses a theory: a simple axiomatisation of arithmetic with the greater-than relation greater and successor function s. Essentially, in this example L is q ≥ c ≥ p & f(c)=1 and R is p ≥ d ≥ q & f(d)=0

Vampire generates the following interpolant.

This interpolant is equivalent to the formula q ≥ p & f(p)=1.

More Examples

More examples on computing interpolants with Vampire can be found here. Each example is given in the TPTP syntax, and hence can be immediately fed into Vampire.

Symbol Elimination

Symbol elimination can be used to generate loop invariants automatically, as described in paper [1]. The idea of invariant generation is as follows.

1. We generate loop properties using a language that contains program variables and some additional symbols. These symbols are required to express loop properties that are not expressible using loop variables. For example, we may introduce the loop counter as an additional constant.
2. We run a saturation theorem prover to eliminate the extra symbols. That is, the prover should generate consequences of the initial formulas not containing extra symbols. These consequences are loop invariants.

To make Vampire eliminate symbols, we run it in the symbol-eliminating mode. We declare the symbols to be eliminated colored. For the purpose of symbol elimination, a single color is sufficient. Here is an example showing how to make Vampire eliminate symbols.

More Examples

More examples on symbol elimination with Vampire can be found here. For each example, we list its source code (in C), its encoding in TPTP, the obtained set of symbol eliminating inferences, and a minimised set of symbol eliminating inferences.