Previous Up Next
Eléments de logique pour l’informatique 2019–20                  http://www.lri.fr/~paulin/Logique


Chapitre 3  Calcul des prédicats

Le calcul propositionnel a de bonnes propriétés (on peut décider si une formule est valide ou satisfiable) mais manque d’expressivité surtout quand il faut modéliser des espaces infinis comme les entiers. On pourrait utiliser une infinité de variables propositionnelles et une infinité d’hypothèses mais ce n’est pas facile à manipuler pour des humains et encore moins pour des machines.

Il peut être utile d’avoir des descriptions finies qui rendent compte de situations potentiellement infinies.

Ainsi la formule x ∈ ℕ, xx2 représente toutes les formules 0≤ 0, 1≤ 1, 2≤ 4, 3≤ 9

Dans ce chapitre nous allons étudier formellement le calcul des prédicats (appelé aussi logique du premier ordre), le langage utilisé, la notion de validité, de modèle, les formes normales, les systèmes de preuve.

Exemple de modélisation.

Même dans le cas fini, le calcul des prédicats permet de modéliser des problèmes de manière plus concise et conceptuellement plus simple.

Pour modéliser le jeu du Sudoku, on introduit le langage suivant :

On a ainsi un seul symbole de prédicat au lieu de 9×9× 9 variables propositionnelles. On peut exprimer sous forme de formule logique les contraintes suivantes sur une solution

3.1  Syntaxe

La première chose à préciser est le langage qui sera utilisé pour écrire les formules. En logique propositionnelle, on a juste des variables propositionnelles, des constantes et et des formules construites à l’aide de connecteurs ¬,, , . Dans le calcul des prédicats, on a de plus des objets dont on va exprimer les propriétés (entiers, ensembles, objets géométriques), on introduit des relations entre ces objets qui vont constituer les formules atomiques (comme l’égalité ou l’appartenance d’un élément à un ensemble ou encore que des droites sont parallèles). En plus des connecteurs logiques propositionnels, on va avoir des quantificateurs x et x qui nous permettent de parler d’objets arbitraires en les désignant par un nom.

Le calcul des prédicats est un cadre général. En mathématiques, on se place a priori dans un langage très puissant qui est celui de la théorie des ensembles. Beaucoup de démonstrations peuvent se faire dans un cadre plus simple qui est celui de l’arithmétique (la logique des entiers naturels). En informatique, il est beaucoup plus courant de s’intéresser à des langages logiques restreints. Par exemple les systèmes de base de données peuvent se voir comme des langages logiques dans lesquels on va avoir des “entités” simples (personnes, nombres, titres d’ouvrages, …) et des relations entre les objets (la personne X a la profession Y), les requêtes sur les bases de données peuvent se voir comme des démonstrations de certaines formules logiques. On s’intéresse aussi à des “spécifications” abstraites dans lesquelles une certaine structure de données (comme une pile ou un arbre) va être caractérisée par un ensemble d’opérations élémentaires qui satisfont certaines propriétés et à partir desquelles on va élaborer des constructions sophistiquées.

3.1.1  Termes

On introduit le langage qui décrit les objets dont on va parler.

Définition 1 (Signature)   Une signature F est composée d’un ensemble d’entités que l’on appellera des symboles et d’une application arity dans F→ ℕ qui associe à chaque symbole f F un entier arity(f) que l’on appellera l’arité de f.
Les symboles d’arité
0 sont appelés des constantes. Les autres symboles sont appelés des symboles de fonction et l’arité représente le nombre d’arguments attendus par ce symbole de fonction. On parle de symbole unaire pour une arité 1 et binaire pour une arité 2.
On notera
Fn l’ensemble des symboles d’arité n de la signature F.
Exemple 1 (Signature pour les entiers)   Une signature possible pour les entiers est constituée d’une constante 0 (arité 0) et un symbole S pour l’opération successeur d’arité 1. On peut aussi ajouter des symboles de fonctions binaires pour les opérations arithmétiques telles que l’addition (notée plus) et la multiplication (notée mult).
Exemple 2 (Signature pour les arbres binaires)   Une signature possible pour les arbres binaires (sans valeur) est constituée d’une constante є (arité 0) pour l’arbre vide et un symbole N d’arité 2 pour représenter un nœud interne.

En logique et en informatique on a besoin de considérer des termes généralisés dans lesquels apparaissent des variables. Les variables peuvent être choisies dans un ensemble infini X (mais seulement un nombre fini de variables apparaît dans chaque terme).

Définition 2 (Termes avec variables T( F, X))   Soit une signature F, un ensemble X de variables, on définit l’ensemble T( F, X) à l’aide des règles suivantes :
Exemple 3   Les mots suivants sont des termes sur la signature des entiers : S(0)    plus(S(0),0). On notera 1 le terme S(0), 2 le terme S(S(0))
Par contre les mots suivants ne sont pas des termes :
S    0(0)    S(0,0).

Sur la signature des arbres binaires on peut former les termes N(є,є) ou N(є,N(є,є)) par contre N(є) n’est pas un terme.

Notations

On utilise parfois une notation infixe pour les symboles de fonctions binaires, c’est-à-dire que l’on écrira (t1 f t2) au lieu de f(t1,t2) de même on peut omettre certaines parenthèses en s’appuyant sur des conventions, mais il s’agit de facilités d’écriture qui ne changent pas la définition mathématique.

Définition 3 (Terme clos)   Un terme de T( F, X) qui ne contient pas de variable est appelé un terme clos.

Représentation arborescente

Les termes peuvent se représenter comme des arbres. Une variable ou une constante est vue comme une feuille de l’arbre, un terme f(t1,…,tn) est représenté comme un arbre dont la racine est étiquetée par f et qui a n fils, que l’on considère de manière ordonnée. Le i-ème sous-arbre est associé au terme ti.

Exemple 4   Soit le terme t=plus(mult(0,x),S(0)) sa représentation sous forme d’arbre est donnée par :

Définition récursive sur les termes

Un terme est un objet syntaxique construit à partir d’une signature et de variables. En particulier les objets plus(0,1) et plus(1,0) sont différents.

La structure des termes nous permet d’introduire une fonction F dont le domaine est l’ensemble des termes sur une signature en se donnant des équations récursives qui “correspondent” à la signature.

On suppose que l’on veut définir une application F dans T( F, X) → A. Pour cela on va se donner les objets suivants :

  1. Une application V dans XA;
  2. Pour chaque constante c F0, un élément dcA
  3. Pour chaque symbole de fonction f Fn, une application Gf dans
     
     
     T( F, X)×… ×   T( F, X)


    n fois
    ×
     
     
    A×… × A


    n fois
     → A
    .

Il existe une unique application F dans T( F, X) → A qui vérifie :

F(x)=V(x)   (x X)   F(c)=dc  (c F0)    F(f(t1,…,tn))=Gf(t1,…,tn,F(t1),…,F(tn))  (f Fn)

Le fait que l’on puisse définir une telle application est une conséquence de l’égalité sur les termes. En particulier, deux termes qui débutent par des symboles différents sont différents.

