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.
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).
(based on SMT-LIB parser 2.0
by Mike Decoster and Michael Schidlowsky)
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:
extlibsand copy the file
maketo compile iPrincess.
If everything went ok, it is possible to run iPrincess with the