Skip to content

Latest commit

 

History

History
14 lines (12 loc) · 710 Bytes

README.md

File metadata and controls

14 lines (12 loc) · 710 Bytes

The Princess Theorem Prover

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.

More information about Princess can be found on the main webpage, https://philipp.ruemmer.org/princess.shtml