En effet ce schéma permet de définir une application F telle que F(c)=1 pour les constantes et F(t)=2 pour tous les termes qui commencent par un symbole de fonction. Si on avait plus(0,0)=0 alors on en déduirait F(plus(0,0))=F(0) et donc 2=1.

Exemple 5 (Taille d’un terme)   Le schéma de définition récursive précédent permet de définir l’application size qui compte le nombre de symboles dans un terme. Dans le cas de la signature sur les entiers, soit t le terme plus(0,S(0)), il vérifie size(t)=4.
Exercice 1   Ecrire une fonction qui renvoie l’ensemble des variables d’un terme.
Exemple 6 (Hauteur d’un terme)   Un autre exemple de définition récursive est l’application ht qui compte le nombre maximal de symboles imbriqués dans un terme. Pour le terme t précédent on a ht(t)=3.
Substitution

On se donne une application σ∈ X T( F, X) qui associe un terme à chaque variable. On définit pour chaque terme t, le résultat de la substitution dans t de toute variable x par σ(x) que l’on note t[σ].

La définition se fait de manière récursive sur t:

Le résultat de t[σ] ne dépend que de la valeur de la substitution σ sur les variables de t. On note souvent cette substitution de la manière suivante {x1u1;…;xnun}. Cette notation correspond à une application σ telle que σ(x)=ui si x=xi et σ(x)=x sinon.

Exemple 7   t=plus(mult(x,y),S(x)) et σ={xmult(y,0);y0}.
On a
t[σ]=plus(mult( mult(y,0),0),S( mult(y,0)))

Récurrence sur les termes

On a également un schéma de preuve par récurrence sur les termes de T( F, X) qui s’exprime de la manière suivante. Soit φ(t) une propriété qui dépend d’un terme t T( F, X). On suppose :

  1. x X,P(x);
  2. pour chaque constante c F0: P(c);
  3. pour chaque symbole f Fn : t1tn T( F, X), P(t1)⇒ ⋯ P(tn)⇒ P(f(t1,…,tn));

alors t T( F, X),P(t).

