Princess
Theorem Proving in First-Order Logic modulo Linear Integer
Arithmetic
Princess is a theorem prover for Presburger arithmetic with
uninterpreted predicates. This means that Princess can reason about
problems in integer arithmetic without multiplication (only
multiplication with integer literals is allowed), augmented with
predicates that can be axiomatised arbitrarily. Such problems can
contain arbitrary quantifiers to express that some formula is supposed
to hold for all or for some integers. Some further features of Princess
include:
- Princess is a decision procedure for formulae in Presburger
arithmetic (without uninterpreted predicates) and can eliminate
quantifiers
- Handling of (partial and total) functions via an encoding into
uninterpreted predicates
- Extraction of Craig interpolants for valid formulae (with some
restrictions on the use of quantifiers)
- Triggers and e-matching for user-guided handling of quantified
formulae, similar as in SMT solvers
- Handling of the theory of arrays via user-specified axioms
- Princess can read problems in its own native format, or in the SMT-LIB
2 format
| You
can
run
Princess
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. |
Princess is free software and distributed under GPL v3.
Authors
Documentation and Publications
- Definition of the Princess
syntax. Examples are included in the Princess
distributions, and on the examples
page
- LPAR paper about the
calculus that is used in Princess
- A more detailed
description
of the calculus and Princess is part of my PhD thesis
- IJCAR paper on
interpolant generation in Presburger arithmetic
- VERIFY and VMCAI papers on
interpolant generation in the presence of uninterpreted predicates,
functions, and arrays
- LPAR paper about
e-matching
and the handling of functions in Princess
- Talk about Princess that I
gave at
Microsoft Research Redmond.
- Talk about E-Matching in
Princess
that I gave at the wintermeeting of the SET division at Chalmers
University
- The native input format of Princess 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.
- There is also a converter
(based on SMT-LIB parser 2.0 by Mike Decoster and Michael Schidlowsky)
from the SMT-LIB 1 format to the Princess format. Note that Princess is
by now able to directly read problems in the SMT-LIB 2 format.
Installation of the binary
distribution
We provide a binary
distribution of the latest version of Princess. This distribution
contains all required libraries, i.e., the Scala API and the Cup parser
generator library; it is only necessary to have a Java runtime
environment
(version 1.5 or newer) installed.
To install, just
download the archive and unpack it in some directory of your choice.
The Princess gui can then be invoked using the script princessGui,
the
command
line
tool
using
the
script
princess.
Compilation, Installation from
source
The compilation is so far only tested on Linux systems. For the
installation,
you need:
The actual installation consists of the following steps:
- Unpack one of the snapshots
(preferably the newest one) and
change to the
princess-* 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 Princess.
If everything went ok, it is possible to run Princess with the
command ./princess <inputfile>