Descriptif
Objectifs pédagogiques
L'objectif de ce cours est fournir aux étudiants une base de connaissances rigoureuse et suffisante pour leur permettre d’appréhender plus facilement dans la suite de leur cursus un ensemble de formalismes, langages, méthodes et outils en lien avec la logique, utilisés dans différents domaine de l’informatique :
- des langages de programmation logique (prolog, datalog), ou fonctionnels (Caml, Haskell),
- des méthodes outils de démonstrations (SAT-Solvers, assistants de preuve),
- des méthodes formelles pour la vérification de programme ou de protocoles (méthode B, …)
- des langages de modélisation pour la représentation des connaissances en IA (Descritpion logics, Owl, …), ou pour la spécification de propriétés (logiques temporelles LTL, CTL).
Pour cela le cours décrira aussi bien la sémantique que la théorie des preuves de différentes logiques .
Diplôme(s) concerné(s)
Parcours de rattachement
Format des notes
Numérique sur 20Littérale/grade européenPour les étudiants du diplôme Echange international non diplomant
Vos modalités d'acquisition :
Examen final.
L'UE est acquise si Note finale >= 10- Crédits ECTS acquis : 2.5 ECTS
La note obtenue rentre dans le calcul de votre GPA.
Pour les étudiants du diplôme Diplôme d'ingénieur
Vos modalités d'acquisition :
Examen final.
L'UE est acquise si Note finale >= 10- Crédits ECTS acquis : 2.5 ECTS
- Crédit d'UE électives acquis : 2.5
La note obtenue rentre dans le calcul de votre GPA.
Programme détaillé
Le cours commencera par présenter la logique classique propositionnelle et du premier ordre : sémantique, systèmes de déduction (système de Hilbert, déduction naturelle, calcul des séquents LK), théorèmes d'adéquation et de complétude, théorème de compacité, théorème d'élimination des coupures.
Il donnera une introduction aux méthodes et outils de démonstration automatiques (Algorithme de Davis-Putnam-Logemann-Loveland, solveurs SAT, Skolémisation, Unification, Résolution).
Il décrira ensuite la logique intuitionniste: calcul des séquents LJ. Traduction de la logique classique vers la logique intuitionniste.
Enfin, une introduction à la logique linéaire sera proposée : sémantique des phases et sémantique des espaces cohérents, calcul des séquents et réseaux de preuves.
