Deduction modulo rewriting
Gilles Dowek (INRIA and ENS Paris-Saclay)
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