MPRI M1 course on proof theory

MPRI M1 course PROT, 7*4+2=30 hours [serveur pédagogique]

Place: ENS Paris-Saclay, room 1O07

Staff: Frédéric Blanqui (lectures) and Antoine Gontard (exercises)

Textbook: Proof in theories, Gilles Dowek, 2022

Planning:

• Friday 22 January 2027, 8:30-10:30 Lecture 1, 10:45-12:45 TD 1
• Friday 29 September 2027, 8:30-10:30 Lecture 2, 10:45-12:45 TD 2
• Friday 5 February 2027, 8:30-10:30 Lecture 3, 10:45-12:45 TD 3
• Friday 12 February 2027, 8:30-10:30 Lecture 4, 10:45-12:45 TD 4
• Friday 26 February 2027, 8:30-10:30: Lecture 5, 10:45-12:45:TD 5
• Friday 5 March 2027, 8:30-10:30: Lecture 6, 10:45-12:45:TD 6
• Friday 12 March 2027, 8:30-10:30: Lecture 7, 10:45-12:45:TD 7
• Friday 19 March 2027, 8:30-10:30: Exam

Online termination, confluence and completion tools:

• AProVE
• TTT2
• CSI
• ConCon
• mkbTT

More tools are available on:

• termination portal
• confluence competition

Useful by not necessary L3 courses:

• 12 leçons de logique en vidéo
• L3 course on logic (LOG2)
• L3 course on λ-calculus (LAL2)

Possible following M2 courses:

• MPRI M2 course on Foundations of Proof Systems (PRFSYS)
• MPRI M2 course on Proof Assistants (PRFA)