Exemple 8   On peut par exemple montrer la propriété suivante sur les termes :
∀ t ∈  T( F, X),ht(t) ≤ size(t)
Preuve: La preuve se fait par récurrence sur la structure du terme t.
variable
x X, ht(x) ≤ size(x) vrai car ht(x)=0 et size(x)=0
constante
ht(c) ≤ size(c) vrai car ht(c)=1=size(c).
symbole
si f Fn: soit des termes arbitraires t1,…,tn T( F), on suppose que ht(ti) ≤ size(ti). on doit montrer ht(f(t1,…,tn)) ≤ size(f(t1,…,tn)).
ht(f(t1,…,tn))=
= 1+max(ht(t1),…,ht(tn)) 
 ≤ 1+ ht(t1)+⋯ + ht(tn
≤ 1+ size(t1)+⋯ + size(tn)
=size(f(t1,…,tn))
Exercice 2   Sur la signature des arbres binaires {є,N}, définir une fonction feuilles qui compte le nombre de feuilles et une fonction noeud qui compte le nombre de nœuds internes. Montrer que pour tout arbre t, on a feuilles(t)=noeuds(t)+1.

3.1.2  Formules

Signature du langage

Pour définir les formules, on ajoute au langage des symboles de relation (on dit aussi prédicat). Ceux-ci nous permettent de former les formules atomiques. Un symbole de relation R a une arité qui est un entier n. Cela signifie que la relation va exprimer une propriété de n termes.

Par exemple, si on s’intéresse à la géométrie on peut avoir deux symboles de relation unaires point qui sera vrai pour un objet qui représente un point et droite qui sera vrai pour un objet qui représente une droite, on introduit aussi un symbole de relation binaire appartient qui représente qu’un point est sur une droite.

A partir de ces éléments de base on peut représenter des notions plus complexes. Par exemple deux droites d1, d2 sont concourantes peut se représenter par la formule :

∃ ppoint(p) ∧ appartient(p,d1) ∧  appartient(p,d2)

Un symbole de relation que l’on va retrouver presque toujours est le symbole d’égalité. C’est un symbole binaire qui sera noté de manière infixe t=u.

Définition 4 (Formule atomique)   Soit une signature ( F, R) composée des symboles de relation R et des symboles de fonctions F. Soit R R et t1,…,tn des termes de T( F, X), alors R(t1,…,tn) est un formule atomique du calcul des prédicats sur la signature ( F, R).
On distingue également comme dans le calcul propositionnel deux formules atomiques
et qui représentent respectivement la propriété “vraie” et la propriété “fausse”.
Définition 5 (Formule du calcul des prédicats)   Une formule du calcul des prédicats sur la signature ( F, R) est soit

Les formules du calcul des prédicats se représentent aussi sous forme d’arbre, on associe la variable quantifiée à son quantificateur. Ainsi la formule x, ∃ y, ¬ (x = y) se représente ainsi :

Nous donnons aux quantificateurs une précédence faible, c’est-à-dire que leur portée va au delà des autres connecteurs logique. x,AB s’interprète comme x.(AB). Attention ce n’est pas une convention universelle. Certains choisissent au contraire une précédence pour les quantificateurs plus fortes que celle des connecteurs.

Variable libre, variable liée.

Par rapport à la logique propositionnelle, on a introduit des quantificateurs qui mettent en jeu des variables. Cela introduit une complexité syntaxique. En effet la variable est un nom qui permet de désigner un objet arbitraire et qui est lié par le quantificateur. Le connecteur x exprime qu’une certaine propriété qui dépend de x est vraie pour tous les objets x et le connecteur x exprime que la propriété est vraie pour au moins un objet x. Que l’on nomme l’objet x ou a ou n’importe quel autre nom n’a pas d’incidence sur la propriété exprimée.

On va donc se donner la liberté d’identifier des formules qui ne diffèrent que par le renommage des variables liées.

Ainsi la formule x, ∃ y, ¬ (x = y) est considérée comme égale à la formule a, ∃ b, ¬ (a = b).

Problème de capture.

Il faut être vigilant lorsque l’on procède au renommage, en effet lorsqu’on veut renommer la variable x dans la formule x, ∃ y, ¬(x = y), on peut remplacer x par a, mais par contre changer x par y n’est pas valide car aboutirait à la formule y, ∃ y, ¬ (y = y) qui exprime une propriété très différente de la propriété initiale. On dit alors que la variable y a été capturée.

Définition 6 (Variables libres, Vl(P))   Soit une formule P et x une variable. On dit que x est libre dans la formule P et on écrira xVl(P) si:

Une variable x est liée dans une formule Q si elle apparait libre dans une formule P telle que x,P ou x,P soit une sous-formule de Q.

Ce n’est pas vraiment la variable qui est libre ou liée, mais c’est chaque occurrence d’une variable x dans la formule qui peut être en position liée (sous un quantificateur x ou x) ou libre (apparaît dans une position qui n’est pas liée).

La définition de la substitution d’une variable x par un terme t dans une formule P doit prendre en compte cette question de la capture. Elle est définie de manière récursive sur la structure de la formule.

Définition 7 (Substitution P[xt] d’une variable par un terme dans une formule)   Soit x une variable et t un terme.

Cette définition est donc partielle dans le cas des formules avec quantificateurs si une variable liée dans la formule est aussi libre dans le terme que l’on veut substituer. Cependant en procédant à un renommage des variables liées dans les quantificateurs, on peut toujours se ramener à une situation dans laquelle la substitution sera licite.

Cette question peut paraître technique mais se pose de manière essentielle dès que l’on écrit des programmes qui manipulent des formules.

La définition de la notion de substitution se généralise à la substitution de plusieurs termes

P[x1← t1;…;xntn]
Définition 8 (Formule close)   Une formule est dite close si elle ne contient pas de variable libre.

3.2  Sémantique

Dans le cadre propositionnel, pour interpréter une formule il suffisait de donner une valeur logique à chaque variable propositionnelle.

Dans le cas du calcul des prédicats, il faut associer une valeur de vérité aux formules atomiques. Or celles-ci expriment des propriétés des objets et donc il faut commencer à donner un sens aux objets c’est-à-dire interpréter les symboles de constantes et de fonctions de la signature.

Par exemple on peut introduire une signature pour parler des nombres qui contient les symboles pour O, 1, l’addition, la multiplication, la soustraction et la division avec les notations usuelles. Il s’agit d’objets syntaxiques. Il y a plusieurs manières d’interpréter ces symboles qui peuvent avoir des propriétés très différentes. On peut vouloir parler des entiers naturels, des entiers relatifs, des rationnels ou des réels. Une formule logique peut être vraie dans certains modèles et fausse dans d’autres. Par exemple xy+y=x est vrai si on s’intéresse aux relatifs, rationnels, ou réels. Par contre cette propriété peut être invalidée sur les entiers naturels car on a par exemple 2−3=0.

3.2.1  Interprétation

Définition 1 (Interprétation)   Soit une signature ( F, R), une interprétation I est donnée par

On utilise également la terminologie de modèle ou de structure pour parler de l’interprétation d’une signature.

Du point de vue informatique, on peut voir les différentes interprétations d’une même signature comme les différentes implémentations d’une même bibliothèque.

Par exemple, les langages de programmation ont une notion primitive d’entiers relatifs mais pas de nombre rationnels. On peut proposer une interprétation des opérations sur les rationnels à l’aide d’un couple (p,q)∈ℤ×ℕ∖{0}. On pourra définir alors :

+((p1,q1),(p2,q2)) 
def
=
 
 (p1q2+p2q1,q1q2)       *((p1,q1),(p2,q2)) 
def
=
 
 (p1p2,q1q2)
=((p1,q1),(p2,q2)) 
def
=
 
  (p1q2=q1p2)

3.2.2  Valeur de vérité d’une formule

Se donner une interprétation de la signature est une étape nécessaire mais pas suffisante pour pouvoir définir la valeur de vérité d’une formule quelconque. En effet celle-ci peut contenir des variables libres auxquelles il faut aussi attribuer une valeur.

Définition 2 (Environnement)   Soit ( D,(fI)f F,(RI)R R) une interprétation d’une signature ( F, R), un environnement est une application ι qui associe un objet dans le domaine D à chaque variable (c’est-à-dire ι∈ X D).
Si
x X et d D et ι un environnement, on note ι+{xd} l’environnement qui vaut d pour la variable x et ι(y) pour toutes les variables yx.

Il ne faut pas confondre une substitution qui associe un terme à une variable avec un environnement qui associe à une variable une valeur du domaine d’interprétation (et donc une valeur sémantique et non syntaxique).

Etant données une signature ( F, R) et une interprétation I =def  ( D,(fI)f F,(RI)R R) de cette signature (que l’on supposera fixés dans la suite) on peut définir en fonction d’un environnement ι, la valeur d’un terme et d’une formule.

Définition 3 (Valeur d’un terme et d’une formule dans une interprétation)   Soit ι un environnement, ι∈ X D.

Contrairement au cas de la logique propositionnelle, on ne peut pas en général calculer cette valeur de vérité car dans le cas des quantificateurs, il faut a priori raisonner sur l’ensemble des objets d D qui peut être infini.

Exemple 1   Les bases de données traitent généralement de problèmes sur des ensembles finis. On peut avoir un domaine qui soit un ensemble de personnes et des relations parent(x,y) qui exprime que x est le père ou la mère de y et fratrie(x,y) qui exprime que x et y sont dans la même fratrie.

Si on veut modéliser une telle base de données en logique du premier ordre, la signature sera juste composée d’un ensemble de constantes par exemple Alice,Bob,Charles,Denis,Eric,Fanny,Georges,Hélène et de deux symboles de relation binaire parent et fratrie. Le modèle peut utiliser comme domaine l’ensemble des constantes {Alice,Bob,Charles,Denis,Eric,Fanny,Georges,Hélène} ou bien une autre représentation comme des entiers par exemple. ou des caractères.

On va prendre ici D =def {A,B,C,D,E,F,G,H}. On interprète chaque constante par un élément de D.

AliceI=A    BobI=B    CharlesI=C     DenisI=D
EricI=E     FannyI=F    GeorgesI=G     HélèneI=H

On a ensuite le choix sur l’interprétation des relations, par exemple :

parentI={(A,B),(G,B),(B,C),(B,H)}
fratrieI={(C,H),(H,C)}

On s’attend à ce que cette interprétation satisfasse les propriétés suivantes :

Exercice 1   Soient les formules suivantes sans variable libre. Sont-elles vraies si on les interprète dans , , avec les conventions usuelles pour l’interprétation des opérations et des relations.
  1. x, ∃ y, x < y
  2. x, ∃ y, y < x
  3. x y, x < yx+1 ≤ y
  4. x y z, xyx× zy × z
On constate que des propriétés vraie ou fausses dans une interprétation ne le sont pas forcément dans une autre même si les interprétations se correspondent sur les formules atomiques.

On vérifie que la définition de la valeur de vérité d’une formule est bien compatible avec l’opération de renommage des variables liées dans les formules. C’est-à-dire que si yVl(P) et P[xy] est bien définie alors val(ι,(∀ x, P))=val(ι,(∀ y, P[xy])) et val(ι,(∃ x, P))=val(ι,(∃ y, P[xy]))

Proposition 1   La valeur d’un terme ne dépend que de la valeur de l’environnement sur les variables libres de ce terme et de l’interprétation des symboles de fonction et des constantes qui apparaissent dans ce terme.
La valeur de vérité d’une formule ne dépend que de la valeur de l’environnement sur les variables libres de cette formule et de l’interprétation des symboles de fonction, constantes et relations qui apparaissent dans la formule.

En particulier pour un terme clos ou une formule close, la valeur est indépendante de l’environnement et on écrira simplement val(P) au lieu de val(ι,P).

Une autre propriété importante est le lien entre substitution et valeur de vérité.

Proposition 2 (Vérité et substitution)   Soit une formule A qui contient une variable libre x et soit t un terme. On suppose que la formule substituée A[xt] est définie (pas de capture). Soit ι un environnement. Interpréter la formule dans laquelle on remplace x par t revient à interpréter la formule de base en complétant l’environnement avec pour valeur associée à la variable x, l’interprétation du terme t.
val(ι,A  [x← t]) = val(ι+{xval(ι,t)},A)

Les notions de validité, satisfiabilité et modèle sont des généralisations du cas propositionnel. La notion d’interprétation prend en compte les symboles de fonctions et de relations et il faut également prendre en compte l’environnement qui donne l’interprétation des variables d’objet.

Définition 4 (Validité, satisfiabilité, modèle)   Soit A, une formule du calcul des prédicats sur une signature ( F, R).
Exercice 2   Dire si les formules suivantes sont valides, satisfiables, insatisfiables :
Proposition 3   
Définition 5 (Conséquence logique, équivalence)   Si E est un ensemble de formules et A une formule, on dit que A est conséquence logique de E et on note EA si toute interprétation et environnement qui rendent vraies les formules de E rendent aussi vraie la formule A.
On dit que
A et B sont des formules équivalentes et on écrit AB si AB et BA.

On montre par exemple les formules suivantes qui généralisent les lois de de Morgan au quantificateurs :

¬ ∃ x,P(x) ≡ ∀ x,¬ P(x)       ¬ ∀ x,P(x) ≡ ∃ x,¬ P(x)
Substitution et validité.

Si une formule A avec une variable libre x est valide, il en est de même de la formule A[xt].

On préserve également la validité en remplaçant un symbole de prédicat par une formule arbitraire. Soit une formule A qui est construite sur une signature qui comporte un symbole de relation n-aire R. Soit une formule B dans laquelle on identifie n variables libres x1,…,xn. Il est possible de remplacer dans la formule A toutes les sous-formules atomiques de la forme R(t1,…,tn) par la formule B[x1t1,…,xntn]. Si la formule A initiale est valide alors il en est de même de la formule obtenue après substitution. En effet si on se donne une interprétation quelconque J pour la formule dans laquelle R a été remplacé par B, on peut toujours construire une interprétation I pour la formule initiale A sur le même modèle en posant

RI(d1,…,dn)⇔ valJ({x1d1,…,xn↦ dn},B)

La valeur de vérité de A dans l’interprétation I (qui est vraie car A est valide) est alors égale à la valeur de vérité de la formule substituée dans l’interprétation J. Et donc la formule substituée est aussi valide.

Interprétation finie.

Si on s’intéresse à un domaine fini particulier D={d1;…;dn} et en supposant que l’on a dans la signature du langage des termes {c1;…;cn} (par exemple des constantes) sans variable libre tels que val(ci)=di, alors on peut éliminer les quantificateurs. En effet on a dans ce modèle :

∀ xP ⇔ (P[x← c1] ∧ … ∧ P[x← cn])       ∃ xP ⇔ (P[x← c1] ∨ … ∨ P[x← cn])

Si on applique cette technique à tous les quantificateurs d’une formule close on se retrouve avec une formule qui ne contient que des connecteurs propositionnels et qui ne contient plus de variables. On peut alors remplacer chaque sous formule atomique R(t1,…,tp) par R(ci1,…,cip) si val(tk)=dik. On peut maintenant introduire une variable propositionnelle pour chaque sous-formule atomique (cela peut faire beaucoup de variables) et utiliser un solveur propositionnel pour calculer les propriétés de la formule.

Exemple 2  

On peut utiliser des modèles finis pour justifier qu’une formule est satisfiable ou au contraire qu’elle n’est pas valide. Par contre pour établir la validité ou l’insatisfiabilité, il faut raisonner a priori sur toutes les interprétations.

3.2.3  Equivalences et formes normales

Proposition 4   Les équivalences suivantes sont vérifiées :
Exercice 3   En utilisant les équivalences précédentes et des équivalence propositionnelles, montrer les équivalences suivantes : Une application de la dernière équivalence est le principe dit du “buveur” : dans un bar quelconque, il existe une personne telle que si cette personne boit alors tout le monde boit. Il suffit de prendre pour A la formule x boit et pour B la formule x, x boit

D’autres équivalences de même nature ne sont pas vérifiées.

Exercice 4   Trouver des interprétations qui justifient les résultats suivants :

Forme normale de négation

On a vu que les lois de de Morgan se généralisent aux quantificateurs universel et existentiel ¬ (∃ x,A) ≡ ∀ xA et ¬ (∀ x,A) ≡ ∃ xA. On peut donc associer à toute formule une formule équivalente dans laquelle les négations ne portent que sur les formules atomiques. De même, il est toujours possible de se débarrasser des connecteurs et et des constantes et en utilisant les équivalences propositionnelles usuelles.

On a vu que les quantificateurs introduisent une difficulté dûe aux variables libres et liées qui limitent l’opération de substitution. Il est toujours possible d’effectuer des renommages qui nous permettent de ne pas utiliser deux fois le même nom de variable liée pour deux quantificateurs différents. On dira qu’une formule A est propre si lorsqu’elle contient deux sous formules distinctes quantifiées Q x,B et Q y,C alors les variables x et y sont différentes.

Skolemisation

La skolemisation est une opération (introduite par le logicien norvégien Thoraf Albert Skolem au 20ème siècle) qui permet de se débarrasser des quantifications existentielles en enrichissant les signatures et en préservant la satisfiabilité des formules.

L’idée de base est que si on s’intéresse à la formule x,∃ y,P(x,y) cette formule est vérifiée si pour tout élément d du domaine, on peut trouver un élément e du domaine tel que PI(d,e) est vraie. En général, la valeur e retenue pour y dépend de la valeur d choisie pour x. On peut exprimer e en fonction de d et donc le problème x,∃ y,P(x,y) est analogue au problème x,P(x,f(x)) dans lequel f est un nouveau symbole de fonction.

De manière plus précise on peut prouver x,P(x,f(x))⊨ ∀ x,∃ y,P(x,y) et si la formule x,∃ y,P(x,y) est satisfiable alors on peut à partir d’un modèle de cette formule, trouver un modèle de la formule x,P(x,f(x)) en choisissant la bonne interprétation pour la fonction f.

Définition 6 (Elimination d’un quantificateur existentiel)   Soit une formule A dans laquelle apparaît une sous-formule y,B. On suppose qu’il y a n variables libres dans y,B, c’est-à-dire Vl(∃ y,B)={x1,…,xn}. On introduit alors dans la signature un nouveau symbole de fonction f à n arguments (si n=0 alors f est juste une constante). On introduit la formule A qui est la formule A dans laquelle on a remplacé la sous-formule y,B par B[yf(x1,…,xn)].

Pour que cette opération soit licite il suffit que les variables x1,…,xn ne soient pas liées dans B ce qui peut toujours être garanti quite à effectuer des renommages de variables liées.

Proposition 5   Soit A une formule en forme normale de négation. Soit A obtenue à partir de A en éliminant un quantificateur existentiel suivant la procédure précédente. On a alors A′⊨ A et tout modèle de A peut être transformé en un modèle de A qui coincide avec celui de A sauf pour l’interprétation du nouveau symbole f.

Preuve: La première propriété est une conséquence de B[yf(x1,…,xn)]⊨ ∃ y,B et du fait que A est en forme normale de négation. Pour la seconde propriété on suppose construit un modèle I de la formule A. La formule B a comme variables libres les variables x1xn, y. On regarde dans le modèle l’ensemble des n+1-uplets (d1,…,dn,e) tels que val({x1d1,…,xndn,ye},B)=V. On peut à partir de cette relation construire une fonction fJ Dn D telle que val({x1d1,…,xndn,yf(d1,…,dn)},B)=V si il existe e tel que val({x1d1,…,xndn,ye},B)=V et f(d1,…,dn)=d avec d une valeur arbitraire de D si pour tout e, val({x1d1,…,xndn,ye},B)=F. On peut alors construire une interprétation J sur le même domaine D que I, qui étend l’interprétation I avec l’interprétation du symbole de fonction f comme la fonction fJ.

Cette interprétation rend vraie la formule (∃ y,B) ⇔ B[yf(x1,…,xn)] pour tout environnement {x1d1,…,xndn}. Elle rend donc aussi vraie la formule x1xn,((∃ y,B) ⇔ B[yf(x1,…,xn)]). Par ailleurs cette interprétation rend vraie la formule A car J est une extension de I qui est un modèle de A. Comme par ailleurs on peut montrer x1xn,((∃ y,B) ⇔ B[yf(x1,…,xn)]) ⊨ AA car A est obtenue à partir de A en remplaçant y,B par B[yf(x1,…,xn)], on en déduit que J est un modèle de A.

On peut itérer l’opération précédente pour éliminer tous les quantificateurs existentiels d’une formule. Chaque élimination de quantificateur introduit un nouveau symbole de fonction.

Si on applique ces transformations à une formule A en forme normale de négation, on obtient une formule B sans quantificateur existentiel telle que

Proposition 6   Soit A une formule en forme normale de négation et B une formule obtenue par élimination des quantificateurs existentiels de A. Preuve: Les deux premières propriétés sont des conséquences directes de BA alors que la dernière vient du fait que s’il existait un modèle de A alors il y en aurait aussi un de B.
Exemple 3   Soit la formule (∃ x,∀ y,P(x,y)) ∧ (∃ z,∀ uP(u,z)) on obtient la formule suivante avec a et b des nouvelles constantes et (∀ x,P(x,a)) ∧ (∀ uP(u,b)). Cette formule est satisfiable, par contre si on avait utilisé deux fois la même constante a on aboutirait à une formule insatisfiable.
Proposition 7 (Skolemisation)   Soit A une formule close alors il existe une formule B en forme normale négative qui ne contient que des connecteurs et et pas de quantificateur existentiel ou universel telle que si Vl(B)={x1,…,xn} on a Preuve: Il suffit d’éliminer les symboles d’implication et mettre la formule en forme normale négative. On applique ensuite l’élimination des quantificateurs existentiels suivant la procédure vue précédemment. On fait ensuite remonter les quantificateurs universels (en s’assurant au préalable qu’il n’y en n’a pas deux différents qui portent sur une variable de même nom) et en utilisant les équivalences A ∘ ∀ x, B ≡ ∀ x, (AB) lorsque x n’est pas libre dans B et ∘ ∈ {∨,∧}. Une fois que tous les quantificateurs universels sont en tête (on dit que la formule est en forme prénexe) il suffit de les éliminer pour obtenir la formule skolemisée.
Exemple 4   On part de la formule A  =def  (∀ x, (P(x) ⇒ Q(x))) ⇒ (∀ x, P(x)) ⇒ ∀ x, Q(x) et on skolemise ¬A Cette formule n’est pas vraie dans l’interprétation {xa,ya} donc la formule x y, ((¬ P(x) ∨ Q(x))∧ P(y) ∧ ¬ Q(a)) n’est pas satisfiable et donc il en est de même de la formule ¬ A donc A est valide.
Skolemisation d’un ensemble de formules

Si on se donne un ensemble de formules A1,…,An on peut traiter la skolémisation de manière indépendante pour chaque formule. On obtient pour chaque Ai une formule Bi sans quantificateurs telle que x1xpi,BiAi avec Vl(Bi)={ x1,…, xpi}. On en déduit aisément que :

3.3  Preuve

Les valeurs de vérité des formules du calcul des prédicats ne peuvent pas en général se calculer (nombreux modèles, domaines possiblement infinis ou trop gros). Pour établir la validité d’une formule on va donc plutôt s’appuyer sur des méthodes syntaxiques.

Décidabilité.

Il est en général indécidable d’établir qu’une formule du calcul des prédicats est valide. De manière équivalente, il est indécidable d’établir qu’une formule est satisfiable, puisque A valide est équivalent à ¬ A est insatisfiable.

La difficulté vient du fait que la validité de la formule x,P(x) exprime potentiellement la validité d’une infinité de formules P(d) pour chaque terme dD.

Certains fragments sont décidables (par exemple si la formule ne contient que des symboles de prédicat unaires), mais le problème est en général semi-décidable : nous montrerons un (semi-)algorithme qui peut établir qu’une formule est insatisfiable, c’est-à-dire que si l’algorithme s’arrête il pourra répondre si la formule est satisfiable ou non, que si la formule est insatisfiable alors l’algorithme s’arrête et répond que la formule est insatisfiable mais qu’il n’y a pas de garantie que l’algorithme s’arrête. Et donc on ne peut jamais savoir si la formule est satisfiable ou bien si on n’a pas attendu assez longtemps pour obtenir la réponse que la formule est insatisfiable.

3.3.1  Modèle de Herbrand

Pour établir qu’une formule est valide, il faut a priori raisonner sur tous les modèles. Le logicien Jacques Herbrand (1908-1931) a établi un résultat très important qui établit qu’on peut se limiter à regarder un seul domaine, appelé domaine de Herbrand que l’on peut voir comme un modèle syntaxique.

L’idée de base est d’interpréter les termes par eux-mêmes. On se donne une signature ( F, R), on suppose que l’ensemble F contient au moins une constante. On rappelle que les termes clos sont ceux formés sur la signature qui ne contiennent pas de variable, on note T( F) l’ensemble des termes clos.

Définition 1   On appelle base de Herbrand et on note B( F, R) l’ensemble des formules R(t1,…,tn) des formules atomiques closes avec R R et ti T( F).

Une interprétation de Herbrand est une interprétation H construite sur le domaine T(F) dans laquelle chaque symbole de fonction f d’arité n est interprété par une fonction fH définie par :

fH(t1,…,tn
def
=
 
  f(t1,…,tn)     ti T( F)

et dans laquelle on se donne une interprétation des symboles de prédicats en associant une valeur de vérité à chaque élément de la base de Herbrand, c’est-à-dire en se donnant une application B B( F, R)→ {V,F} ou de manière équivalente le sous-ensemble de la base de Herbrand correspondant aux formules atomiques vraies. L’interprétation du symbole de prédicat R sera alors RH =def {(t1,…,tn)∈ T( F)n|B(R(t1,…,tn))=V}.

Remarques :

Proposition 1   Une formule close sans quantificateur est satisfiable si et seulement si il existe une interprétation de Herbrand qui rend vraie la formule.

Preuve: Si la formule est close et sans quantificateur, alors toutes les sous-formules atomiques sont dans la base de Herbrand, la formule se comporte donc comme une formule propositionnelle (en considérant les éléments de la base de herbrand comme des variables propositionnelles). S’il y a une interprétation de Herbrand qui rend vraie la formule, alors la formule est satisfiable. Si maintenant on a un modèle I de la formule alors on construit une interprétation de Herbrand en prenant comme valeur pour les objets de la base de Herbrand B(R(t1,…,tn))=valI(R(t1,…,tn)). La valeur de la formule initiale est alors la même dans l’interprétation I et dans l’interprétation de Herbrand et est donc vraie.

Donc dans le cas de formules closes sans quantificateur, il suffit de s’intéresser aux interprétations de Herbrand.

On a vu avec la skolemisation que l’on pouvait se ramener à des formules closes de la forme x1xn,A dans lesquelles A n’a pas de quantificateur.

Si une formule A ne contient pas de quantificateur, et que ses variables libres sont {x1,…,xn}. Alors la satisfiabilité de la formule x1xn,A se ramène à la satisfiabilité d’un ensemble dénombrable de formules closes {A[x1t1,…,xntn] |t1,…,tn T( F)}. Une formule de la forme A[x1t1,…,xntn] avec t1,…,tn T( F) est appelée instance close de A.

En effet on montre d’abord que la satisfiabilité de x1xn,A se ramène à l’existence d’un modèle de Herbrand pour cette formule. Si la formule est satisfiable dans une interprétation I, on regarde l’interprétation de Herbrand H avec pour valeur de la base de Herbrand B(R(t1,…,tn))=valI(R(t1,…,tn)).

Il suffit de montrer que pour tout terme t1,…,tn T(F) la valeur de A dans l’environnement ι =def  {x1t1,…,xntn} est vraie dans l’interprétation H. Or valH(ι,A)=valH(A[x1t1;…,xntn]) en utilisant la propriété 2 et le fait que dans un modèle de Herbrand la valeur d’un terme clos est lui-même c’est-à-dire que valH(t)=t. Comme notre modèle de Herbrand a été choisi pour donner la même valeur aux formules atomiques que I et que A[x1t1;…,xntn] est une formule propositionnelle close, on a valH(A[x1t1;…,xntn])=valI(A[x1t1;…,xntn])=valI({x1valI(t1),…,xnvalI(∅,tn)},A)=V car x1xn,A est vraie dans le modèle I.

En utilisant les mêmes arguments que précédemment, x1xn,A est vraie dans une interprétation de Herbrand si pour tous les termes t1,…,tn T(F), A[x1t1;…,xntn] est vraie dans ce modèle. Et donc en assemblant les éléments précédents, on a que x1xn,A est satisfiable si et seulement si l’ensemble (fini ou dénombrable) de toutes les formules A[x1t1;…,xntn] pour t1,…,tn T(F) est satisfiable.

On va s’appuyer sur un théorème dit de compacité qui est un résultat théorique important en logique propositionnel pour se ramener à des ensembles finis.

Proposition 2 (Théorème de compacité)   Soit E un ensemble possiblement infini de formules propositionnelles, E est satisfiable si et seulement si tout sous-ensemble fini de formules de E est satisfiable.

Dire qu’un ensemble infini de formules E est satisfiable, c’est-dire qu’il y a une interprétation qui rend vraie toutes les formules de E. Dire que tous les sous-ensembles finis de formules est satisfiable, c’est dire que pour chaque sous-ensemble F E, on a une interprétation qui satisfait les formules de F. La force de ce théorème est de dire que l’on peut “assembler” les interprétations locales pour construire une solution globale.

Une conséquence immédiate de ce théorème est que si un ensemble infini de formules propositionnelles est insatisfiable alors il existe un sous-ensemble fini de ces formules qui est insatisfiable.

On revient au problème de la satisfiabilité d’une formule close dans le calcul des prédicats.

Proposition 3 (Théorème de Herbrand)   Soit B =def  ∀ x1xn,A une formule du calcul des prédicats avec A sans quantificateur.

On remarque que le domaine de Herbrand qui nous intéresse est celui formé de la signature correspondant uniquement aux symboles qui apparaissent dans la formule A, auquel on ajoute éventuellement une constante.

Exercice 1   On s’intéresse à la satisfiabilité des formules suivantes. On commence par préciser le domaine de Herbrand qui nous intéresse.
Semi-algorithme pour tester l’insatisfiabilité.

Le théorème de Herbrand nous donne une méthode algorithmique pour savoir si une formule (ou un ensemble de formules) est insatisfiable. On met tout d’abord la formule en forme de Skolem x1xn,A avec A sans quantificateur. On énumère ensuite toutes les instances de la formule A : A1,…,An,… et pour chaque préfixe A1,…,Ap, on cherche par une méthode propositionnelle (par exemple la résolution) si cet ensemble est satisfiable. Si la réponse est non on a gagné, la formule initiale x1xn,A est insatisfiable, si l’ensemble A1,…,Ap est satisfiable alors on ajoute une nouvelle instance Ap+1 et on relance le problème. Si on n’a pas de nouvelle instance à ajouter (cas où le domaine de Herbrand est fini), c’est que la formule initiale est satisfiable.

Cette méthode nous permet donc d’établir que le problème de validité d’une formule du calcul des prédicats est semi-décidable.

3.3.2  Unification

On voit que la méthode qui consiste à énumérer de manière naive l’ensemble des instances d’une formule n’est pas forcément efficace. En pratique, on préfère engendrer des instances qui vont pouvoir interagir avec d’autres parties de la formule pour conduire à une contradiction.

On s’intéresse ici à résoudre des équations sur les termes avec variables. On se donne une signature F pour les termes et un ensemble X de variables. On rappelle qu’une substitution est une application σ ∈ X T( F, X). On s’intéresse à des substitutions dites à support fini c’est-à-dire telles que σ(x)=x sauf pour un nombre fini de variables. De telles substitutions se représentent facilement comme des ensembles finis {x← σ(x) | x X ∧ σ(x)≠x}. Étant donnée une substitution, on peut définir une application de T( F, X)→ T( F, X) qui à un terme t associe le terme noté t[σ] dans lequel on a remplacé chaque variable x par σ(x).

Définition 2 (Composition de substitutions)   On peut composer deux substitutions σ1 et σ2 en une nouvelle substitution notée σ1σ2 définie par 1σ2)(x)=σ1(x)[σ2].
Pour tout terme
t : on a t1σ2]=(t1])[σ2].
Remarque.

