content/tools/sat-smt/princess.md

+++ date = 2025-06-07 draft = false title = 'Princess' subtitle = 'Theorem Prover' links = [ { title = "Homepage", url = "http://www.philipp.ruemmer.org/princess.shtml", icon = 'fa-solid fa-home' }, { title = "Source Code", url = "https://github.com/uuverifiers/princess", icon = 'fa-solid fa-code' }, { title = "Playground", url = "https://eldarica.org/princess/", icon = 'fa-solid fa-gamepad' } ] applications = ['SMT Solver', 'Theorem Prover', 'SAT Solver'] developers = ['Uppsala University'] licenses = ['MIT'] inputs = ['WhyML'] interfaces = ['CLI', 'Why3'] maintenance = ['Actively Maintained']

techniques = ['CDCL']

publications = ['deMoura2008']

+++

Princess is a theorem prover (aka SMT Solver) for Presburger arithmetic with uninterpreted predicates, written entirely in Scala.