INF551 - Computational Logic: Artificial Intelligence in Mathematical Reasoning

Teaching staff: Stéphane Graham-Lengrand <stephane.lengrand@polytechnique.edu>, and Roberto Blanco <roberto.blanco@inria.fr>.

Lectures and practicals are on Fridays afternoons, from 14:00 to 18:15, in PC18.

Evaluation is, for 25% of the grade, class participation, and for 75% of the grade, either an exam (on 22/12/2017) or a course project. The choice is almost up to you, notwithstanding that the number of projects done in the class will be limited to around 10.

Date Lectures Practicals
22/09/2017

Lecture 0 - Introduction
slides

Install party

Lecture 1 - Review of undergradate curriculum
slides

TD1 (OCaml)

Correction

29/09/2017

Lecture 2 - Automated reasoning mechanisms for propositional logic
slides

06/10/2017

Lecture 3 - Extending propositional reasoning
slides

13/10/2017

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

TD2 (Prolog)

Correction

20/10/2017

Lecture 5 - Introduction to logic programming, Resolution
slides

TD3 (Coq)

Correction

27/10/2017

Lecture 6 - The theory of sets
slides

10/11/2017

Lecture 7 - The theory of functions
slides

24/11/2017

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

TD4 (Coq)

Correction

01/12/2017

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

TD5 (Coq)

Correction

22/12/2017

Exam

Correction

All lectures in one file: lectureall.pdf