Il ne faut pas confondre la composition de deux substitutions qui correspond à deux substitutions successives avec la substitution simultanée. Ainsi si on pose σ1={xy} et σ2={yz}. On a σ1σ2={xz;yz} et (x+y)[σ1σ2]=z+z alors que la substitution simultanée est définie par {xy;yz} et donne le résultat (x+y)[xy;yz]=y+z.

Définition 3 (Problème d’unification)   Un problème d’unification est donné par deux termes avec variables t et u. Ce problème admet une solution s’il existe une substitution σ telle que t[σ]=u[σ]. On dira que σ est solution du problème t=? u, on dira aussi que σ est un unificateur des termes t et u ou encore qu’il unifie les termes t et u.

De manière plus générale, on peut se donner un ensemble de couples de termes {(ti,ui)|iI}. Résoudre ce problème d’unification revient à chercher une substitution σ telle que ti[σ]=ui[σ] pour tout iI.

Il s’agit de la résolution d’une équation (ou d’un système d’équations), on trouve des valeurs pour les variables qui apparaissent dans t et u, telles que si on remplace les variables par ces valeurs, alors les deux termes obtenus sont syntaxiquement égaux.

On s’intéresse ici à l’égalité syntaxique, c’est-à-dire que les termes f(t1,…,tn) et g(u1,…,up) sont égaux uniquement lorsque les symboles f et g sont égaux, on a alors la même arité donc p=n et on doit avoir récursivement ti=ui pour i=1… n.

