Institute for Computer Languages

Compilers and Languages Group

# Vinter: A Vampire-Based Tool for Interpolation

Vinter is a Vampire-based tool for interpolation,
whose aim is to generate minimal interpolants.

Vinter translates arbitraty proofs into interpolating ones (local proofs), extracts interpolants from local
proofs, and minimises interpolants using various measures, such as for example the size of the interpolants or the number of quantifiers used in the interpolants.

Vinter takes an input problem written in either SMT-LIB or TPTP syntax.
Proofs are found using either Z3 or Vampire, solving pseudo-boolean optimisation is delegated to Yices,
while localising proofs and generating minimal interpolants is done by Vampire.

## Source Code

The latest release of Vinter
is: vinter-2012-02-01.tar.gz

Note: To run Vinter, you also need to have the Z3 and Yices executables.

## Benchmarks

See the examples
to try Vinter.

## Publications

Vinter is based
on the technique of playing in the grey area of proofs
to find interpolants minimal with respect to various measures.