Descriptif

This course addresses the issue of using computers for modelling and solving problems of logical or mathematical nature.

In that respect we shall explore the deductive approach to Artificial Intelligence, based on mathematical logic and advocated by AI's founder John McCarthy.

More precisely, we shall investigate how the deductive mechanisms of mathematical reasoning give rise to computational models and algorithms for automated reasoning.

We shall see the trade-off between expressivity and efficient automation: Starting with the complete automation of boolean logic, we shall gradually increase the expressivity of our frameworks to model more and more complex problems, ending up with Set Theory and Type Theory as the foundations of all mathematics. Acknowledging the strengths and weaknesses of human reasoning and automated reasoning, we shall end with a form of human-computer interaction, namely interactive theorem proving.

Along the way, we shall see the principles of Logic Programming, and the Goedel-Church-Turing incompleteness and undecidability theorems will always be in the background. More comprehensively, the programme can be given by the following sequence of keywords:

- Review: logic, models, Peano's and Presburger's arithmetics, Church's and Goedel's theorems.
- SAT, SAT-modulo-Theories, quantifier elimination.
- General-purpose proof-search: forward reasoning / backward reasoning, unification.
- Proof-search as a programming paradigm: introduction to Logic Programming / Prolog.
- Set Theory, Type Theory, lambda-calculus, Curry-Howard correspondence

This is also a course on Logic in practice, so all practicals will be on computers, unless you specifically decide to be evaluated by paper-based / theoretical work (in which case you may devote some of the practicals to the preparation of this evaluation).

The website for the course is located at the following URL: http://www.enseignement.polytechnique.fr/informatique/INF551/

Important: You need to bring a working laptop for this course (running Windows, MacOS, or Linux).

Practicals will consist in programming theorem proving algorithms and strategies (the OCaml language is recommended for this, unless you have reasons to use another one), getting familiar with Prolog, and using an interactive proof assistant such as Coq, in particular to formalise algebraic problems and proofs.

Pre-requisites: some basic knowledge of logic, the course INF412 being of course perfect for this, otherwise reading some introductory book on logic over the summer is recommended (e.g. the course notes of INF412 -ch. 3-6 may suffice, or G. Dowek's book "Proofs and Algorithms: An Introduction to Logic and Computability" -ch. 1-2 may suffice, or S. Cerrito's "Logique pour l'informatique").

Tuition language: English