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: p, q, r
• predicate symbols: P, Q, R
• constant symbols: a, b, c
• function symbols: f, g, h
• variable symbols: x, y, z, u, v
• false/bottom is written bottom
• true/top is written top

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.