v2.4.0 (3109)

Enseignement scientifique & technique - MITRO201 : Logique

Domaine > Mathématiques.

Descriptif

Ce cours propose une introduction à la logique mathématique en lien avec son utilisation en ’informatique.

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 .

Format des notes

Numérique sur 20

Littérale/grade européen

Pour 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. 

Mots clés

Logique classique, logique intuitionniste, logique linéaire, théorie des preuves, théorie des modèles.
Veuillez patienter