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

Bibliography

Comments are closed.