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, 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:

Princess is written in Scala, and 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. The latest release is 2016-12-26.

Please contact me if you are interested in any projects or thesis work related to Princess.

Download Binary CASC/TPTP Version Web Interface Java Webstart

Examples

Sources

Benchmarks

Documentation and Publications

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 client-server 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" % "2016-12-26"

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 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 Royal Family

More recently, some siblings of Princess have appeared as well:

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:

  1. Unpack one of the snapshots (preferably the newest one) and change to the princess-* 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 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!

Funding

The development of Princess has been supported by: