Playground

You can try out Naproche in your browser with the Naproche web interface. You can load examples or write your own formalizations there and have Naproche check them for you. The choice of automated prover is between SPASS running locally in your browser or a remote prover at System on TPTP (such as E or Vampire). Running provers remotely may add a bit of delay, but these provers can solve more demanding tasks than the local instance of SPASS.