|
Courses and Workshops
|
| Title: | Recent advances in deduction modulo |
| Lecturer(s): | Gilles Dowek (Ecole polytechnique and INRIA) |
| Type: | Advanced Course |
| Section: | Logic and Computation |
| Week: | First | | Time: | 14.00-15.30 (Slot 3) |
| Webpage: | http://www.lix.polytechnique.fr/~dowek
|
| Reader: | Download | | Room: | C1 |
Description This course is in the same spirit as the course I gave at ESSLLI two
years ago. But it put more emphasis on ongoing developments in deduction
modulo, in particular on the expression of set theory in deduction
modulo using a representation of sets as pointed graphs. Another
modification is the introduction of a first non-technical lecture
dedicated to an history of the notion of computation in logic and in
mathematics.
Deduction modulo is a framework that integrates computation and
deduction in a single notion of proof. It is particularily well-suited
to study proofs and proof search methods in various theories, such as
equational theories, the simple type theory, set theory, stratified set
theories, etc. The goal of this course is to present deduction modulo
and to use it to present basic results in proof theory (Gentzen'
theorem, Girard's theorem, Crabbe' counter-example, ...) and ongoing
work on the expression of set theory in deduction modulo using a
representation of sets as pointed graphs.
1. Computation and deduction integrated
An history of the notion of computation in logic and in mathematics.
2. Predicate logic and deduction modulo
Predicate logic, proofs, natural deduction, models, classical and
constructive logic, rewriting terms and rewriting propositions, the
equivalence lemma, Prawitz' cuts and cuts modulo.
3. Simple type theory and arithmetic
Type theory as a first-order theory. Deduction and computation in type
theory. Peano's axioms as rewrite rules.
< 4. Cut elimination in first-order logic and in deduction modulo
Curry-de Bruijn-Howard isomorphism, cut elimination in the empty theory,
Reducibility candidates. Pre-models. Examples and counterexamples of
theories having the cut elimination property. Girard's theorem.
Crabbe''s counterexample. Applications of cut elimination to proof
search and to programming in constructive logic.
5. Set theory
Sets as pointed graphs. Bisimulation. Extensionality and strong
extensionality. Deduction and computation in set theory. Cut elimination.
|
© 2003, 2004 LORIA, Carlos Areces. |
2003-11-20
| |
