Objectifs : Pour ce module nous avons fixé deux objectifs :
Introduire les étudiants à la logique mathématique et en particulier à la méthode de la démonstration.
Fournir aux étudiants les bases nécessaires afin de pouvoir comprendre le fonctionnement de la plupart des outils de démonstration automatique développés en particulier dans le monde académique, et éventuellement de coder eux-mêmes un tel outil.
Contenu de la matière
Chapitre 1 : Introduction
1.1 Récursivité et induction
1.2 Raisonnement par récurrence sur N
1.3 Formalisation : Premier théorème du point fixe
1.4 Applications
1.4.1 Quelques exemples
1.4.2 Arbres binaires étiquetés
2 Chapitre : Démonstrations
2.1 Introduction
2.2 Démonstrations à la Frege et Hilbert
2.3 Démonstration par déduction naturelle
2.3.1 Règles de la déduction naturelle
2.3.2 Validité et complétude
2.4 Démonstrations par résolution
3 Chapitre : Modèles de calculs
3.1 Machines de Turing
3.1.1 Ingrédients
3.1.2 Description
3.1.3 Programmer avec des machines de Turing
3.1.4 Techniques de programmation
3.1.5 Applications
3.1.6 Variantes de la notion de machine de Turing
3.1.7 Localité de la notion de calcul
3.2 Modèles rudimentaires
3.2.1 Machines à k ≥ 2 piles
3.2.2 Machines à compteurs
3.3 Thèse de Church-Turing
3.3.1 Équivalence de tous les modèles considérés
4 Chapitre : Calculabilité
4.1 Machines universelles
4.1.1 Interpréteurs
- معلم: MOHAMMED CHAOUI