Princess Web Interface

Load a predefined example: ... or enter some formulas:

Princess is a theorem prover developed and maintained by Uppsala University. Princess accepts input in its own format, in SMT-LIB format, or in TPTP.


 
Enable incremental SMT-LIB processing
 
Output models/ countermodels
 
Search for most-general constraints satisfying a formula
 
Pretty-print proof for valid/unsatisfiable problems