Logique des prédicats

Cette conférence porte sur la logique des prédicats, une extension de la logique des propositions permettant de modéliser des situations plus complexes, notamment celles impliquant plusieurs individus. Elle s'inscrit dans un cours d'introduction à la logique formelle et à ses applications en informatique, notamment en bases de données déductives et en programmation logique.

Introduction à la logique des prédicats

La logique des propositions présente des limites lorsqu'il s'agit de raisonner sur plusieurs individus. Par exemple, pour modéliser la situation suivante :

• Si un étudiant a les unités d'enseignement (UE) PROG001 et PROG002, alors il a le module PROG.
• Si cet étudiant a aussi l'UE Stage, alors il obtient le certificat professionnel CP PROGRAMMEUR.

En logique des propositions, on peut écrire :

prog001 ∧ prog002 → prog
prog ∧ stage → cp

Mais ce système ne permet pas de gérer plusieurs étudiants sans dupliquer les règles pour chaque cas particulier, par exemple :

aragornAprog001 ∧ aragornAprog002 → aragornAprog
aragornAprog ∧ aragornAstage → aragornAcp
bilboAprog001 ∧ bilboAprog002 → bilboAprog
bilboAprog ∧ bilboAstage → bilboAcp

Pour éviter cette duplication, on introduit la notion de variables, permettant de raisonner de manière générale :

∀X(prog001(X) ∧ prog002(X) → prog(X))
∀X(prog(X) ∧ stage(X) → cp(X))

On ajoute ainsi des arguments aux propositions, formant des prédicats, qui sont des expressions vraies ou fausses selon les valeurs des variables.

Syntaxe de la logique des prédicats sans symboles fonctionnels

On définit un sous-ensemble simplifié de la logique des prédicats du premier ordre, sans symboles fonctionnels :

