Logique 2Code de l'UE : HLIN602
Présentation
Ce cours vise à donner les bases mathématiques permettant de manipuler la logique des prédicats, (c'est à dire les quantificateurs
quel que soit
et
il existe)
.
Une fois la syntaxe définie (dans un premier temps sans symbole fonctionnel), c'est à dire une fois qu'a été défini sans ambiguité ce qu'on a
le droit
d'écrire, on est amené, pour pouvoir donner
un sens
à ce qu'on a le droit décrire, à définir les notions de domaine d'interprétation d'un prédicat et d'assignation d'une variable.Le sens de la formule est alors donné par un
calcul
.
Pour pouvoir automatiser ce calcul, on définit des manipulations syntaxiques (passage à la forme prénexe et à la forme clausale, skolémisation, unification),ce qui permet de présenter l'algorithme de Robinson (base du langage Prolog).
Enfin le théorème de Herbrand précise la complétude de l'algorithme.
Volume horaire
- CM : 15
- TD : 27
- TP : 0
Diplômes intégrant cette UE
En bref
Crédits ECTS 5
Nombre d'heures 46 HE
Période de l'année
S6
Contact(s)
Composante
Faculté des Sciences