Teaching staff: Stéphane GrahamLengrand <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 
Install party 
Lecture 1  Review of undergradate curriculum 
TD1 (OCaml)  
29/09/2017 
Lecture 2  Automated reasoning mechanisms for propositional logic 

06/10/2017 
Lecture 3  Extending propositional reasoning 

13/10/2017 
Lecture 4  Semidecision procedures for proofsearch: goaldirected techniques and unification 
TD2 (Prolog)

20/10/2017 
Lecture 5  Introduction to logic programming, Resolution 
TD3 (Coq)

27/10/2017 
Lecture 6  The theory of sets 

10/11/2017 
Lecture 7  The theory of functions 

24/11/2017 
Lecture 8  The lambdacalculus: Arithmetic and Computability 
TD4 (Coq)

01/12/2017 
Lecture 9  Intuitionistic logic(s) and the proofsasprograms paradigm 
TD5 (Coq)

22/12/2017 
Past exams:
2016, Correction
2015, Correction
2013 with correction