Logique et Raisonnement – CETS8AB

Programme et contenu

Objectifs pédagogiques

Qu’est-ce qu’une 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 d’incomplé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, l’informatique
(complexité, démonstration automatique, sécurité, base de données), et les systèmes complexes.

Contenu – Programme

• Logique du 1er ordre :
  • Dualité syntaxe et sémantique
  • Système formel et déduction
  • Théorème de complétude (Gödel 1930) et théorème de compacité
• Base de la théorie de la démonstration
  • Lambda-calcul
  • Preuves et programmes : Isomorphisme de Curry-Howard
  • Systèmes de types et programmation sûre
• Calculabilité et Complexité
  • Problèmes indécidables, théorèmes d’incomplétudes
  • Fragments décidables, problèmes NP et déduction automatique

Chaque séance sera composée d’un cours suivi d’une 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.

Compétences