Princess is a theorem prover (aka SMT Solver) for Presburger arithmetic with uninterpreted predicates, written entirely in Scala. Princess can reason about problems in integer arithmetic, 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.
Main features of Princess include:
Princess runs on any platform that provides a Java runtime environment (version 1.5 or higher). There is a 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 runner-up in the overall TFA division. We currently maintain a separate branch for full support of the TPTP format.
Princess is free software. Since version 2015-12-07, Princess is distributed under LGPL v2.1 or later; older versions were licenced under LGPL v3, and even earlier under GPL v3.
Please contact me if you are interested in any projects or thesis work related to Princess.
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
princess. In addition, the script
can be used to run Princess in client-server mode
If you want to use
the Princess API, it is
easiest to start from the class
ap.SimpleAPI, and use the
to construct formulae. A number of examples are included in both the
source and binary distributions, in
We maintain a Maven repository with the latest Princess binaries,
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" % "2017-07-17"
You can download a
complete hello-world project
here. The example can be compiled
using sbt. If you have sbt
installed, just calling
sbt run in
hw should take care of downloading Princess,
and all other dependencies, compilation, and running the example.
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:
+multiStrategy, with a portfolio of strategies optimised for TPTP problems;
+printProofcan be added.
sbt runin order to compile Princess and run it
sbt assemblyto create a standalone jar file that you can run with
java -jar target/scala-2.XX/Princess-assembly-XX.jar.
sbt assembly, you can also use the
princessClient to invoke Princess through the jar file.
The compilation is so far only tested on Linux systems. For the installation, using the make tool, you need:
The actual installation consists of the following steps:
extlibsand copy the file
maketo compile Princess.
If everything went ok, it is possible to run Princess with the
A list of the Princess options can be printed using