La logique informatique est utilisé dans un large éventail d'applications en informatique, allant de l'approche déductive de l'Intelligence Artificielle préconisée par le pionnier de l'IA, John McCarthy, à la démonstration de l'absence de bogues dans de grands logiciels industriels, comme la ligne 14 du métro de Paris, ou à vérifier les théorèmes difficiles comme celui de Feit-Thompson dans la classification des groupes simples finis.
L'objectif de ce cours est d'expliquer la manière dont la logique peut être utilisée afin de modéliser des problèmes de nature informatique ou mathématique, et comment les ordinateurs peuvent être utilisés pour y parvenir. Nous allons présenter des assistants de preuve, qui permettent de formaliser un raisonnement humain par la construction interactive de preuves, et expliquent leur utilité pour certifier l'absence de bogues dans les programmes. Il est basé sur la correspondance Curry-Howard : un programme est identique à une preuve (ou plus précisemment, un programme fonctionnel typé correspond à une dérivation de son type). Afin d'atteindre des applications réalistes, nous présenterons l'assistant de preuve Agda et la logique dépendente qu'il sous tend. Si le temps nous le permet, nous présenterons également différentes notions et techniques telles que la théorie des ensembles et la recherche de preuve.
Ce cours est aussi à propos de logique en pratique : toutes les PC se feront sur ordinateurs, utilisant OCaml puis Agda.
Site du cours : http://inf551.mimram.fr/
Computational logic has been used in a wide range of application in computer science, ranging from the deductive approach to Artificial Intelligence advocated by AI's founder John McCarthy, to proving the absence of bugs in large industrial software such as the 14th metro line in Paris, or checking difficult theorems the as the one of Feit-Thompson in the classification of finite simple groups.
The goal of this course is to explain how logic can be used in order for modeling problems of computational or mathematical nature, and how computers can be used to achieve this. In particular, we will present proof assistants, which allow to formalize human reasoning by interactively constructing proofs, and explain their use to certify the absence of bugs in programs. This is based on the so-called Curry-Howard correspondence: a program is the same as a proof (or, more precisely, a typed functional program corresponds to a derivation of its type). Then in order to reach realistic applications, we will present the proof assistant Agda and dependent logic which underlies it. Time permitting, we will also present various important related notions and techniques such as set theory and proof search.
This course is also about logic in practice: all the TDs will be on computer, using OCaml and then Agda.
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 (see the references on the website).
The website for the course is http://inf551.mimram.fr/
- Teaching coordinator: Mimram Samuel