L’objectif de cette UE est de présenter à la fois la logique comme modèle de calcul et outil de programmation et d’aborder la notion de calculabilité et les différents modèles de calcul.
Une première partie est consacrée à la logique des prédicats et la construction de preuves dans différents systèmes formels, incluant la résolution et sa mise en œuvre en programmation logique. Une seconde partie est consacrée à la calculabilité et à différents modèles de calcul, leurs correspondances et leurs impacts sur des langages de programmation.
Prérequis
Fondements mathématiques.
Acquis d’apprentissage
- Logique classique du premier ordre
- Sémantique
- Systèmes formels : calcul des séquents, déduction naturelle
- Correction, complétude, construction de preuves
- Résolution et preuves
- Mise sous forme clausale
- Résolution : concepts, clauses, stratégies
- Programmation logique : clauses de Horn, SLD-résolution
- Machines de Turing
- Définitions
- Calculabilité
- Fonctions récursives
- Définitions
- Équivalence avec les machines de Turing
- Calculabilité et non-calculabilité
- Calculabilité et décidabilité
- Principe de réduction pour l’indécidabilité
- Équivalences entre les modèles de calcul
- Fonctions récursives et lambda-calcul.
Compétences visées
- Comprendre et mettre en œuvre des méthodes de raisonnement et de démonstration en vue de la vérification de programmes.
- Maîtriser les notions de calculabilité et de décidabilité pour proposer des solutions algorithmiques à certains problèmes.
- Concevoir des algorithmes et évaluer leur complexité.
- Modéliser des problèmes complexes.