## Deduction modulo rewritingGilles Dowek (INRIA and ENS Paris-Saclay) |

Slides of Lecture 1 and Lecture 2.

We all know that 2+2 is equal to 4 and that the square root of 2 is irrational. But to judge that this is the case, we proceed in a different way. In the first case, we compute: we rewrite the term 2+2 to the term 4, in the second we deduce: we build a proof of this statement. Computation and deduction are often intertwined: the proof of a theorem alternates computation steps and deduction steps.

In this course, we shall see how rewrite rules and deduction rules can be articulated to bring a new definition of the notion of proof, and also a new notion of theory: Predicate logic, Simple type theory, or the Calculus of constructions will just appear to us as examples of theories, defined by different rewrite rules, paving the way to a universal representation of formal proofs, independently of the theory or the system in which they have been developed.

### Outline of the course

- Deduction modulo theory
- Examples of theories
- Dependent types
- Application to reverse mathematics

### Bibliography

- Proofs in theories, lecture notes, Gilles Dowek, 2018
- logipedia.science, an online library of Dedukti proofs