Code available here

Pravda - the pedagogical prover of ENS Rennes - exercices in proof systems

Humanity is in danger! We need you to save the world. For this mission, you need to provide proofs in formal logic. We will consider propositional logic and first-order logic. The syntax uses is: Formal proofs are written one formula/sequent per line. Then the system checks whether you wrote a correct axiom or whether you correctly applied one of the rules. Please choose below the proof system you want to use.