Features | ## Interpolation and Symbol EliminationNote: special thanks are to Laura Kovacs who contributed both to the work described in this page and the page content.Vampire implements two new features: Both features have been implemented using ## InterpolationIn the original definition of Craig, an interpolant of two formulas L and R is any formula I such that - both ⊨ L ⊃ I and ⊨ I ⊃ R (that is, I is implied by L and implies R).
- 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: - symbols colored in left may only occur in L;
- symbols colored in right may only occur in R;
- all symbols occurring in the theory are transparent
We call an interpolant of L and R any formula I such that - both ⊨
_{T}L ⊃ I and ⊨_{T}I ⊃ R. - 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 - both ⊨
_{T}L ⊃ I and ⊨_{T}I & R ⊃ ⊥. - 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: - symbol colors
- which part of the input relates respectively to L, R, and the theory T.
## Example 1The 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. `% request to generate an interpolant` Vampire outputs the following: `17. $false (2:0) [resolution 16,5]` 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: `fof(fA,axiom, q(f(a)) & ~q(f(b)) ).` `10. $false (0:0) [subsumption resolution 9,8]` ## Example 2This example uses a theory: a simple axiomatisation of arithmetic with the greater-than
relation `% request to generate an interpolant` Vampire generates the following interpolant. `(~greater(p,q) | ~greater(p,q)) & (~greater(p,q) | ~greater(p,q)) & (~greater(p,q) | ~greater(p,q)) & (~greater(p,q) | ~greater(p,q)) & (greater(q,p) | s(zero) = f(p)) & (~greater(p,q) | ~greater(p,q)) & (~greater(p,q) | ~greater(p,q)) & (~greater(p,q) | ~greater(p,q)) & (~greater(p,q) | ~greater(p,q)) & (greater(q,p) | s(zero) = f(p)) & (~greater(p,q) | ~greater(p,q)) & (~greater(p,q) | ~greater(p,q)) & (~greater(p,q) | ~greater(p,q)) & (~greater(p,q) | ~greater(p,q)) & (greater(q,p) | s(zero) = f(p))` This interpolant is equivalent to the formula q ≥ p & f(p)=1. ## More ExamplesMore 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 EliminationSymbol elimination can be used to generate loop invariants automatically, as described in paper [1]. The idea of invariant generation is as follows. - 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.
- 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 ExamplesMore 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. |