Princess
Theorem Proving in FirstOrder 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. Features of Princess
include:
 Decision + quantifier elimination procedure for
Presburger arithmetic
 Support for uninterpreted predicates and
partial or total functions
 Theory modules for nonlinear integer arithmetic
(diophantine) and the theory of arrays
 Support for Craig interpolation
 Free variable calculus, to handle
quantifiers and extract solutions of formulae
 Triggers and ematching for userguided handling of quantified
formulae, similar as in SMT solvers
 Problem input in the native language of Princess, in the SMTLIB
2 format, and in the FOF/TFF/CNF dialects of TPTP
(see details).

Written in Scala, and runs on any platform
that provides a Java runtime environment (version 1.5 or higher)

Convenient API for programmatic use from Scala applications.
This API can also be used to integrate Princess in Java applications,
although this is somewhat less convenient (for instance see the
wrapper used in Bixie, or the JavaSMT library)
Princess won
the TFA division (arithmetic problems) at CASC J6, 2012.
In 2013 and 2014, Princess won in the TFI category of CASC,
(integer problems), and was runnerup in the overall TFA division.
We currently maintain a separate branch for full support of the
TPTP format.
Princess is free software. Since version 20151207,
Princess is distributed under
LGPL v2.1 or later; older
versions were licenced under LGPL v3, and even earlier under GPL v3. The latest
release is 20161226.
Please contact me if you are interested in
any projects or thesis work
related to Princess.
Documentation and Publications
 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
ematching
and the handling of functions in Princess
 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.
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
. In addition, the script princessClient
can be used to run Princess in clientserver mode
(more details).
Using Princess as a Scala Library
If you want to use
the Princess API, it is
easiest to start from the class
ap.SimpleAPI, and use the
functions in
ap.parser.IExpression
to construct formulae. A number of examples are included in both the
source and binary distributions, in
directory testcases/api
.
We maintain a Maven repository with the latest Princess binaries,
with URL
http://logicrunch.it.uu.se:4096/~wv/maven/
and organisation id
uuverifiers
. If you build your software
using sbt, you can simply
add the following two lines in the build.sbt
script to
automatically download Princess during compilation:
resolvers += "uuverifiers" at "http://logicrunch.it.uu.se:4096/~wv/maven/"
libraryDependencies += "uuverifiers" %% "princess" % "20161226"
You can download a
complete helloworld project
here. The example can be compiled
using sbt. If you have sbt
installed, just calling sbt run
in
directory hw
should take care of downloading Princess,
and all other dependencies, compilation, and running the example.
Installation of the binary
CASC/TPTP distribution
We currently maintain a separate branch for full support of the
TPTP format. You can
download a binary of the latest version, or the
sources.
This version
differs from normal Princess mainly in the following points:
 the default input format is chosen to be TPTP;
 by default, the prover runs with the option
+multiStrategy
,
with
a
portfolio
of
strategies
optimised
for
TPTP
problems;
 the
semantics
of
uninterpreted
sorts is different from
the semantics assumed by standard Princess: in the standard version,
uninterpreted sorts are always considered to be infinite (since
they are internally mapped to the datatype of integers), whereas in
the CASC version type guards are generated to correctly model
also finite domains;
 results are output in the SZS
notation;

to generate and output proofs, the option
+printProof
can be added.
The Royal Family
More recently, some siblings of Princess have appeared as well:
 ePrincess,
a variant of Princess that uses Bounded Rigid EUnification
for closing branches.
 iPrincess (now defunct),
which added support for Craig interpolation to Princess. This functionality
is now integrated in the main Princess branch.
Compilation and 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 javacup11a.jar
into it
 In case you want to compile the parser yourself (not necessary),
run
make parserjar
 Run
make
to compile Princess.
If everything went ok, it is possible to run Princess with the
command ./princess <inputfile>
A list of the Princess options can be printed using ./princess h
Applications
Here is a (probably incomplete) list of applications of Princess
that I am aware of. I am interested in learning about further
situations where Princess was found to be useful, so in case you
have one feel free to drop me a mail!
 JavaSMT,
a unifying Java interface for SMT solvers
 Seneschal, a ranking function generator for bitvector relations
 Eldarica, a predicate abstractionbased
model checker
 Joogie,
Gravy, and
Bixie, tools for detecting inconsistent and
infeasible code in Java applications
 JayHorn, a Java model checker
 Picasso, a static analyzer for depthbounded systems
Funding
The development of Princess has been supported by:

The Microsoft Research PhD Grant "FirstOrder
Satisfiability Modulo Theories"
(20132016)

The Swedish Research Council grant 20145484
"Satisfiability Modulo Theories and Quantifiers"
(20152018)