# Gilles Dowek ## Deduction modulo rewriting

Gilles 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