Code available on gitlab Inria

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.

Resolution

Resolution proof system has been designed by Robinson.

A single rule (or two in first-order)

Easy to (semi-)automatize

Requires formulas to be in clausal form (skolemisation et tutti quanti)

Proofs are boring to read for humans

Hilbert's proof system

Hilbert's proof system was invented by Hilbert.

Any formulas can be written, no syntactic restriction

A proof is just a list of formulas

Easy to define. Often used when you quickly want to define a notion of formal proof

Proofs are tedious to read by humans

Difficult to (semi-)automatize

Natural deduction

Natural deduction was invented by Gentzen.

Proofs look like what mathematicians do, thus are easy to read for humans.

Proofs are not a list of formulas anymore, but a list of sequents.

Difficult to (semi-)automatize