Exemple 1   Si on se donne deux expressions sur la signature pour les nombres plus(x,0) et plus(y,z) une solution est {x← 0;y← 0; z← 0}. Une autre solution est {xy; z← 0}. Certaines équations n’ont pas de solution, par exemple plus(x,0) et 0 car on s’intéresse à une égalité syntaxique entre les termes et les symboles plus et 0 sont distinctes.
Exercice 2   La signature sur les arbres est donnée avec la constante є et la fonction binaire N. Les problèmes d’unification suivants ont-ils des solutions :
  1. N(x,є)=? N(є,y)
  2. N(N(x,y),є) =? N(є,y)
  3. N(x,є) =? x
Ensemble des solutions.

Si σ1 est une solution du problème d’unification t=? u alors il en est de même de σ1σ2 pour toute substitution σ2. En effet on a t1]=u1] car σ1 est solution du problème et donc t1σ2]=t1][σ2]=u1][σ2]=u1σ2].

Si on a deux solutions σ et τ a notre problème d’unification, on dira que σ est plus générale que τ s’il existe une substitution σ′ telle que σσ′=τ.

Exemple 2   Si on reprend notre exemple, on a une solution σ =def  {xy; z← 0} et une solution τ =def  {x← 0;y← 0; z← 0}. On a τ=σ{y← 0} donc σ est plus général.

