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:
- atomic propositions in propositional logic:
- predicate symbols:
- constant symbols:
- function symbols:
- variable symbols:
- false/bottom is written
- true/top is written
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.