-
Notifications
You must be signed in to change notification settings - Fork 1
System Princess
Princess was originally designed and is maintained by Philipp Rümmer. Further contributors are Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, Amanda Stjerna.
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. Princess also contains theory modules for, among others, non-linear arithmetic, rationals, bit-vectors, arrays, heaps, algebraic data-types, strings.
- Proving
- Model finding
Princess can read input in three different formats:
-
SMT-LIB 2.6, supporting EUF, LIA, NIA, LRA, NRA, bit-vectors, arrays, data-types, strings. Beyond the standard, also problems with heaps and sequences can be parsed. Quantifiers are supported.
-
TPTP, supporting CNF, FOF, TFF.
The output notation corresponds to the input format:
-
TPTP, SZS notation.
-
Answers and models in the native Princess format.
Princess can output proofs, and uses proofs internally to compute Craig interpolants, but it does not yet output proofs in a machine-readable format.
We plan to support the Alethe proof format in future versions.
http://www.philipp.ruemmer.org/princess.shtml
Princess is distributed under BSD 3-clause license. Since Princess is implemented in Scala, it runs on any platform with a JVM. The main application area of Princess is program verification. Princess is the underlying SMT solver of the Horn solver Eldarica, and supported by the Java-SMT library.
Maintained
Philipp Rümmer: A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic. LPAR 2008: 274-289. DOI: 10.1007/978-3-540-89439-1_20.