This page contains the teaching material of David Baelde. Other documents may be accessed through the pages of the other teachers of the course: Gilles Dowek and Emilie Grienenberger.
Material
- Classical first-order logic: lecture notes in French (extended on 26/11)
- Rules of natural deduction: PDF (fixed on 24/11)
- Homework 1: Nelson-Oppen combination (PDF) due by March 2
- Intuitionistic logic: PDF (fixed on 24/11)
- Resolution strategies: PDF, TeX
- Decidable theories: PDF
- Ehrenfeucht-Fraïssé games: PDF
- Final homework exam: PDF (revision 1, fixes question 2 of flat Kripke exercise).
Agenda
Items in gray taught by Gilles Dowek. Past sessions:
- january 20: predicate calculus, syntax & semantics and natural deduction
- january 27: α-renaming, soundness, arithmetics
- february 3: independence, geometry, set theory
- february 10: completeness
- february 24: undecidability, incompleteness
- march 2: intuitionistic logic, proof normalization, witness properties
- march 9: models of intuitionistic logic
- march 16:
mid-term exam - 23 mars: calcul des séquents, recherche de preuve, unification
- march 30: cut elimination
- april 20: clausal form, Skolem theorem, resolution
- april 27: Herbrand theorem, completeness of resolution
- may 4: resolution strategies
- may 11: decidable theories
- may 18: Ehrenfeucht-Fraissé games
Upcoming:
- may 25: examination (homework)