Princess Web Interface

Princess is a theorem prover developed and maintained by Uppsala University and the University of Regensburg.
Princess accepts input in its own format, in SMT-LIB format, or in TPTP.
It optionally uses OSTRICH to solve string constraints written using a superset of a subset of the new SMT-LIB string theory.

Load a predefined example: adts1 bv-equation bv-interpolation1 bv-interpolation2 bv-interpolation3 bv-interpolation4 interpolation1 modulo palindrome quantifiers1 quantifiers2 template bv-interpolation-1 bv-interpolation-2 bv-interpolation-3 datatype1 datatype2 datatype3 finite-field-2 incremental interpolation1 quantifier-elimination-2 quantifier-elimination simple concat regex-parsing replace-1 replaceall-1 replaceall-2 replaceall-regex-1 successor-OSTRICH successor-seq to-uppercase tree-of-strings GEG021=1 ex:1 ex:10 ex:2 ex:3 ex:5 ex:6 ex:7a ex:7b ex:8 ex:P1 ex:P2 ... or enter some formulas: