Programmes et contenus : Objectifs pédagogiques
Quest-ce quune démonstration ? Peut-on résoudre tous les problèmes ? Est-ce que les mathématiques sont cohérentes ? Quelles sont les limites des calculs ? Ce cours essaiera de répondre à toutes ces questions. Tout d'abord, nous formaliserons la notion de démonstration et le rapport avec la notion de vérité, ce qui nous conduira au théorème de complétude de Gödel (1930). Ensuite, nous aborderons la notion centrale d'indécidabilité et de décidabilité, jusqu'aux théorèmes dincomplétudes (Church-Gödel-Turing). Cela nous mènera à construire des algorithmes de démonstration automatique. Enfin, nous verrons la relation entre démonstrations et algorithmes à savoir que certaines démonstrations de logiques constructives sont, en essence, des algorithmes.
Les développements et les applications de la logique touchent la philosophie, la linguistique, linformatique
(complexité, démonstration automatique, sécurité, base de données), et les systèmes complexes.
Contenu - Programme
Logique du 1er ordre :
o Dualité syntaxe et sémantique
o Système formel et déduction
o Théorème de complétude (Gödel 1930) et théorème de compacité
Base de la théorie de la démonstration
o Lambda-calcul
o Preuves et programmes : Isomorphisme de Curry-Howard
o Systèmes de types et programmation sûre
Calculabilité et Complexité
o Problèmes indécidables, théorèmes dincomplétudes
o Fragments décidables, problèmes NP et déduction automatique Chaque séance sera composée d'un cours suivi dune discussion et d'exercices. Des articles seront proposés pour comprendre les notions du cours et pour aller plus loin.
Non-french speakers are welcome. |