INF551 - Computational Logic: Artificial Intelligence in Mathematical Reasoning

Teaching staff: Stéphane Graham-Lengrand <stephane.lengrand@polytechnique.edu>

Lectures and practicals are on Fridays afternoons, from 14:00 to 18:15, in Salle Nicole-Reine Lepaute, Turing building (building 24 on this map).

Evaluation is, for 25% of the grade, class participation, and for 75% of the grade, an exam (on 21/12/2018).

Date Lectures Practicals
21/09/2018

Lecture 0 - Introduction
slides

Install party

Lecture 1 - Review of undergradate curriculum
slides

TD1 (OCaml)

Correction

28/09/2018

Lecture 2 - Automated reasoning mechanisms for propositional logic
slides

05/10/2018

Lecture 3 - Extending propositional reasoning
slides

12/10/2018

Lecture 4 - Semi-decision procedures for proof-search: goal-directed techniques and unification
slides

TD2 (Prolog)

Correction

19/10/2018

Lecture 5 - Introduction to logic programming, Resolution
slides

TD3 (Coq)

Correction

26/10/2018

Lecture 6 - The theory of sets
slides

09/11/2018

Lecture 7 - The theory of functions
slides

23/11/2018

Lecture 8 - The lambda-calculus: Arithmetic and Computability
slides

TD4 (Coq)

Correction

30/11/2018

Lecture 9 - Intuitionistic logic(s) and the proofs-as-programs paradigm
slides

TD5 (Coq)

Correction

21/12/2018

Exam

Correction

Past exams:
2017, Correction
2016, Correction
2015, Correction
2013 with correction

All lectures in one file: lectureall.pdf