iPrincess

An interpolating theorem prover for quantifier-free Presburger Arithmetic

iPrincess is an interpolating theorem prover for Presburger arithmetic with uninterpreted predicates. The tool is able to prove or disprove the validity of formulae in this logic and, in case a formula is found to be valid, iPrincess is able to generate Craig interpolants for any two partitions of the formula.

The implementation is based on Princess which has been extended to generate proofs of validity. Our new algorithm recursively visits the proof and generates an interpolant using the rules presented in this paper.

You can run iPrincess using Java Webstart, provided that you have a Java runtime environment (version 1.5 or newer) and Webstart installed on your computer. Java Webstart is usually included in JREs. For example problems to be proven, see the source distributions below.

iPrincess is free software and distributed under GPL v3.

Documentation

IJCAR'10 paper about interpolation in quantifier-free Presburger arithmetic, as done in iPrincess.
VERIFY-2010 paper about interpolation in the theory of arrays.
The Princess examples explain the input format accepted by iPrincess.
The input format of iPrincess much resembles the format that is used by the KeY tool. You can have a look at the example files that are included in the distributions below.

Authors

Some Benchmarks (May 2010)

The following results compare interpolation runtimes of iPrincess and Quantifier Elimination. Diagrams and a discussion of the benchmarks are given in our IJCAR paper. The benchmarks were run on an Intel Pentium Xeon with 3 GHz, using a timeout of 120s. The interpolation problems are derived from the QF_LIA category of SMT-LIB (quantifier-free formulae over linear integer arithmetic).

QF_LIA
Directory	Results	Directory	Results
CIRC	results	mathsat	results
check	results	rings	results

SMT-LIB converter (based on SMT-LIB parser 2.0
by Mike Decoster and Michael Schidlowsky)

Snapshots

31/08/2010: The functionality of iPrincess has been backported and integrated into the standard Princess version; we do not plan to separately continue development on iPrincess.
27/05/2010: Updated version with many optimisations and fixes. The calculus has been extended to support interpolation in quantifier-free Presburger arithmetic with uninterpreted predicates, which also makes it possible to handle uninterpreted functions and the theory of arrays. More details are given in a paper at the VERIFY-2010 workshop.
24/01/2010: First official release of iPrincess

Compilation, Installation of the Commandline Tool

We recommend to use Princess instead of the older versions of iPrincess on this page. As of August 2010, all functionality of iPrincess is also available in Princess.

The compilation is so far only tested on Linux systems. For the installation, you need:

A compiler for Scala version 2.7
A Java SDK version 1.5 or newer
The Cup parser generator for Java (get the file java-cup-11a.jar)
If you want to compile the parser yourself (binaries are included in the iPrincess snapshots below), you also need the BNF converter and JLex.

The actual installation consists of the following steps:

Unpack one of the snapshots below (preferably the newest one) and change to the iprincess-* directory
Create a directory extlibs and copy the file java-cup-11a.jar into it
In case you want to compile the parser yourself (not necessary), run make parser-jar
Run make to compile iPrincess.

If everything went ok, it is possible to run iPrincess with the command ./princess <inputfile>