• Un ensemble de symboles de prédicats P, chaque prédicat ayant une arité (nombre d'arguments).
• Un ensemble de constantes C.
• Un ensemble de variables X.

Les formules sont construites inductivement :

• Base : si p/n ∈ P, alors p(a1, ..., an) est une formule, pour tout ai dans C ∪ X (appelée atome).
• Les prédicats d'arité 0 correspondent aux propositions.
• Si A et B sont des formules et X une variable, alors :
• ¬A est une formule.
• (A ∧ B), (A ∨ B), (A → B) sont des formules.
• ∀X A et ∃X A sont des formules.

Les parenthèses servent à éviter les ambiguïtés.

Une grammaire formelle en DCG (Definite Clause Grammar) peut décrire cette syntaxe, avec des règles pour termes, atomes et formules, ainsi qu'un lexique simple.

Quantification et variables

Les quantificateurs universel (∀X p(X)) et existentiel (∃X p(X)) permettent d'exprimer des propriétés sur tous les éléments ou sur au moins un élément du domaine.

Quelques particularités :

• La portée d'un quantificateur ∀X A est la formule A. Les variables portant le même nom mais hors portée sont considérées comme différentes.
• ¬(∀X A(X)) est équivalent à ∃X ¬A(X).
• ¬(∃X A(X)) est équivalent à ∀X ¬A(X).

On distingue :

• Variables quantifiées : apparaissant immédiatement après un quantificateur.
• Variables liées : apparaissant dans la portée d'un quantificateur.
• Variables libres : n'étant dans la portée d'aucun quantificateur.

Une formule est dite fermée (close) si elle ne contient aucune variable libre. Un terme est clos s'il ne contient pas de variable.

Notion d'ordre en logique

La logique du premier ordre quantifie uniquement sur les termes (constantes, variables, fonctions). La logique du second ordre permet de quantifier aussi sur les prédicats eux-mêmes.

Exemple de formule du second ordre : ∀P ∃Y P(Y).

Sémantique de la logique des prédicats

Comme en logique des propositions, une interprétation associe un sens aux constantes et aux prédicats :

• Les constantes sont associées à des éléments d'un domaine D.
• Un prédicat p/n est interprété comme une fonction de D^n vers {vrai, faux}.

Exemples :

• Avec D = {1, 2}, a interprété comme 1, b comme 2, et r(X) signifiant "X est pair", alors r(a) est faux, r(b) est vrai.
• Avec D = {java, lisp}, a interprété comme java, b comme lisp, et r(X) signifiant "X est un langage impératif", r(a) est faux, r(b) est vrai.

Pour interpréter une formule avec variables, on considère une assignation donnant une valeur à chaque variable. L'interprétation est définie inductivement sur la structure des formules, en évaluant d'abord les termes, puis les atomes et les formules composées.

Exemples de modélisation avec la logique des prédicats

On peut modéliser l'organisation des cours dans un IUT à partir de tables représentant les enseignants, étudiants et modules. Chaque table est interprétée comme un prédicat :

• enseignant/3 : enseignant(id, nom, prénom)
• étudiant/3 : étudiant(id, nom, prénom, classe)
• module/3 : module(id-mod, intitulé, classe, id-prof)

Par exemple, enseignant(1, Baggins, Frodo) est vrai.

On peut écrire des formules avec une variable libre X pour exprimer :

• X est le nom d’un enseignant.
• X est le nom d’un enseignant de programmation.
• X est le nom d’un étudiant qui suit au moins un cours.
• X est l’intitulé d’une matière suivie par tous les étudiants.

On peut aussi exprimer en logique du premier ordre :

• Il n’y a pas d’enseignant qui enseigne la programmation (formule fausse si un tel enseignant existe).
• Tous les étudiants suivent au moins un cours.
• Il existe un enseignant qui donne des cours à tous les étudiants.

Logique des prédicats du premier ordre avec symboles fonctionnels

Les prédicats peuvent avoir pour arguments des termes construits à l’aide de symboles fonctionnels, qui modélisent des fonctions ou des structures comme les listes. Ces symboles ne doivent pas être confondus avec les prédicats.

Exemple :

∀X estPair(plus(X, X))

où estPair/1 est un prédicat, plus/2 un symbole fonctionnel.

Les constantes sont considérées comme des symboles fonctionnels d’arité 0.

Exemple de définition de listes :

• vide : constante représentant la liste vide.
• cons : symbole fonctionnel prenant deux arguments, le premier élément et la queue de la liste.

La liste [4, 2, 8] s’écrit : cons(4, cons(2, cons(8, vide))).

Le prédicat membre/2, membre(X, L), signifie que X est un élément de la liste L. Par exemple :

membre(2, cons(4, cons(2, cons(8, vide))))

est vrai.

Syntaxe des termes et formules avec symboles fonctionnels

Les termes sont définis inductivement :

• Une variable est un terme.
• Une constante est un terme.
• Si f/n est un symbole fonctionnel d’arité n, et t1,...,tn sont des termes, alors f(t1,...,tn) est un terme.

Les formules sont définies comme précédemment, avec la base :

Si p/n est un prédicat d’arité n et t1,...,tn sont des termes, alors p(t1,...,tn) est une formule.

Sémantique avec symboles fonctionnels

L’interprétation doit associer :

• À chaque constante une valeur dans le domaine ID.
• À chaque symbole fonctionnel d’arité n une fonction de ID^n vers ID.
• À chaque prédicat d’arité n une fonction de ID^n vers {vrai, faux}.

Exemple simple en arithmétique :

• Constante z interprétée comme 0.
• Symbole fonctionnel s/1 (successeur) interprété comme la fonction "successeur" sur les entiers.
• Prédicat p/1 interprété comme "est pair".

On définit l’évaluation des termes et formules par induction, en tenant compte de l’assignation des variables.

Modèles, formules consistantes et valides

Une interprétation I est un modèle d’une formule F si F est vraie dans I pour toute assignation. On note :

|=I F

Une formule est :

• Consistante si elle possède au moins un modèle.
• Inconsistante si elle n’a aucun modèle (par exemple p(X) ∧ ¬p(X)).
• Valide si elle est vraie dans toutes les interprétations et toutes les assignations (par exemple ∀X (p(X) ∨ ¬p(X))).

Une formule F est conséquence logique de formules F1, F2,..., Fn si tout modèle de F1,..., Fn est aussi un modèle de F.

Interprétation de Herbrand

L’interprétation de Herbrand donne une version purement syntaxique de l’interprétation :

• Le domaine ID est l’ensemble des termes clos (sans variables), appelé domaine de Herbrand.
• La base de Herbrand est l’ensemble des formules atomiques closes construites à partir du domaine.
• Une interprétation de Herbrand est une partition de cette base en atomes vrais et faux.

Exemple 1 :

• F = {sethy, ramses}, P = {pere/2}.
• Domaine de Herbrand DH = {sethy, ramses}.
• Base de Herbrand = {pere(sethy, ramses), pere(sethy, sethy), pere(ramses, sethy), pere(ramses, ramses)}.
• Une interprétation possible : {pere(sethy, ramses)}.

Exemple 2 :

• F = {z/0, s/1}, P = {p/1}.
• Domaine de Herbrand DH = {z, s(z), s(s(z)), s(s(s(z))), ...} (infini).
• Base de Herbrand = {p(z), p(s(z)), p(s(s(z))), ...} (infini).
• Tout sous-ensemble de la base définit une interprétation, par exemple :
• I1 = base entière.
• I2 = éléments avec un nombre pair de s.
• I1 et I2 sont modèles de ∀X (p(X) → p(s(s(X)))).

Manipulation des variables : substitutions et unification

En démonstration automatique et en programmation logique (Prolog), il est souvent nécessaire de remplacer des variables par des termes (substitution), pas seulement par des valeurs.

Substitution de variables

Une substitution σ est une fonction qui associe à des variables libres des termes.

Exemple :

σ = [X ← Y, Z ← s(X)]

applique X → Y et Z → s(X).

On applique la substitution simultanément sur toutes les occurrences libres des variables concernées.

Sur une formule A, on note Aσ la formule obtenue après substitution.

Attention : on ne substitue que les variables libres. Pour éviter des confusions, on ne permet pas que des variables liées apparaissent dans les termes substitués.

Unification de variables

Un unificateur est une substitution rendant deux formules égales (à un renommage près des variables liées).

Exemple :

• A = ∃Y p(Z, W, Y)
• B = ∃K p(A, A, K)
• σ1 = [Z ← f(m), W ← f(m), A ← f(m)] est un unificateur.
• σ2 = [Z ← A, W ← A] est un autre unificateur, plus général.

Il existe un unificateur le plus général, qui est plus général que tous les autres au sens où tout autre unificateur peut s'obtenir en lui appliquant une substitution.

Exercices d’application : modélisation de tableaux et prédicats Prolog

Pour raisonner sur des programmes manipulant des tableaux, on introduit une fonction case/2, où le premier argument est le nom du tableau et le second l’indice de la case.

En supposant que le tableau t est de taille n, et en utilisant la logique des prédicats (avec des symboles mathématiques usuels comme <, >, =), on peut exprimer :

• Le tableau t contient la valeur a.
• m est le maximum des éléments du tableau t.
• Le tableau t est trié.

Exemple en Prolog du prédicat contient :

contient(X, cons(X, L)).
contient(X, cons(A, L)) :- contient(X, L).

Traduction en logique des prédicats :

∀X ∀L contient(X, cons(X, L))
∀X ∀A ∀L (contient(X, L) → contient(X, cons(A, L)))

En réalité, ce programme Prolog correspond à :

∀X ∀L (contient(X, L) ↔ (∃L0 (L = cons(X, L0)) ∨ ∃A ∃L0 (L = cons(A, L0) ∧ contient(X, L0))))