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.

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. Warning: this will lead to certain quantifiers being ignored, and destroys completeness