Princess Web Interface

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.

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

Send given input to Princess
Save input on the server and make it available through a private link
Enable incremental SMT-LIB processing
Output models/ countermodels
Search for most-general constraints satisfying a formula
Pretty-print proof for valid/unsatisfiable problems