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.



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).

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)


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:

The actual installation consists of the following steps:

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

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