Une bonne propriété de l’unification sur les termes syntaxiques est que si un problème a une solution alors il existe une solution qui est plus générale que toutes les autres. Et donc pour calculer l’ensemble de toutes les solutions, il suffit de calculer cette substitition que l’on appelle aussi unificateur principal.

Proposition 4 (Unification)   Soit E={ti=? ui|iI} un ensemble fini de problèmes d’unification. Si ce problème admet une solution, alors il existe un unificateur principal σ et celui-ci est calculé par la fonction suivante :
unif(∅)={}fonction identité  σ(x)=x  pour tout  x X (1)
unif({x
?
=
 
 x} ⋃ E)
unif(E)équation triviale (2)
unif({x
?
=
 
 t} ⋃ E)
echecsi  xVl(tpas de solution finie (3)
unif({x
?
=
 
 t} ⋃ E)
= {x← tunif(E[x← t])si  xVl(t) (4)
unif({t
?
=
 
 x} ⋃ E)
unif({x
?
=
 
 t} ⋃ E)
si  t  n’est pas une variable (5) 
unif({f(t1,…,tn)
?
=
 
 g(u1,…,up)} ⋃ E)
echecsi  fg (6)
unif({f(t1,…,tn)
?
=
 
 f(u1,…,un)} ⋃ E)
unif({t1
?
=
 
 u1;…;tn
?
=
 
 un}⋃ E)
(7)

Preuve: On vérifie que chaque cas possible est couvert par une équation unique. Un problème plus délicat à justifier est la terminaison de cette définition vue comme un procédé de calcul. Dans les cas récursifs, on regarde ce qui diminue :

En résumé pour un problème E si on regarde le triplet nbvars(E),taille(E),nbeqs(E) avec nbvars(E) le nombre de variables différentes dans E, taille(E) le nombre d’occurrences de symboles dans E, et nbeqs(E) le nombre d’équations dans E, alors on remarque que chaque appel se fait sur un problème strictement plus petit si on prend l’ordre lexicographique, sauf celui où on change l’équation t=x en x=t. Mais cette règle n’est appliquée que lorsque t n’est pas une variable et sera donc immédiatement suivie de l’application d’une règle qui fait diminuer le “poids” du problème. Une autre possibilité est de définir taille(t=u) =def  2× nbsymb(t)+nbsymb(u) au lieu de taille(t=u) =def  nbsymb(t)+nbsymb(u). On a alors taille(x=t)<taille(t=x) lorsque t n’est pas une variable.

On vérifie que les cas d’échec correspondent à des problèmes sans solution et que dans les cas où une solution est trouvée, il s’agit bien de l’unificateur principal.

Cet algorithme n’est pas efficace à cause en particulier de l’opération de substitution lorsqu’on élimine l’équation x=? t. On peut utiliser une représentation des termes qui rend cette opération moins coûteuse. Il existe d’autres algorithmes plus complexes mais plus efficaces.

L’unification est une opération utilisée dans de nombreuses applications, par exemple dans l’algorithme de typage des programmes Caml afin de trouver le type le plus général que peut traiter une fonction. L’unification se généralise également à des théories plus complexes dans lesquelles l’égalité entre termes n’est plus syntaxique mais prend en compte des propriétés des opérations comme la commutativité ou l’associativité. Suivant les théories, on va perdre la décidabilité ou l’existence d’un unificateur principal.

L’unification sur les termes se généralise en une unification entre des littéraux. Si on a deux littéraux P et Q, ils s’unifient s’il existe une substitution σ telle que P[σ]=Q[σ]. Si P =def  R(t1,…,tn) (resp. P =def  ¬ R(t1,…,tn)) alors σ est un unificateur de P et Q si et seulement si P =def  R(u1,…,un) (resp. P =def  ¬ R(u1,…,un)) et σ est un unificateur de l’ensemble de problèmes {ti=? ui|i=1… n}.

Exercice 3   Résoudre les problèmes d’unification suivants :
  1. (plus(x,0)=x)=? (plus(0,y)=y)
  2. (plus(x,0)=x)=? yz
  3. (plus(x,0)=x)=? (y=plus(y,0))

3.3.3  Résolution

En logique propositionnelle, une clause est un ensemble de littéraux (variable propositionnelle ou négation de variable propositionnelle) et on peut se ramener au cas où chaque variable propositionnelle apparaît une seule fois. La résolution propositionnelle traite un ensemble de clauses et déduit à partir de cet ensemble de nouvelles clauses en utilisant la règle de résolution :

C ∨ l      C′ ∨ ¬ l
C∨ C

Dans le cas du premier ordre, les clauses peuvent contenir des variables et donc chaque symbole de prédicat peut apparaître plusieurs fois, en concernant des termes différents. Par ailleurs ces termes peuvent contenir des variables et dans ce cas la clause représente l’ensemble de toutes les instances possibles de la formule.

On part d’un ensemble de clauses (disjonction de littéraux vue comme un ensemble de littéraux). Chaque clause C dont les variables libres sont x1,…,xn est interprétée comme la formule universellement quantifiée x1xn,C que l’on notera aussi ∀ (C).

L’unification sur les termes s’étend de manière naturelle à l’unification sur les littéraux. Deux littéraux L1 et L2 s’unifient s’ils sont de la forme P(t1,…,tn) et P(u1,…,un) ou bien ¬ P(t1,…,tn) et ¬ P(u1,…,un) et que le problème (ti=? ui) admet une solution. Dans ce cas on note unif(L1,L2) l’unificateur principal.

Règles pour la résolution

Les transformations de clauses en calcul des prédicats se font en utilisant trois règles :

  1. Factorisation : si σ est l’unificateur principal de L1 et L2 alors :
    L1 ∨ L2 ∨ C
    L1[σ]∨ C[σ]
  2. Renommage : si σ est une bijection sur les variables alors :
    C
    C[σ]
  3. Résolution binaire : si les clauses L1C et ¬ L2C n’ont pas de variables communes et si σ est l’unificateur principal de L1 et L2 alors :
    L1 ∨ C      ¬ L2 ∨ C
    C[σ]∨ C′[σ]

On remarque que les deux premières règles sont triviales dans le cas propositionnel et que la dernière règle généralise la règle de résolution propositionnelle.

Preuve par résolution.

Les définitions de preuves par résolution sont une simple généralisation du cas propositionnel. Soit E un ensemble de clauses:

La règle de renommage sert juste à préparer les clauses pour appliquer la règle de résolution qui nécessite que les deux clauses ne partagent pas de variables. La règle de factorisation permet de faire disparaitre plusieurs littéraux lors d’une étape de résolution binaire.

Correction de la résolution

La correction de la méthode de résolution établit que si l’on peut déduire une clause C à partir d’un ensemble de clauses E alors la formule ∀(C) est conséquence logique de l’ensemble des formules {∀ (D)|D E}

Une propriété clé est que si σ est une substitution alors ∀ (C) ⊨ ∀ (C[σ]) qui se déduit du lien entre substitution et vérité :

val(e,C[σ])=val({x↦ val(e,σ(x))},C)

. Cette règle permet de ramener la correction de la résolution dans le cas du premier ordre à celle du cas propositionnel.

Exemple 3  
  1. E={P(x,y)∨ P(y,x), ¬ P(u,z) ∨ ¬ P(z,u)} il faut commencer par factoriser avant de faire la résolution.
  2. E={¬ P(z,a)∨ ¬ P(z,x) ∨ ¬ P(x,z), P(z,f(z)) ∨ P(z,a), P(f(z),z) ∨ P(z,a) }

La méthode de résolution est complète, c’est-à-dire que si E est un ensemble de clauses et que est une conséquence de {∀(C)|C E} alors on peut déduire la clause vide par la méthode de résolution à partir de l’ensemble E.

3.3.4  Calculs de séquents

Déduction naturelle

On avait donné dans le chapitre 1 les règles de déduction naturelle pour les connecteurs logiques. Il y a pour chaque connecteur une règle d’introduction et une règle d’élimination.

On vérifie aisément que toutes ces règles sont correctes c’est-à-dire que si les prémisses sont valides, alors il en est de même de la conclusion et donc si on peut construire un arbre de preuve complet qui suit ces règles, alors le séquent qui apparaît à la racine de l’arbre est valide.

Système G

Nous avons vu que le système G est un autre calcul des séquents qui a l’avantage d’utiliser des règles “réversibles”, c’est-à-dire que l’on ne risque pas en les appliquant de passer d’un séquent valide à un séquent non valide.

Les séquents s’écrivent Γ ⊢ Δ, ils ont plusieurs formules à droite (interprétées comme une disjonction) et les règles se séparent en règles gauche et règle droite suivant si on fait disparaître le quantificateur à gauche ou à droite du signe .

On a comme règle droite de et règle gauche de , des règles analogues à celles de la déduction naturelle :

Γ ⊢ Δ,P      x ∉Vl(Γ,Δ)
Γ ⊢ Δ,(∀ x,P)
        
P,Γ ⊢ Δ      x ∉Vl(Γ,Δ)
(∃ x,P), Γ ⊢ Δ

Ces deux règles sont réversibles. Par contre, pour la règle gauche de et la règle droite de , il faut faire plus attention.

Si on prend l’exemple de la conjonction, il y a deux règles d’élimination en déduction naturelle :

Γ ⊢ A∧ B
Γ ⊢ A
   
Γ ⊢ A∧ B
Γ ⊢ B

qui deviennent dans le système G, une seule règle

A∧ B,Γ ⊢ Δ
A,B,Γ ⊢ Δ

Si on généralise la conjonction à une quantification universelle, on a un schéma de règle en déduction naturelle

Γ ⊢ ∀ x,P
Γ ⊢ P[x← t]

qui correspond à un ensemble de règles (une pour chaque terme t), cet ensemble pouvant être infini. On ne peut pas ajouter une infinité d’hypothèses dans la partie gauche du séquent. Pour contourner ce problème, on va bien introduire P[xt] dans les hypothèses mais on va aussi garder une copie de x, P qui nous permettra si on en a besoin de récupérer d’autres instances de P. Cela revient juste à utiliser le fait que (∀ x,P) ≡ P[xt]∧ (∀ x,P).

Le même raisonnement s’applique pour la règle droite du quantificateur existentielle. La règle d’introduction de la déduction naturelle :

Γ ⊢ P[x← t]
∃ x,P

correspond à tout un ensemble de règles et on voudrait remplacer à droite la formule x,P par un ensemble de formules P[xt] mais qui pourrait être infini. Pour contourner ce problème, il suffit de transformer x,P en P[xt] ∨ (∃ x,P).

Pour résumer les règles du système G pour les quantificateurs sont données dans le tableau suivant :

 gauchedroite 
P[x← t],(∀ x,P),Γ ⊢ Δ 
(∀ x,P),Γ ⊢ Δ 
Γ ⊢ Δ,P      x ∉Vl(Γ,Δ) 
Γ ⊢ Δ,(∀ x,P
P,Γ ⊢ Δ      x ∉Vl(Γ,Δ) 
(∃ x,P),Γ ⊢ Δ 
Γ ⊢ Δ,(∃ x,P),P[x← t
Γ ⊢ Δ,(∃ x,P
 

Il est facile de montrer que ces règles sont correctes et réversibles. Le séquent du haut est valide si et seulement si celui de la conclusion est valide.

Contrairement au cas propositionnel, on ne fait pas décroitre la taille du séquent en appliquant les règles et donc il n’y a pas de stratégie pour être sûr d’arriver à un arbre de preuve. Par contre, si la formule est valide, il existe un arbre de preuve fini. Le calcul des prédicats est complet, toute formule qui est valide (vraie dans tous les modèles) peut être prouvée (à l’aide d’un arbre de preuve fini).

Exemple 4   Pour montrer l’application de ces règles, nous allons montrer le séquent ¬∃ x,p(x) ⊢ ∀ yp(y)
¬ g 
d 
¬ d 
d 
hyp  
 p(y) ⊢ p(y),∃ x,p(x)
 p(y) ⊢ ∃ x,p(x)
  ⊢ ∃ x,p(x),¬ p(y)
  ⊢ ∃ x,p(x),(∀ y,¬ p(y))
 ¬∃ x,p(x) ⊢ ∀ y,¬ p(y)
Exercice 4   Montrer le principe des buveurs, c’est-à-dire que x,(p(x) ⇒ ∀ y,p(y))

Previous Up Next