Chapitre 10

Algèbre de Boole

I Propriétés générales

D ÉFINITION 10.1 (A LGÈBRE DE B OOLE ). On appelle algèbre de Boole la structure algébrique (A, +, ., )
définie par un ensemble (non vide) A et trois opérations :
– la somme booléenne (binaire) : “+”,
– le produit booléen (binaire) : “.” et
– la négation booléenne (unaire) : “ ” (par exemple a).
et qui doivent posséder les propriétés données dans les deux premières colonnes du tableau ci-dessous.♦

Propriété A P(E)
idempotence a+a=a A∪A=A
a·a=a A∩A=A
commutativité a+b=b+a A∪B =B∪A
a·b=b·a A∩B =B∩A
associativité a + (b + c) = (a + b) + c A ∪ (B ∪ C) = (A ∪ B) ∪ C
a · (b · c) = (a · b) · c A ∩ (B ∩ C) = (A ∩ B) ∩ C
éléments neutres a+0=a A∪ 6 o = A
a·1=a A∩E =A
absorption a+1=1 A∪E =E
a·0=0 A∩ 6 o =6 o
distributivités a · (b + c) = a · b + a · c A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C)
a + b · c = (a + b) · (a + c) A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C)
involution a=a E \ (E \ A) = A
complémentation 0=1 E\ 6 o = E
1=0 E \ E =6 o
partition a+a=1 A ∪ (E \ A) = E
a·a=0 A ∩ (E \ A) =6 o
« Lois de De Morgan » a+b=a·b E \ (A ∪ B) = (E \ A) ∩ (E \ B)
a·b=a+b E \ (A ∩ B) = (E \ A) ∪ (E \ B)

Propriétés d’une algèbre de Boole

73
1 / 92
 Le tableau précédent met en parallèle les mêmes propriétés, écrites en utilisant
– soit les notations générales d’une algèbre de Boole,
– soit les notations ensemblistes, définies lorsque A est l’ensemble P(E) des parties d’un ensemble
E : c’est une algèbre de Boole particulière, bien connue, et qui possède des notations spécifiques.

R EMARQUE 10.1. Les signes opératoires utilisés sont les mêmes que ceux de l’addition et de la multi-
plication des réels. Cependant, ces opérations n’ont évidemment pas les mêmes propriétés, et ne portent
pas sur les mêmes éléments.

Exercice 10.1 (Somme disjonctive). On considère une algèbre de Boole quelconque (E, +, ·, ).
On définit l’opération « somme disjonctive », notée ⊕, par a ⊕ b = ab + ab.
1. Que vaut a ⊕ 0 ? a ⊕ 1 ?
2. Calculez a ⊕ a et a ⊕ a.
3. Calculez a ⊕ b.
4. Montrez que ⊕ est associative et commutative.

Exercice 10.2 (Opérateurs de Sheffer et de Peirce). Soit (E, +, ·, ) une algèbre de Boole.
1. On définit l’opération de Sheffer 1 par : a|b = a + b.
Comment obtenir a, a + b, a · b en n’utilisant que l’opérateur | ? Faire de même pour a + b ; étudier
l’associativité de cette opération.
2. On définit la flèche de Peirce 2 par : a ↓ b = a · b.Mêmes questions.

R EMARQUE 10.2. Ces connecteurs sont donc remarquables, puisqu’ils sont universels (tous les autres
connecteurs peuvent s’exprimer avec uniquement la barre de Scheffer, ou uniquement avec la flèche
de Peirce). Cependant, par manque de concision et de lisibilité, ces connecteurs ne sont pas utilisés en
logique.

II Règles de calcul dans une algèbre de Boole

1. Les priorités habituelles sont respectées pour la somme et le produit booléen.
2. Les éléments neutres sont notés 0 et 1, par analogie avec les entiers de même symbole (ne pas
oublier que ces calculs ne se déroulent pas dans R...)
3. L’absence d’éléments symétriques pour la somme et pour le produit interdit les simplifications que
l’on a l’habitude de pratiquer « sans y réfléchir » :
– a + b = a + c ne donne pas b = c,
– ab = ac n’entraîne pas b = c.
En particulier, ne jamais perdre de vue que
– a + b = 0 n’est réalisable en algèbre de Boole que si a = b = 0
– a.b = 1 n’est réalisable en algèbre de Boole que si a = b = 1 (A∩B = E ⇔ A = E et B = E)
– a.b = 0 peut être réalisé avec a 6= 0 et b 6= 0 (par exemple, avec b = a, mais ce n’est pas la
seule solution...). On parle de « diviseurs de zéro ». (Ainsi, A ∩ B = ∅ est possible sans avoir
obligatoirement A = ∅ et B = ∅).
4. Il y a deux distributivités. Celle de la somme (booléenne) sur le produit (booléen) n’est pas
habituelle. Par exemple, simplifier (a + b)(a + c)(a + d)(a + e)(a + f )
5. Signalons pour finir que, comme ci-dessus, le point pour le produit est souvent omis.
1. D’après le logicien H.M. Sheffer
2. Lorsque les logiciens, dans les années 1930, cherchèrent un symbole pour exprimer le connecteur découvert par C.S.
Peirce (1839-1914), “Pierce Arrow” était le nom d’une célèbre marque de voiture !

74
2 / 92
 Dans une expression booléenne, une sous-expression est dite « redondante » lorsqu’on peut la sup-
primer sans changer la « valeur » de l’expression :
1. Dans une somme booléenne, tout terme absorbe ses multiples.
Autrement dit : a + a · b = a.

P REUVE En effet, a+a·b = a·(b+b)+a·b = a·b+a·b+a·b = a·b+a·b (par idempotence) =

a · (b + b) = a.

2. Dans un produit booléen, tout facteur absorbe tout autre facteur qui le contient en tant que terme.
Autrement dit : a · (a + b) = a.

P REUVE En effet, a · (a + b) = a · a + a · b = a + a · b = a.

3. Enfin, la troisième règle de redondance s’exprime par :

a+a·b=a+b

P REUVE a + a · b = (a + a) · (a + b) = 1 · (a + b) = a + b.

E XEMPLE 10.3. ab + ac + bc = ab + (a + b) · c = ab + ab · c = ab + c

Exercice 10.4. Montrer que a · b + a · c + b.c = a · b + a · c

Exercice 10.5 (Somme disjonctive). Montrez que l’on a a = b si et seulement si a ⊕ b = 0.

Exercice 10.6 (Calcul booléen élémentaire). Appliquer au maximum les règles précédentes pour sup-
primer les redondances dans les calculs suivants.
1. (a + b + c) · (a + b + c) · (a + b + c)
2. a + a · b · c + a + a · b
3. a · b + a · b · c + a · b · c
4. (a + b + c) · (a + b + c + d)

Exercice 10.7 (Calcul booléen). Même énoncé qu’à l’exercice précédent.

1. (a + b)(c + a · b + a · b) .
2. (a + b + c) · (a + b) · (b + c).
3. (a + c) · (a + d) · (b + e) · (b · c + b · c) · (d + c · e) · (c + d).
4. (a · a · (b + c) + a · (b + c)) · (b · a + c + (a + c) · b) · (a · b · c + a · b · c).

III Fonctions booléennes

III.1 Définitions
Soit A une algèbre de Boole.

D ÉFINITION 10.2 (F ONCTION BOOLÉENNE ). On appelle fonction booléenne de n variables toute ap-
plication de An dans A dont l’expression ne contient que :
– les symboles des opérations booléennes,
– des symboles de variables, de constantes,
– d’éventuelles parenthèses. ♦

75
3 / 92
E XEMPLE 10.8. f (a, b, c) = a · b + c.

R EMARQUE 10.3. Si a est une variable booléenne, elle peut intervenir dans l’expression d’une fonction
booléenne sous la forme a ou sous la forme a, qui sont appelées les deux aspects de cette variable :
affirmé et nié.

D ÉFINITION 10.3 (F ONCTION BOOLÉENNE NULLE ). On appelle fonction booléenne nulle (à n vari-
ables) la fonction booléenne qui, à chaque valeur des variables, associe la valeur 0.
Son expression est f (x1 , x2 , . . . , xn ) = 0. ♦

D ÉFINITION 10.4 (F ONCTION RÉFÉRENTIEL ). On appelle fonction référentiel (à n variables) la fonc-

tion booléenne qui, à chaque valeur des variables, associe la valeur 1.
Son expression est f (x1 , x2 , . . . , xn ) = 1. ♦

III.2 Fonctions booléennes élémentaires

D ÉFINITION 10.5 (M INTERME , MAXTERME ). Un minterme à n variables est une fonction booléenne
à n variables dont l’expression se présente sous la forme du produit d’un aspect et d’un seul de chacune
des n variables.
Définition analogue pour un maxterme , en remplaçant dans la définition précédente « produit » par
« somme ». ♦

D ÉFINITION 10.6 (F ONCTIONS BOOLÉENNES ÉLÉMENTAIRES ). Pour un nombre de variables n fixé,

les fonctions booléennes élémentaires sont les mintermes et les maxtermes (à n variables). ♦

E XEMPLE 10.9 (M INTERME À TROIS VARIABLES ). a · b · c

E XEMPLE 10.10 (M AXTERME À TROIS VARIABLES ). a + b + c.

Exercice 10.11. Pour 3 variables a, b et c, repérez les mintermes et les maxtermes : bc, a + b + c, abbc,
abc, a + bc.

Exercice 10.12. Dressez la liste des mintermes et des maxtermes pour deux variables a et b.

P ROPRIÉTÉ 10.1 (N OMBRE DE MINTERMES ET DE MAXTERMES ) : Les mintermes et maxtermes,

pour un nombre donné n de variables, sont au nombre de 2n chacun.

N OTATION (R EPRÉSENTATION DES MINTERMES ET DES MAXTERMES ) : Les mintermes et les max-
(n) (n)
termes sur n variables sont respectivement notés mi et Mi . L’indice i varie entre 0 et 2n − 1, selon
une convention d’ordre de numérotation des mintermes et maxtermes.

La convention est la suivante : à chaque variable, on associe 0 ou 1 selon que cette variable apparaît
sous son aspect nié ou sous son aspect affirmé dans l’expression du minterme ou du maxterme. En
écrivant ces chiffres les uns à côté des autres, dans le même ordre que les variables correspondantes,
on obtient un code binaire du minterme ou du maxterme, qu’on peut considérer comme l’écriture d’un
entier positif en base 2.
Pour que cette convention de numérotation ait un sens, il est indispensable de fixer un ordre d’énuméra-
tion des variables une fois pour toutes, et de s’y tenir.

76
4 / 92
E XEMPLE 10.13. Si les variables sont a, b, c et d et qu’on décide de les énumérer dans l’ordre alphabé-
tique, il sera, par exemple, strictement interdit d’écrire un produit sous la forme c · a · d · b, et ceci, même
de manière transitoire au cours d’un calcul : la seule expression admissible est alors a · b · c · d.

D ÉFINITION 10.7 (I NDICE D ’ UN MINTERME OU D ’ UN MAXTERME ). L’ indice d’un minterme ou d’un

maxterme est la valeur décimale du code binaire de ce minterme ou de ce maxterme. ♦

E XEMPLE 10.14. Pour 3 variables a, b et c rangées par ordre alphabétique :

minterme (ou Maxterme) code binaire associé indice décimal représentation

a·b·c 010 2 m2
a·b·c 100 4 m4
a+b+c 111 7 M7

Exercice 10.15. Pour 3 variables a, b et c rangées par ordre alphabétique, trouvez l’indice des minter-
mes et maxtermes suivants : a + b + c, a + b + c, a · b · c et a · b · c.

III.3 Correspondance entre maxtermes et mintermes

P ROPRIÉTÉ 10.2 : La négation (booléenne) d’un minterme est un maxterme (et réciproquement).

P REUVE Lois de De Morgan : la négation échange les opérations booléennes binaires...

E XEMPLE 10.16. a · b · c = a + b + c

Si l’indice du minterme (ou du maxterme) dont on prend la négation est i et si l’indice de cette
négation est j, on a des expressions du type :
i = 0011 0100 1110 . . . . . . 0110
j = 1100 1011 0001 . . . . . . 1001
i + j = 1111 1111 1111 . . . . . . 1111
L’expression en système binaire de la valeur de i + j est donc, quelles que soient les valeurs de ces
deux indices, 111.....1 (n chiffres). La valeur correspondante est 2n − 1. Autrement dit,

P ROPRIÉTÉ 10.3 : La négation d’un minterme est un maxterme, et réciproquement.

(n) (n) (n) (n)

∀i ∈ {0, ..., 2n − 1}, mi = M2n −1−i et Mi = m2n −1−i .

III.4 Principaux résultats concernant mintermes et maxtermes

P ROPRIÉTÉ 10.4 : Les mintermes à n variables sont disjoints.

(n) (n)
Si i 6= j, alors mi · mj = 0.

77
5 / 92
Exercice 10.17. Vérifiez la dernière propriété dans le cas de deux variables.

P REUVE Si i 6= j, les écritures en système binaire des entiers i et j comportent au moins un chiffre
différent, en l’occurrence au moins un « 1 » à la place d’un « 0 ».
Il y a donc au moins une variable qui figure sous deux aspects différents.
Or, on sait que a · a = 0. Donc, lorsque l’on calcule le produit des deux mintermes, celui-ci est
nécessairement nul.

R EMARQUE 10.4. On prend la négation de chacun des membres de l’égalité, et l’on obtient : si i 6= j,
(n) (n)
alors Mi + Mj = 1. Ainsi, la somme de deux maxtermes distincts vaut 1.

P ROPRIÉTÉ 10.5 : Les mintermes forment une partition de l’unité :

n −1
2X
(n)
mi =1
i=0

P REUVE En effet, il y a un nombre pair de mintermes. Dans cette somme, on ordonne les mintermes
par indice croissant, puis on les regroupe deux à deux. Dans chacun de ces groupes, seul diffère
l’aspect de la dernière variable. On met les autres en facteur de la somme xn + xn , c’est-à-dire 1 : le
facteur qui subsiste est un minterme à (n − 1) variables.
n −1
2X
(n) X−1
2n−1
(n−1)
Donc mi = mi .
i=0 i=0
Par récurrence, cette somme est égale à x1 + x1 , c’est-à-dire finalement 1.

Exercice 10.18. Le vérifier dans le cas de deux variables.

R EMARQUE 10.5. Par négation (booléenne) de cette propriété, on obtient : le produit de tous les max-
termes à n variables est nul.

III.5 Formes canoniques d’une fonction booléenne

D ÉFINITION 10.8 (M ONÔMES ). Un monôme est une fonction booléenne produit de variables booléennes
éventuellement niées. ♦

Exercice 10.19. Parmi les expressions suivantes dire lesquelles sont des monômes et lesquelles ne le
sont pas en justifiant : a + b, a + bc, a(b + c), ab, b.

P ROPRIÉTÉ 10.6 : Quelle que soit l’expression de la fonction booléenne, il est possible de la mettre
sous la forme d’une somme de monômes.

P REUVE En effet, comme elle ne fait intervenir que les trois opérations booléennes, il suffit de lui
appliquer les règles du calcul booléen :
1. On développe les négations (en appliquant les règles a + b = a · b et a · b = a + b), jusqu’à ce
qu’il n’y ait plus de négations que sur les variables ;
2. Puis on développe les produits qui portent sur des sommes, en utilisant la distributivité du
produit sur la somme ;

78
6 / 92
 3. On obtient ainsi une expression qui s’écrit sans parenthèses, et qui ne contient que des sommes
de produits de variables éventuellement niées.

P ROPRIÉTÉ 10.7 : Chaque monôme peut ensuite être mis sous la forme d’une somme de minter-
mes.

P REUVE En effet, si, dans l’expression de ce monôme, toutes les variables interviennent, c’est déjà
un minterme.
Dans le cas contraire, il manque (par exemple) la variable a dans son expression : on la fait
intervenir sous la forme (a + a). On développe, les deux monômes obtenus font intervenir la variable
a.
Ou bien, il s’agit de mintermes et le processus est terminé, ou bien il manque encore une variable,
qu’on fait intervenir en utilisant le même procédé, et ainsi de suite jusqu’à aboutir aux mintermes.

On fait évidemment disparaître du résultat, par idempotence, les occurrences multiples de mintermes,
pour pouvoir énoncer le résultat suivant :

P ROPRIÉTÉ 10.8 (F ORME CANONIQUE DISJONCTIVE ) : Toute fonction booléenne à n variables

(autre que la fonction nulle) peut se mettre sous la forme d’une somme de mintermes à n variables.
Cette forme, unique, s’appelle Forme Canonique Disjonctive (dans la suite, FCD).

R EMARQUE 10.6. L’unicité de cette FCD permet la comparaison des fonctions booléennes entre elles.

Par négation booléenne de ce résultat, on obtient :

P ROPRIÉTÉ 10.9 (F ORME CANONIQUE CONJONCTIVE ) : Toute fonction booléenne de n variables

(autre que la fonction référentiel) peut se mettre sous la forme d’un produit de maxtermes à n vari-
ables.
Cette forme, unique, est la Forme Canonique Conjonctive (FCC dans la suite).

III.5.1 Obtention des formes canoniques

La méthode algébrique consiste à :
– tout développer pour mettre l’expression sous la forme d’une somme de monômes,
– dans chaque terme de cette somme, faire apparaître les valeurs qui n’y figurent pas.

E XEMPLE 10.20. On illustre cela :

f (a, b, c) = a + bc = a(b + b)(c + c) + (a + a)bc
= abc + abc + abc + abc + abc + abc = m3 + m4 + m5 + m6 + m7 .

Pour la FCC, on peut imaginer une méthode analogue.

E XEMPLE 10.21. f (a, b, c) = a + bc = (a + b)(a + c) = (a + b + cc)(a + bb + c)

= (a + b + c) · (a + b + c) · (a + b + c) · (a + b + c) = M5 M6 M7

79
7 / 92
R EMARQUE 10.7. Si on prend la négation de la FCD, on obtient bien sûr une FCC... mais pas celle de
la fonction, celle de sa négation !
Il suffit de prendre la négation de la fonction, de calculer sa FCD puis de prendre la négation du
résultat.

Exercice 10.22. Obtenir la FCC de x + yz.

Il existe une autre méthode pour obtenir ces formes canoniques : la méthode des diagrammes.

IV Diagrammes de Karnaugh
La représentation des fonctions booléennes par diagrammes de Karnaugh-Veitch : est fondée sur les
propriétés des mintermes (ils réalisent une partition de l’unité),
Ces derniers diagrammes deviennent rapidement inextricables quand le nombre de variables aug-
mente, c’est pourquoi, dans les diagrammes de Karnaugh, on divise systématiquement l’« univers » (le
référentiel E) en deux parties égales en superficie pour représenter la partie concernée et son complé-
mentaire.
À chaque introduction de variable supplémentaire, chaque case du précédent diagramme est divisée
en 2.

E XEMPLE 10.23. On obtient, par exemple :

a a
b ab ab
b ab ab

Pour obtenir un diagramme de Karnaugh, on place dans ce diagramme les numéros des mintermes :

HH a
HH 0 1
b H
H
0 0 2
1 1 3

E XEMPLE 10.24. Cas de trois variables :

– les deux premières colonnes correspondent à a, les deux dernières à a,
– la première et la dernière colonne correspondent à b, les deux centrales à b,
– enfin, la première ligne est associée à c, la deuxième à c.
...ce qui donne

HH ab
HH 00 01 11 10
c H
H
0 0 2 6 4
1 1 3 7 5

E XEMPLE 10.25. Cas de quatre variables :

80
8 / 92
 H
HH ab
00 01 11 10
cd HHH
00 0 4 12 8
01 1 5 13 9
11 3 7 15 11
10 2 6 14 10

Dans un tel diagramme, chaque case représente un minterme. Les autres monômes regroupent un
nombre de cases qui est une puissance de 2, selon le nombre de variables présentes.

Exercice 10.26. Faire un diagramme à cinq variables.

Réponse :

H
HH abc
000 001 011 010 110 111 101 100
de HH H
00 0 4 12 8 24 28 20 16
01 1 5 13 9 25 29 21 17
11 3 7 15 11 27 31 23 19
10 2 6 14 10 26 30 22 18

C’est-à-dire :
– les quatre premières colonnes correspondent à a, les quatre dernières à a,
– les deux premières, et les deux dernières colonnes correspondent à b, les quatre centrales à b,
– les colonnes 1, 4, 5 et 8 à c, les autres à c,
– les deux premières lignes à d, les deux dernières à d,
– enfin, la première et la dernière ligne sont associées à e, les deux centrales à e.
Les diagrammes peuvent être utilisés en réunion, en intersection ou en complémentation.
Ils permettent :
– d’obtenir la FCD d’une fonction booléenne plus aisément que par le calcul algébrique (utilisé pour
découvrir la forme en question),
– une première approche du problème de la simplification des fonctions booléennes (dans des cas
simples et pour un petit nombre de variables)...
Utilisation des diagrammes de Karnaugh pour représenter les fonctions booléennes...
En réunion. Soit par exemple f (a, b, c) = a + bc. Son diagramme est :
HH ab
HH 00 01 11 10
c H
H
0 0 2 6 4
1 1 3 7 5

On lit aisément la FCD de f sur le diagramme : f (a, b, c) = m1 + m4 + m5 + m6 + m7 .

En intersection. Soit f (a, b, c) = (a + b)(a + c).
On peint en rouge les cases correspondant à a + b, et on note en italique les nombres correspondant
àa+c:

81
9 / 92
 H
HH ab
c HH 00 01 11 10
H
0 0 2 6 4
1 1 3 7 5

La représentation de f est contenue dans les cases rouges possédant les nombres en italique.
Comme (a + b)(a + c) = a + bc, on retrouve la même FCD.
En complémentation. Soit f (a, b, c) = a + bc, de diagramme :
HH ab
HH 00 01 11 10
c H
H
0 0 2 6 4
1 1 3 7 5

Alors la négation de a + bc est dans les cases pas rouge : la FCD de f est m0 + m2 + m3 .

Exercice 10.27 (Fonctions booléennes). Donner la forme canonique disjonctive de la fonction booléeene
dont l’expression est

f (a, b, c, d, e) = a · [b · e · (c + d) + b · (c · d · e + c · d · e)].

Exercice 10.28. Pour chacune des expressions suivantes...

E1 = xyz + xyz + xyz + xyz

E2 = xyz + xyz + xyz + xyz
E3 = xyz + xyz + xyz + xyz + xyz

donner la forme minimale en exploitant les diagrammes de Karnaugh

Exercice 10.29 (Application de la méthode de Karnaugh). Trouver une forme minimale de E = xy +

xyz + xyz + xyzt.

Exercice 10.30 (Composition de la méthode de Karnaugh). On considère deux fonctions booléennes

u et v des quatres variables a, b, c, d définies par u = (a + d)(b + c) et v = (a + c)(b + d).
1. Dessiner les diagrammes de Karnaugh de u et de v.
2. En déduire le diagramme de Karnaugh de w = uv + uv.
3. Donner une forme minimale pour w

Exercice 10.31 (BTS-2009). La société K-Gaz décide de recruter en interne des collaborateurs pour sa
filiale en Extrême-Orient. Pour chaque employé, on définit les variables booléennes suivantes :
– a = 1 s’il a plus de cinq ans d’ancienneté dans l’entreprise ;
– b = 1 s’il possède un B.T.S. informatique de gestion (BTS-IG) ;
– c = 1 s’il parle couramment l’anglais.
La direction des ressources humaines décide que pourront postuler les employés :
– qui satisfont aux trois conditions,
– ou qui ont moins de 5 ans d’ancienneté mais qui maîtrisent l’anglais,
– ou qui ne maîtrisent pas l’anglais mais qui possèdent un BTS-IG.
1. Écrire une expression booléenne E traduisant les critères de la direction.
2. Représenter l’expression E par un tableau de Karnaugh.
3. À l’aide du tableau de Karnaugh, donner une expression simplifiée de E.

82
10 / 92
 4. Retrouver ce résultat par le calcul.
5. En déduire une version simplifiée des critères de la direction.

Exercice 10.32 (BTS-2002). On considère l’expression E = a.c + b.c + a.b + a.b.c dépendant des
variables booléennes a, b et c :
1. Simplifier l’expression E à l’aide de la lecture d’un tableau de Karnaugh (ou d’une table de
vérité).
2. Dans un organisme qui aide des personnes au chômage à trouver un emploi, on considère pour
ces personnes, trois variables booléennes définies ainsi :
– a = 1 si la personne est âgée de 45 ans ou plus (sinon a = 0) ;
– b = 1 si la personne est au chômage depuis un an ou plus (sinon b = 0) ;
– c = 1 si la personne a déjà suivi une formation l’année précédente (sinonc = 0).
Une formation qualifiante sera mise en place pour les personnes vérifiant au moins un des critères
suivants :
– avoir 45 ans ou plus et être au chômage depuis moins de un an ;
– avoir moins de 45 ans et ne pas avoir suivi de formation l’année précé- dente ;
– être au chômage depuis un an ou plus et ne pas avoir suivi de formation l’année précédente ;
– avoir moins de 45 ans, être au chômage depuis moins de un an et avoir suivi une formation
l’année précédente.
Les personnes qui ne répondent à aucun de ces quatre critères, pourront par- ticiper à un stage
d’insertion en entreprise.
(a) Écrire l’expression booléenne F en fonction des variables a, b et c qui traduit le fait que la
personne pourra suivre cette formation qualifiante.
(b) En déduire une caractérisation simple des personnes qui participeront à un stage d’insertion
en entreprise.

V Résolution d’équations booléennes

Soit une équation booléenne de la forme la plus générale :

f (x1 , x2 , . . . , xn ) = g(x1 , x2 , . . . , xn )

1. Puisque A = B ⇐⇒ A ⊕ B = 0, on se ramène immédiatement à une équation du type :

F (x1 , x2 , . . . , xn ) = 0

2. On met F sous la forme :

F (x1 , x2 , . . . , xn ) = x1 · r + x1 · s = 0

Cette dernière équation est équivalente, en algèbre de Boole, aux deux équations

(1) x1 · r = 0


(2) x1 · s = 0

3. Une équation du type de (2) se résout par introduction d’une variable auxiliaire y1 . En effet,

x1 · s = 0 ⇐⇒ ∃y1 ∈ E, x1 = y1 · s

.
4. Dans ces conditions, x1 = y1 + s, valeur que l’on porte dans (1), pour obtenir l’équation y1 · r +
r · s = 0, qui est elle-même équivalente aux deux équations

83
11 / 92
 (3) y1 · r = 0

.
(4) r·s=0
En utilisant la variable auxiliaire z1 , (3) se résout comme (2) par :

∃z1 ∈ E, y1 = z1 + r

5. Finalement, l’équation proposée est équivalente aux équations :

– (5) x1 = (z1 + r) · s ;(qui donne les valeurs de x1 )
– (4) r · s = 0 (qui ne comporte plus que n-1 variables).
On recommence donc les mêmes opérations pour x2 dans (4), et ainsi de suite.

Exercice 10.33. Résoudre l’équation : x + y = x + z.

Exercice 10.34. Résoudre l’équation : x · y + x · z = 0

x+y =x+z

Exercice 10.35. Résoudre le système d’équations :
x·y =x·z

Exercice 10.36 (Fonctions booléennes universelles). On considère une fonction booléenne de deux vari-
ables, mise sous forme canonique disjonctive : f (x, y) = α · x · y + β · x · y + γ · x · y + δ · x · y, où
(α , β , γ , δ) ∈ {0, 1}4
– Montrer que cette fonction n’est susceptible d’exprimer la négation que si α = 1 et δ = 0.
– Dans ce cas, montrer qu’il n’y a que deux couples de valeurs possibles pour β et γ, si l’on veut
que f puisse aussi exprimer la somme x + y et le produit x · y.

La simplification des fonctions booléennes doit être laissée aux méthodes algébriques dans les cas
plus complexes, de manière à pouvoir affirmer avoir trouvé une forme minimale, et éventuellement
toutes, si nécessaire. Diverses méthodes visent cet objectif. Nous n’en exposerons ici qu’une seule, la
méthode de Quine-Mac Cluskey, dite aussi méthode des consensus.

VI Méthode des consensus

La méthode des consensus est une méthode algébrique permettant :
– d’être certain d’obtenir la forme minimale,
– de les obtenir toutes.
Commençons par introduire la notion de consensus...

D ÉFINITION 10.9. Lorsque, dans une somme booléenne, deux monômes admettent dans leur expression
une et une seule variable qui se présente sous son aspect affirmé dans l’un et sous son aspect nié dans
l’autre, on dit que ces deux monômes présentent un consensus (ou sont en consensus).
Le consensus de ces deux monômes est alors le produit de toutes les autres variables. ♦

E XEMPLE 10.37. Les monômes a · b · d · e et a · c · d · f présentent un consensus, car le premier contient

a et le second a. Le consensus de ces deux termes est b · c · d · e · f .

E XEMPLE 10.38. abc et bcd présentent un consensus (acd), quand abc et bcd d’une part, et abc et bcd
d’autre part, n’en présentent pas.

Exercice 10.39. Trouvez tous les consensus de

f (a, b, c, d) = abc + acd + abcd + acd + bcd

84
12 / 92
 P ROPRIÉTÉ 10.10 (R ÉSULTAT FONDAMENTAL ) : Rajouter, à une somme booléenne, le consensus
de deux termes de la somme (qui en présentent un) ne modifie pas sa valeur.

P REUVE En effet, le consensus de a · m et de a · m′ est m · m′ , et on peut constater que a · m + a ·

m′ + m · m′ = a · m + a · m′ + (a + a) · m · m′ = a · m + a · m′ + a · m · m′ + a · m · m′ = a · m + a · m′ .

Venons-en à la méthode proprement dite (qui permettra, on le rappelle, de trouver toutes les formes
les plus simplifiées d’une expression booléenne donnée). Elle se déroule en trois étapes...

Étape préliminaire. Développer l’expression pour la mettre sous la forme d’une somme de monômes,
et en suppprimer les multiples (toute autre tentative de simplification est inutile).

Obtention d’une forme stable par consensus. Répéter les deux phases suivantes, jusqu’à ce que
l’expression obtenue soit stable, ne change plus :
1. rajouter tous les consensus des termes qui en présentent un,
2. supprimer les multiples nouvellement introduits.

R EMARQUE 10.8. L’introduction des consensus fait parfois apparaître des multiples. La suppression de
ces derniers fait parfois apparaître de nouvelles possibilités de consensus...

D ÉFINITION 10.10 (E XPRESSION STABLE , MONÔMES PRINCIPAUX ). L’expression obtenue est dite sta-
ble du point de vue des consensus ; elle est unique. Ses termes s’appellent les monômes principaux. ♦

Exercice 10.40. Trouvez la forme stable par consensus de

f (a, b, c, d) = abc + acd + abcd + acd + bcd

La somme des monômes principaux d’une expression booléenne est généralement plus longue que
l’expression de départ. Parfois, elle peut s’avérer plus courte, mais même dans ce cas, rien ne prouve
qu’il n’existe pas une expression encore plus courte. C’est pourquoi, dans tous les cas, une nouvelle
étape est nécessaire.

E XEMPLE 10.41. Dans a + a · b, les deux termes présentent un consensus, qui est b, et on a alors
a + a · b = a + a · b + b = a + b (comme on le sait, c’est la règle n◦3). Ici, il y a simplification.
Mais dans a · b + a · c, les deux termes présentent un consensus, qui est b · c. On a alors a · b + a · c =
a · b + a · c + b · c. Ici, il apparaît un terme de plus.

Choix d’un nombre minimal de monômes principaux. C’est la dernière étape de la méthode des
consensus, qui fait intervenir la FCD.
Les formes minimales de l’expression algébrique de départ sont des sommes des monômes prin-
cipaux ci-dessus. Pour savoir quels monômes principaux garder, et quels monômes principaux sup-
primer, on calcule la FCD de l’expression de départ. Les mintermes de cette FCD sont des multiples
des monomes principaux. Les monômes principaux retenus dans les formes minimales sont tels qu’ils
possèdent tous les mintermes de la FCD parmi leurs multiples.
Pour bien comprendre cette dernière étape, i.e. cette sélection des monômes principaux réellement
utiles, on donne plusieurs exemples complets...

85
13 / 92
E XEMPLE 10.42. Appliquons la méthode des consensus à

f (a, b, c) = (a + b)(a + b + c)

1. On développe : f (a, b, c) = ab + ac + ab + bc.

2. Obtention d’une forme stable par consensus.
– ab, ac : pas de consensus,
– ac, ab : consensus bc,
– ab, ab : pas de consensus,
– ac, bc : pas de consensus,
– ab, bc : consensus ac,
– ab, bc : pas de consensus,
D’où f (a, b, c) = ab + ac + ab + bc + ac + bc.
Par idempotence : f (a, b, c) = ab + ac + ab + bc.
Rajouter des consensus ne change alors rien : c’est notre forme stable.
Soient p1 , p2 , p3 , p4 les quatre monômes principaux.
3. Le diagramme de Karnaugh de l’expression de départ est :
H
HH ab
H 00 01 11 10
c H
H
0 0 2 6 4
1 1 3 7 5

D’où la FCD de l’expression de départ : m2 + m3 + m4 + m5 + m7 .

4. Choix d’un nombre minimal de monomes principaux :
hhhh
h hhh mintermes
hhhh 2 3 4 5 7
monomes principaux hhhh
h
1 X X
2 X X
3 X X
4 X X
↑ ↑ ↑ ↑ ↑
p3 p3 p1 p1 p2
p4 p2 p4

Tout minterme de la FCD doit être pris au moins une fois. Donc :
– pour avoir m2 , pas le choix : il faut prendre p3 . Mais, comme on a pris p3 , on a récupéré m3 .
– pour avoir m4 , il faut prendre p1 . Avec cela, on récolte m5 .
– enfin, pour avoir m7 , on a le choix entre p2 et p4 .
Il y a donc deux formes minimales :
– p 1 , p2 , p3 ,
– p 1 , p3 , p4 .

E XEMPLE 10.43. Appliquons la méthode des consensus à

S =a·b+a·c

La somme des monômes principaux de S est a · b + a · c + b · c.

Posons :

86
14 / 92
 – P1 = a · b,
– P2 = a · c
– P3 = b · c.
La FCD de S est m1 + m3 + m6 + m7 .
– m1 est contenu dans P2 . Le choix de P2 est donc obligatoire, ce que l’on exprime par l’équation
booléenne p2 = 1.
– m3 est contenu dans P2 et P3 . On a donc le choix entre ces deux monômes, ce que l’on exprime
par l’équation booléenne p2 +p3 = 1 (évidemment, le choix précédent rend cette condition inutile,
mais on expose ici la méthode).
– m6 est contenu dans P1 , soit p1 = 1.
– m7 est contenu dans P1 et P3 , soit p1 + p3 = 1.
Il faut donc développer le produit p2 (p2 + p3 )p1 (p1 + p3 ) = p1 p2 qui prouve que la forme minimale
(unique, dans cet exemple) de la fonction donnée est obtenue avec la somme de P1 et de P2 ; il s’agit,
bien entendu, de a · b + a · c.

E XEMPLE 10.44. Appliquons la méthode des consensus à

S =a·c+a·b·d+a·b·c+a·b·c+b·c·d+a·b·c

1. Suppression des multiples : a · c absorbe a · b · c

Il reste :
a·c+a·b·d+a·b·c+a·b·c+b·c·d
2. Premiers consensus :
a·c+a·b·d+a·b·c+a·b·c+b·c·d+b·c·d+a·b+b·c+a·b·d+b·c·d+a·c·d+a·c·d+a·c·d+a·b·d
3. Suppression des multiples :
a · b absorbe a · b · c
b · c absorbe a · b · c
Il reste :
a·c+a·b·d+b·c·d+b·c·d+a·b+b·c+a·b·d+b·c·d+a·c·d+a·c·d+a·c·d+a·b·d
4. Nouveaux consensus (on n’a fait figurer qu’une seule fois chacun d’entre eux) :
a·c+a·b·d+b·c·d+b·c·d+a·b+b·c+a·b·d+b·c·d+a·c·d+a·c·d+a·c·d+
a·b·d+a·b·d+c·d+a·d+b·c·d+b·d+a·b·c+b·d+b·c·d+a·b·c+a·b·c+c·d
5. Suppression des multiples :
a · b absorbe a · b · d et a · b · c, b · c absorbe b · c · d et a · b · c, c · d absorbe b · c · d et a · c · d
a · d absorbe a · b · d et a · c · d, b · d absorbe a · b · d et b · c · d, b · d absorbe b · c · d et a · b · d
c · d absorbe a · c · d et b · c · d
Il reste : a · c + a · b + b · c + c · d + a · d + b · d + a · b · c + b · d + c · d
6. Nouveaux consensus (on n’a fait figurer qu’une seule fois chacun d’entre eux) :
a·c+a·b+b·c+c·d+a·d+b·d+a·b·c+b·d+c·d+b·c+a·b·d+b·c·d+a·c·d
7. Suppression des multiples :
b · d absorbe a · b · d, c · d absorbe a · c · d et b · c · d, b · c absorbe a · b · c
Il reste : a · c + a · b + b · c + c · d + a · d + b · d + b · d + c · d + b · c
8. Un dernier tour de consensus montre que cette expression est stable par consensus.
A l’aide d’un diagramme de Karnaugh, on détermine les mintermes contenus dans chacun des
monômes principaux.
On en déduit la FCD, et, dans le tableau qui suit, on fait apparaître les monômes principaux et les
mintermes qu’ils contiennent :

87
15 / 92
```
` ``minterme
``` m0 m1 m2 m4 m5 m6 m7 m8 m9 m10 m13 m14 m15
monome `
P1 = a · c ⋄ ⋄ ⋄ ⋄
P2 = a · b ⋄ ⋄ ⋄ ⋄

P3 = b · c ⋄ ⋄ ⋄ ⋄
P4 = c · d ⋄ ⋄ ⋄ ⋄

P5 = a · d ⋄ ⋄ ⋄ ⋄
P6 = b · d ⋄ ⋄ ⋄ ⋄

P7 = b · d ⋄ ⋄ ⋄ ⋄

P8 = c · d ⋄ ⋄ ⋄ ⋄
P9 = b · c ⋄ ⋄ ⋄ ⋄
La première colonne, par exemple, s’interprète comme suit : dans toute forme (réduite ou non) pré-
tendant représenter l’expression donnée au départ, il est nécessaire qu’un monôme au moins contienne
le minterme m0 , puisque ce dernier figure dans la FCD.
Cette condition peut être réalisée en choisissant le monôme principal P1 , ou P3 , ou P5 , ou P7 . Elle
peut être exprimée par l’équation booléenne p1 + p3 + p5 + p7 = 1, etc.
On obtient l’équation booléenne :
(p1 + p3 + p5 + p7 )(p1 + p3 + p4 )(p5 + p7 + p8 )(p1 + p2 + p5 )(p1 + p2 + p4 + p6 )(p2 + p5 + p8 +
p9 )(p2 + p6 + p9 )(p3 + p7 )(p3 + p4 )(p7 + p8 )(p4 + p6 )(p8 + p9 )(p6 + p9 ) = 1
On supprime évidemment les conditions qui sont automatiquement réalisées lorsque d’autres le sont
(si p3 + p7 vaut 1, alors p1 + p3 + p5 + p7 aussi), il reste
(p1 + p2 + p5 )(p3 + p7 )(p3 + p4 )(p7 + p8 )(p4 + p6 )(p8 + p9 )(p6 + p9 ) = 1
On développe le produit, mais pas le premier facteur, car il est le seul à contenir les monômes prin-
cipaux p1 , p2 et p5 , donc on sait déjà qu’il faudra en prendre un (et un seul, pour une forme minimale...)
des trois.
On obtient
(p1 + p2 + p5 )(p3 + p4 p7 )(p8 + p7 p9 )(p6 + p4 p9 ) = (p1 + p2 + p5 )(p3 p8 p3 p7 p9 + p4 p7 p8 + p4 p7 p9 )(p6 +
p4 p9 ) = (p1 + p2 + p5 )(p3 p6 p8 + p3 p4 p8 p9 + p3 p6 p7 p9 + p3 p4 p7 p9 + p4 p6 p7 p8 + p4 p7 p8 p9 + p4 p6 p7 p9 +
p4 p7 p9 ) = (p1 + p2 + p5 )(p3 p6 p8 + p3 p4 p8 p9 + p3 p6 p7 p9 + p4 p6 p7 p8 + p4 p7 p9 ) = 1
On constate qu’il est possible de réaliser la condition de la seconde parenthèse en ne choisissant que
3 monômes principaux : P3 , P6 et P8 , ou encore P4 , P7 et P9 (les autres choix possibles en nécessitent
4).
En plus, il faut choisir l’un des trois de la première parenthèse, comme on l’a dit plus haut.
On obtient donc 6 formes minimales :

a·c
 
  
 

 b·c+b·d+c·d   ou

 


ou + a·b
c·d+b·d+b·c ou 
  
 

 

a·d
 

Exercice 10.45. On considère f (a, b, c, d) = abc + acd + abcd + acd + bcd

– Trouvez sa FCD.
– En déduire ses formes minimales.
Exercice 10.46. Utiliser la méthode des consensus pour obtenir toutes les formes minimales des fonc-
tions booléennes suivantes :
1. Celles des précédents exemples et exercices.
2. d · e + a · c + b · c + a · b + a · d · e + a · d · e
Fin du Chapitre

88
16 / 92
Chapitre 1

Calcul propositionnel

1.1 Introduction
Les formules (ou phrases, ou énoncés) du calcul propositionnel sont de deux types : ou bien
une formule est une proposition atomique, ou bien elle est compose à partir d’autres formules
à l’aide des connecteurs logiques ∧, ¬, ∨, ⇒ (et, non, ou, implique, que l’on appelle connecteurs
propositionnels).
Considérons, par exemple, l’énoncé arithmétique « 2+2 = 4 ou 3+3 = 5 ». Cet énoncé peut se
considérer comme construit des propositions atomiques « 2+2 = 4 » et « 3+3 = 5 », via le connecteur
propositionnel ou. Une analyse similaire peut se faire pour les énoncés du langage naturel. On
considère l’énoncé « s’il pleut, alors le soleil se cache », que l’on reconnaîtra être équivalent à « il
pleut implique que le soleil se cache », comme obtenu des deux propositions atomiques « il pleut »
et « le soleil se cache » via le connecteur propositionnel implique.
Une proposition atomique est un énoncé simple, ne pouvant prendre que les valeurs "vrai" ou
"faux ", et ce de façon non ambiguë ; elle donne donc une information sur un état de chose. De
plus une proposition atomique est indécomposable : « le ciel est bleu et l’herbe est verte » n’est
pas une proposition atomique mais la composition de deux propositions atomiques. Dans l’analyse
du langage naturel, on ne peut pas considérer comme des propositions : les souhaits, les phrases
impératives ou les interrogations.
Nous avons déjà vu des exemples de formules composées. Considérons maintenant l’énoncé
« s’il neige, alors le soleil se cache et il fait froid ». C’est une formule composée, via le connecteur
implique, depuis la formule atomique « il neige » et la formule composée « le soleil se cache et il fait
froid ». On peut donc composer des formules à partir d’autres formules composées. La valeur de
vérité d’une formule composée se calcule comme une fonction des formules dont elle est composée.
Le calcul des propositions est la première étape dans la définition de la logique et du rai-
sonnement. Il définit les règles de déduction qui relient les phrases entre elles, sans en examiner
le contenu ; il est ainsi une première étape dans la construction du calcul des prédicats, qui lui
s’intéresse au contenu des propositions.
Nous partirons donc en général de faits : "p est vrai, q est faux" et essaierons de déterminer si
une affirmation particulière est vraie.

1.2 Syntaxe du calcul propositionnel : les formules

Le langage du calcul propositionnel est formé de :
— symboles propositionnels Prop = {p1 , p2 , . . .} ;
— connecteurs logiques {¬, ∧, ∨, ⇒} ;
— symboles auxiliaires : parenthèses et espace.

Remarque 1.1. Dans la littérature logique on utilise plusieurs synonymes pour symbole proposi-
tionnel ; ainsi variable propositionnelle, proposition atomique, formule atomique, ou encore atome
sont tous des synonymes de symbole propositionnel.

17 / 92
6 Chapitre 1. Calcul propositionnel

Définition 1.2. L’ensemble Fcp des formules du calcul propositionnel est le plus petit
ensemble tel que :
— tout symbole propositionnel est une formule ;
— si ϕ est une formule alors ¬ϕ est une formule ;
— si ϕ, ψ sont des formules alors ϕ ∨ ψ, ϕ ∧ ψ et ϕ ⇒ ψ sont des formules.

Les symboles auxiliaires ne sont utilisés que pour lever les ambiguïtés possibles : par exemple,
la formule p ∨ q ∧ r est ambiguë, car elle peut se lire de deux façons différentes, ((p ∨ q) ∧ r) ou
bien (p ∨ (q ∧ r)).

Exemple 1.3. p, p ⇒ (q ∨ r) et p ∨ q sont des formules propositionnelles ; ¬(∨q) et f (x) ⇒ g(x)

n’en sont pas.

A cause de la structure inductive de la définition, une formule peut-être vue comme un arbre
dont les feuilles sont étiquetées par des symboles propositionnels et les noeuds par des connecteurs.
Par exemple, la formule p ⇒ (¬q ∧ r) correspond à l’arbre représenté Figure 1.2.

p ∧

¬ r

Figure 1.1 – Représentation arborescente de la formule p ⇒ (¬q ∧ r)

Notation 1.4. On utilise souvent en plus le connecteur binaire ⇔ comme abréviation : ϕ ⇔ ψ

est l’abréviation de (ϕ ⇒ ψ)∧(ψ ⇒ ϕ). De la même façon, on ajoute le symbole ⊥ qui correspond
à Faux et le symbole > qui correspond à Vrai. Ces deux symboles sont aussi des abréviations, ils
ne sont pas indispensables au langage. (Par exemple ⊥ peut être utilisé à la place de p ∧ ¬p et >
à la place de p ∨ ¬p.)
Définition 1.5 (Sous-formule). L’ensemble SF (ϕ) des sous-formules d’une formule ϕ est défini
par induction de la façon suivante.
— SF (p) = {p} ;
— SF (¬ϕ) = {¬ϕ} ∪ SF (ϕ) ;
— SF (ϕ ◦ ψ) = {ϕ ◦ ψ} ∪ SF (ϕ) ∪ SF (ψ) (oú ◦ désigne un des symboles ∧, ∨, ⇒).
Par exemple, SF (p ⇒ (¬q ∧r)) = {p, q, r, ¬q, ¬q ∧r, p ⇒ (¬q ∧r)}. Quand on voit une formule
comme un arbre, une sous-formule est simplement un sous-arbre (voir Figure 1.2).
Définition 1.6 (Sous-formule stricte). ψ est une sous-formule stricte de ϕ si ψ est une sous-
formule de ϕ qui n’est pas ϕ.

1.3 Sémantique du calcul propositionnel

Il faut maintenant un moyen de déterminer si une formule est vraie ou fausse. La première
étape est de donner une valeur de vérité aux propositions atomiques. L’évaluation d’une formule,

18 / 92
1.3 Sémantique du calcul propositionnel 7

p ∧

¬ r

Figure 1.2 – Représentation arborescente des sous-formules de p ⇒ (¬q ∧ r)

dépend donc des valeurs choisies pour les symboles propositionnels. Ces valeurs sont données par
une valuation.

Définition 1.7 (Valuation). Une valuation est une application de Prop dans {0, 1}. La valeur
0 désigne le "faux" et la valeur 1 désigne le "vrai".
Une valuation sera souvent donnée sous forme d’un tableau. Par exemple, si Prop = {p, q}
p q
alors la valuation v : p 7→ 1, q 7→ 0 s’écrit plus simplement v :
1 0
Une fois la valuation v choisie, la valeur de la formule se détermine de façon naturelle, par
extension de la valuation v aux formules de la façon suivante :
Définition 1.8 (Valeur d’une formule).
— v(¬ϕ) = 1 ssi v(ϕ) = 0 ;
— v(ϕ ∨ ψ) = 1 ssi v(ϕ) = 1 ou v(ψ) = 1 ;
— v(ϕ ∧ ψ) = 1 ssi v(ϕ) = 1 et v(ψ) = 1 ;
— v(ϕ ⇒ ψ) = 0 ssi v(ϕ) = 1 et v(ψ) = 0.
La définition précédente peut apparaître trompeuse car circulaire : afin d’expliquer la logique,
nous somme en train de l’utiliser (ssi, ou, et . . . ). Ceci peut être contournée en utilisant la
définition (équivalente à la Définition 1.8) suivante.

Définition 1.9 (Valeur d’une formule (bis)).

— v(¬ϕ) = 1 − v(ϕ) ;
— v(ϕ ∨ ψ) = max(v(ϕ), v(ψ)) ;
— v(ϕ ∧ ψ) = min(v(ϕ), v(ψ)) ;
— v(ϕ ⇒ ψ) = v(¬ϕ ∨ ψ).

Cette dernière définition est purement combinatoire car elle repose sur la structure de l’ensemble
ordonné fini { 0 < 1 } ; nous supposons en fait que cette structure est évidente et claire par elle-
même et qu’il n’y a pas besoin de la justifier plus.

Exercice 1.10. Proposez un algorithme qui, étant donné une formule ϕ du calcul propositionnel
et une valuation v, calcule v(ϕ). Quel type de structure de données utiliser pour coder les formules ?
Quel type de structure de données utiliser pour coder les valuations ?

Notez que la définition 1.9 correspond aux tables de vérité des connecteurs logiques (dont vous

19 / 92
8 Chapitre 1. Calcul propositionnel

avez sûrement entendu parler) :

p q p∧q p q p∨q p q p⇒q

p : ¬p 0 0 0 0 0 0 0 0 1
0 1 0 1 0 0 1 1 0 1 1
1 0 1 0 0 1 0 1 1 0 0
1 1 1 1 1 1 1 1 1

Remarque 1.11 (Langage naturel et langage formel). Remarquez la définition particulière de

l’implication : on l’entend en général comme un "si ..., alors ...", on voit ici que l’énoncé "si 1+1=1,
alors la capitale de la France est Marseille" est vrai, puisque toute phrase ϕ ⇒ ψ est vraie dès
lors que ϕ est évaluée à faux. Ceci est peu naturel, car dans le langage courant, on ne s’intéresse à
la vérité d’un tel énoncé que lorsque la condition est vraie : "s’il fait beau je vais à la pêche" n’a
d’intérêt pratique que s’il fait beau. . . Attribuer la valeur vrai dans le cas ou la prémisse est fausse
correspond a peu près à l’usage du si .. alors dans la phrase suivante : "Si Pierre obtient sa Licence,
alors je suis Einstein" : c’est à dire que partant d’une hypothèse fausse, alors je peux démontrer
des choses fausses (ou vraies). Par contre, il n’est pas possible de démontrer quelque chose de faux
partant d’une hypothèse vraie.
D’autres exemples où il est difficile de coder le langage naturel via le langage formel :
— comment coderiez vous, en langage formel, l’énoncé français « Soit il est froid, soit il est
chaud » ?
— et comment coderiez vous l’énoncé anglais « Either I cannot understand French, or my
professor doesn’t know how to speak it » ?

Terminons en mentionnant de la valeur de l’abréviation ⇔ : v(ϕ ⇔ ψ) = 1 ssi v(ϕ) = v(ψ).

Ce qui correspond à la table de vérité suivante :

p q p⇔q
0 0 1
0 1 0
1 0 0
1 1 1

Exercice 1.12. Définissons l’ensemble Prop(ϕ) des variables propositionnelles contenues dans
ϕ ∈ Fcp par l’induction suivante :

Prop(p) = { p } ,
Prop(¬ϕ) = Prop(ϕ) ,
Prop(ϕ ◦ ψ) = Prop(ϕ) ∪ Prop(ψ) , ◦ ∈ { ∧, ∨, ⇒ } .

Montrez que :
— Prop(ϕ) = Prop ∩ SF (ϕ), pour tout ϕ ∈ Fcp ;
— si v(p) = v 0 (p) pour tout p ∈ Prop(ϕ), alors v(ϕ) = v 0 (ϕ).

Cet exercice montre que pour présenter les modèles d’une formule ϕ, on peut se restreindre aux
valuations v : Prop(ϕ) → {0, 1}.

1.3.1 Modèles d’une formule

Définition 1.13. L’ensemble des valuations d’un ensemble de variables propositionnelles Prop
est noté Val(Prop) (ou juste Val lorsqu’il n’y a pas d’ambiguité sur Prop). Val(Prop) est donc
l’ensemble des fonctions de Prop dans {0, 1}.

Par exemple, si Prop = {p, q, r}, alors Val est représenté par la Table 1.1, dans laquelle chaque
ligne est une valuation de Prop :

20 / 92
1.3 Sémantique du calcul propositionnel 9

p q r
0 0 0
0 0 1
0 1 0
0 1 1
1 0 0
1 0 1
1 1 0
1 1 1

Table 1.1 – Val pour Prop = {p, q, r}

Définition 1.14 (Modèle d’une formule). Un modèle de ϕ est une valuation v telle que v(ϕ) = 1.
On note mod(ϕ) l’ensemble des modèles de ϕ.

Exemple 1.15. Si Prop = {p, q, r} et ϕ = (p ∨ q) ∧ (p ∨ ¬r) alors l’ensemble des modèles de ϕ est

p q r
0 1 0
1 0 0
mod(ϕ) =
1 0 1
1 1 0
1 1 1

Définition 1.16 (Satisfaisabilité). Une formule ϕ est satisfaisable (ou consistante, ou encore
cohérente) si elle admet un modèle (i.e., s’il existe une valuation v telle que v(ϕ) = 1, i.e. si
mod(ϕ) 6= ∅).

Définition 1.17 (Insatisfaisabilité). Une formule ϕ est insatisfaisable (ou inconsistante, ou

incohérente) si elle n’admet aucun modèle (i.e., si pour toute valuation v, v(ϕ) = 0, i.e., si
mod(ϕ) = ∅)

Définition 1.18 (Tautologie). Une formule ϕ est une tautologie (ou valide) si v(ϕ) = 1 pour
toute valuation v (i.e., si mod(ϕ) = Val). On note |= ϕ pour dire que ϕ est une tautologie.

Un exemple de tautologie est ϕ ∨ ¬ϕ, c’est à dire le tiers exclus.

Exercice 1.19. Montrez que les formules suivantes sont des tautologies :

p ⇒ p, p ⇒ (q ⇒ p) , (p ⇒ (q ⇒ r)) ⇒ ((p ⇒ q) ⇒ (p ⇒ r)) , ((p ⇒ q) ⇒ p) ⇒ p .

Définition 1.20 (Equivalence). On dit que ϕ est équivalente à ψ si les deux formules ont les
mêmes modèles (i.e. si mod(ϕ) = mod(ψ)). On note alors ϕ ≡ ψ.

Exemple 1.21. Les opérateurs ∧, ∨ sont associatifs-commutatifs. Deux formules identiques à

associativité-commutativité près sont équivalentes. Remplacer une sous-formule ψ d’une formule
ϕ par une formule équivalente ψ 0 donne une formule notée ϕ[ψ ← ψ 0 ]. Cette substitution préserve
les modèles, i.e., mod(ϕ) = mod(ϕ[ψ ← ψ 0 ]).

Exercice 1.22. Prouvez les équivalences suivantes :

21 / 92
10 Chapitre 1. Calcul propositionnel

ϕ∨⊥≡ϕ ϕ∧⊥≡⊥ (ϕ ∧ ψ) ∧ θ ≡ ϕ ∧ (ψ ∧ θ)
ϕ∨>≡> ϕ∧>≡ϕ (ϕ ∧ ψ) ∨ θ ≡ (ϕ ∨ θ) ∧ (ψ ∨ θ)
ϕ∨ψ ≡ψ∨ϕ ϕ∧ψ ≡ψ∧ϕ (ϕ ∨ ψ) ∧ θ ≡ (ϕ ∧ θ) ∨ (ψ ∧ θ)
ϕ∨ϕ≡ϕ ¬(ϕ ∨ ψ) ≡ (¬ϕ) ∧ (¬ψ) (ϕ ∨ ψ) ∨ θ ≡ ϕ ∨ (ψ ∨ θ)
¬¬ϕ ≡ ϕ ϕ∧ϕ≡ϕ ¬(ϕ ∧ ψ) ≡ (¬ϕ) ∨ (¬ψ) .

La proposition suivante explicite les liens forts existants entre logique et algèbre ensembliste.
En fait, par la sémantique, nous sommes en train d’étudier et comprendre la logique par cette
algèbre (dont nous supposons disposer d’une compréhension intuitive et exacte).

Proposition 1.23. Soient ϕ et ψ deux formules, on a :

1. mod(¬ϕ) = Val − mod(ϕ) ;
2. mod(ϕ ∨ ψ) = mod(ϕ) ∪ mod(ψ) ;
3. mod(ϕ ∧ ψ) = mod(ϕ) ∩ mod(ψ) ;
4. |= ϕ ⇒ ψ ssi mod(ϕ) ⊆ mod(ψ).

Démonstration. 1. pour toute valuation v ∈ Val,

v ∈ mod(¬ϕ) ssi v(¬ϕ) = 1 par la définition de modèle

ssi v(ϕ) = 0 par la Définition 1.8
ssi v ∈
/ mod(ϕ) encore, par la définition de modèle
ssi v ∈ Val − mod(ϕ)

2. pour toute valuation v ∈ Val,

v ∈ mod(ϕ ∨ ψ) ssi v(ϕ ∨ ψ) = 1

ssi v(ϕ) = 1 ou v(ψ) = 1
ssi v ∈ mod(ϕ) ou v ∈ mod(ψ)
ssi v ∈ mod(ϕ) ∪ mod(ψ)

3. pour toute valuation v ∈ Val,

v ∈ mod(ϕ ∧ ψ) ssi v(ϕ ∧ ψ) = 1

ssi v(ϕ) = 1 et v(ψ) = 1
ssi v ∈ mod(ϕ) et v ∈ mod(ψ)
ssi v ∈ mod(ϕ) ∩ mod(ψ)

4.

|= ϕ ⇒ ψ ssi pour toute valuation v ∈ Val, v(ϕ ⇒ ψ) = 1

ssi pour toute valuation v ∈ Val, v(¬ϕ ∨ ψ) = 1
ssi pour toute valuation v ∈ Val, v(ϕ) = 0 ou v(ψ) = 1
ssi pour toute valuation v ∈ Val, v(ϕ) ≤ v(ψ)
ssi pour toute valuation v ∈ Val, si v(ϕ) = 1 alors v(ψ) = 1
ssi mod(ϕ) ⊆ mod(ψ)

Définition 1.24 (Conséquence logique). Une formule ϕ est conséquence logique d’une formule

22 / 92
1.3 Sémantique du calcul propositionnel 11

ψ si tout modèle de ψ est un modèle de ϕ (c’est-à-dire, si mod(ψ) ⊆ mod(ϕ)). On note alors ψ |= ϕ.

Remarque 1.25. Attention à la confusion dans les notations !
— ψ |= ϕ où ψ est une formule : ϕ est conséquence logique de ψ ;
— |= ϕ (rien à gauche du symbole |=) : ϕ est une tautologie ;
— v |= ϕ où v est une valuation, i.e., l’assignation d’une valeur aux propositions atomiques de
la formule ; c’est un raccourcis assez fréquent dans la littérature (noté quelques-fois aussi
v ϕ, exactement pour ne pas utiliser |=) pour v(ϕ) = 1. Dans ces notes, nous essayerons
d’éviter cette notation, si possible.
Attention : la notation ψ |= ϕ signifie que ϕ est conséquence logique de ψ (donc mod(ψ) ⊆
mod(ψ)) et non pas que ψ est conséquence logique de ϕ, ce que serait plutôt mod(ϕ) ⊆ mod(ψ).

Proposition 1.26. Soient ϕ et ψ deux formules propositionnelles.

1. ϕ |= ψ si et seulement si |= ϕ ⇒ ψ.
2. ϕ ≡ ψ si et seulement si |= ϕ ⇔ ψ.

Démonstration.
1. Conséquence directe du point 4 de la Proposition 1.23
2.

ϕ ≡ ψ ssi mod(ϕ) = mod(ψ)

ssi mod(ϕ) ⊆ mod(ψ) et mod(ψ) ⊆ mod(ϕ)
ssi |= ϕ ⇒ ψ et |= ψ ⇒ ϕ
ssi |= ϕ ⇒ ψ ∧ ψ ⇒ ϕ .

23 / 92
12 Chapitre 1. Calcul propositionnel

1.3.2 La conséquence logique (d’un ensemble de formules)

Les formules propositionnelles peuvent être vues comme des contraintes sur les propositions
atomiques. Par exemple, p ∧ q contraint p et q à être vraies, où p ⇒ q contraint q à être vraie toute
fois que p est vraie. Il est donc très courant de considérer des ensembles de formules proposition-
nelles pour modéliser des problèmes de satisfaction de contraintes. Une valuation satisfaisant toute
formule de l’ensemble pourra donc se considérer comme une solution du problème.
On étend les définitions vues précédemment aux ensembles de formules.

Définition 1.27 (Modèle). Un modèle d’un ensemble de formules Γ est une valuation v telle
que v(ϕ) = 1 pour tout ϕ ∈ Γ. On note mod(Γ) l’ensemble des modèles de Γ.
Cet ensemble de modèles est donc l’ensemble des valuations qui respectent toutes les
contraintes de Γ.
Définition 1.28 (Satisfaisabilité/Consistance, Insatisfaisabilité/Contradiction). Un ensemble de
formules Γ est
— satisfaisable (ou consistant, ou cohérent) s’il admet au moins un modèle (i.e., si
mod(Γ) 6= ∅) ;
— insatisfaisable (ou contradictoire, ou inconsistant, ou encore incohérent) s’il n’ad-
met aucun modèle (i.e., si mod(Γ) = ∅), on note alors Γ |=⊥.

Un ensemble Γ contradictoire ne peut être satisfait : par exemple l’ensemble Γ = {p, ¬p} est
insatisfaisable.
Définition 1.29 (Conséquence logique). Une formule ϕ est conséquence logique de Γ si et
seulement si toute valuation qui donne 1 à toutes les formules de Γ donne 1 à ϕ (i.e., si
mod(Γ) ⊆ mod(ϕ)), on note alors Γ |= ϕ. On note cons(Γ) l’ensemble des conséquences logiques
de Γ.

Remarque 1.30. Attention aux deux notations :

— ψ |= ϕ où ψ est une formule ;
— Γ |= ϕ où Γ est un ensemble de formule.
Par ailleurs, remarquez que ϕ |= ψ si, et seulement si, { ϕ } |= ψ ; les deux notations sont donc
cohérentes entre elles.

Voici des relations élémentaires entre les relations que nous venons de présenter.

Proposition 1.31. Γ |= ϕ ssi Γ ∪ {¬ϕ} est contradictoire.

Démonstration. On peut calculer comme suit :

Γ |= ϕ ssi pour toute valuation v,

— soit v est un modèle de Γ et v(ϕ) = 1
— soit v n’est pas un modèle de Γ
ssi pour toute valuation v,
— soit v est un modèle de Γ et v(¬ϕ) = 0
— soit v n’est pas un modèle de Γ
ssi pour toute valuation v,
v n’est pas un modèle de Γ ∪ {¬ϕ}
ssi Γ ∪ {¬ϕ} est contradictoire.

Proposition 1.32. Pour tous ensembles de formules Σ, Γ,

mod(Σ ∪ Γ) = mod(Σ) ∩ mod(Γ).

En particulier, si Σ ⊆ Γ alors mod(Γ) ⊆ mod(Σ).

Cette proposition se comprend bien si on voit un ensemble de formules comme un ensemble

24 / 92
1.3 Sémantique du calcul propositionnel 13

de contraintes sur les variables propositionnelles. Plus on ajoute de contraintes, et moins il reste
de possibilités pour résoudre ces contraintes.
Démonstration de la Proposition 1.32. Pour toute valuation v :

v ∈ mod(Σ ∪ Γ) ssi pour tout ϕ ∈ Σ ∪ Γ, v(ϕ) = 1

ssi pour tout ϕ ∈ Σ, v(ϕ) = 1 et pour tout ψ ∈ Γ, v(ψ) = 1
ssi v ∈ mod(Σ) et v ∈ mod(Γ)
ssi v ∈ mod(Σ) ∩ mod(Γ).

La preuve de la Proposition suivante est laissée en exercice.

Proposition 1.33. Si Γ0 ⊆ Γ et Γ0 |= ϕ, alors Γ |= ϕ.
Proposition 1.34. Soit Γ = { ϕ1 , . . . , ϕn } un ensemble fini de formules. Nous avons alors

mod(Γ) = mod(ϕ1 ∧ . . . ∧ ϕn ) ,

de façon que {ϕ1 , . . . ϕn } |= ψ ssi ϕ1 ∧ . . . ∧ ϕn |= ψ, ssi (ϕ1 ∧ . . . ∧ ϕn ) ⇒ ψ est une tautologie.

Cette proposition exprime le fait qu’un ensemble fini de formules propositionnelles peut
toujours être vu comme une seule formule formée de la conjonction des formules de l’ensemble. Une
formule étant un objet fini, ce résultat ne peut pas se généraliser (au moins, de façon immédiate)
au cas des ensembles de formules de taille infinie. Dans le cas où Γ est infini, il faudra utiliser le
théorème de compacité (Théorème 1.40) qui permet de ramener les problèmes de satisfaisabilité
et de contradiction d’un ensemble de taille quelconque à celle d’ensemble finis.
Démonstration. Remarquons que

mod({ ϕ1 , . . . , ϕn }) = mod({ ϕ1 } ∪ . . . ∪ { ϕn })
= mod({ ϕ1 }) ∩ . . . ∩ mod({ ϕn }) (par la Proposition 1.32)
= mod(ϕ1 ) ∩ . . . ∩ mod(ϕn ) (par la Remarque 1.30)
= mod(ϕ1 ∧ . . . ∧ ϕn ) . (par la Propositon 1.23)

Donc, on a que mod({ ϕ1 , . . . , ϕn }) ⊆ mod(ψ) si et seulement si mod(ϕ1 ∧ . . . ∧ ϕn ) ⊆ mod(ψ) et,

par la Proposition 1.23, la dernière relation est vraie ssi (ϕ1 ∧. . .∧ϕn ) ⇒ ψ est une tautologie.
Proposition 1.35. Γ |= ϕ si, et seulement si, mod(Γ) = mod(Γ ∪ {ϕ}).
La proposition peut se comprendre comme suit. Une conséquence logique ϕ d’un ensemble Γ
est une nouvelle contrainte déduite directement de Γ. Puisqu’elle découle de Γ, elle ne peut pas
apporter des “vraies” contraintes supplémentaires que celles apportées par Γ. Cela signifie que les
modèles de Γ et ceux de Γ ∪ {ϕ} sont exactement les mêmes.
Démonstration de la Proposition 1.35. La proposition découle du fait que mod(Γ ∪ {ϕ}) =
mod(Γ) ∩ mod({ϕ}), et que la relation mod(Γ) ⊆ mod(ϕ) est équivalente à mod(Γ) ∩ mod({ϕ}) =
mod(Γ).

Exemple 1.36. L’ensemble Γ = {(p ⇒ s) ∨ q, ¬q} possède comme conséquence logique p ⇒ s.

Bien entendu, les modèles de Γ sont exactement les modèles de Γ ∪ {p ⇒ s}.
La Proposition 1.35 implique également une méthode de simplification d’un ensemble de for-
mules : si Γ contient une formule ϕ conséquence logique de Γ − {ϕ}, alors ϕ peut être retirée de
l’ensemble de contraintes Γ sans en modifier la sémantique, mod(Γ) = mod(Γ − {ϕ}). L’exemple
suivant éclaircit cette méthode.
Exemple 1.37. Avec cet exemple, nous allons tirer avantage des propositions et remarques pré-
cédentes pour résoudre un ensemble de contraintes ayant une certaine complexité.
On dispose de 4 variables propositionnelles, p, q, r, s, qui obéissent aux contraintes suivantes :

25 / 92
14 Chapitre 1. Calcul propositionnel

ϕ1 : q ∧ ¬r
ϕ2 : p ⇒ (r ∨ s)
ϕ3 : ¬r ∧ (q ∨ p)

Soit Γ1 = {ϕ1 , ϕ2 , ϕ3 }, cet ensemble forme l’ensemble des contraintes sur les valeurs que les
variables propositionnelles peuvent prendre.
On se pose les questions suivantes :
1. Peut-on simplifier l’ensemble Γ1 de façon à ne pas changer l’ensemble de ses modèles, et donc
de ses conséquences ?
(a) On remarque que la contrainte ϕ3 est une conséquence logique de la contrainte ϕ1 .
En effet, pour toute valuation v,
— v satisfait ϕ1 ssi v(r) = 0 et v(q) = 1,
— v satisfait ϕ3 ssi v(r) = 0 et (v(p) = 1 ou v(q) = 1).
D’où, mod(ϕ1 ) ⊆ mod(ϕ3 ).
(b) Soit Γ2 = {ϕ1 , ϕ2 }, on a mod(Γ2 ) = mod(Γ1 ). En effet, par définition,

mod(Γ1 ) = mod(ϕ1 ) ∩ mod(ϕ2 ) ∩ mod(ϕ3 ) = mod(ϕ1 ) ∩ mod(ϕ2 ) = mod(Γ2 ) .

Donc les conséquences de Γ1 et Γ2 sont les mêmes et on peut alors simplifier Γ1 par Γ2 .
2. Quel est l’ensemble des modèles de Γ2 ?

Modèles de ϕ1 : Modèles de ϕ2 :
p q r s p q r s
0 1 0 0 0 0 0 0
0 1 0 1 0 0 0 1
1 1 0 0 0 0 1 0
1 1 0 1 0 0 1 1
0 1 0 0
0 1 0 1
0 1 1 0
0 1 1 1
1 0 0 1
1 0 1 0
1 0 1 1
1 1 0 1
1 1 1 0
1 1 1 1

L’ensemble M des modèles de Γ2 est l’intersections des modèles de ϕ1 et ϕ2 :

p q r s
0 1 0 1
0 1 0 1
1 1 0 1
(Évidemment, nous aurions pu éviter de calculer tous le modèles de ϕ2 ! ! !)
3. Γ2 est-il consistant ? contradictoire ?
Γ2 admet un modèle, il est donc consistant et non contradictoire.
4. Quelles conséquences logiques pouvons nous tirer de l’ensemble Γ2 ?
Les conséquences logiques de Γ2 sont toutes les formules dont l’ensemble des modèles contient
M . On a donc entre autres :
¬r, q, q ∧ ¬r ∈ cons(Γ)
5. Ajoutons maintenant une nouvelle contrainte : Γ3 = {¬q∧¬s}∪Γ2 . On a mod(Γ3 ) = mod(Γ2 )∩
mod(¬q ∧ ¬s) = ∅. Donc mod(Γ3 ) = ∅ et Γ3 est contradictoire.

26 / 92
1.3 Sémantique du calcul propositionnel 15

[Link] Compacité
Le théorème de compacité sert à caractériser la conséquence logique dans les cas où l’ensemble
des formules est infini en ne considérant que des sous-ensembles finis. Par ailleurs, ce théorème
jouera un rôle cruciale plus tard, dans le cadre de la preuve de complètude pour la calcul de la
résolution (Théorème 2.93).

Le théorème de compacité. Pour commencer, nous avons besoin du lemme suivant, appelé
Lemme de König.
Lemme 1.38 (König). Tout arbre infini à branchement fini possède une branche infinie.
Démonstration. Supposons que T , qui est à branchement fini, soit infini. On définit une branche
infinie e0 , e1 , . . . , en , . . . dans T par induction sur les entiers. La propriété suivante :

P (n) ::= le sous-arbre issu de en est infini

sera vraie de tout entier n ≥ 0.

(Base de l’induction). Pour n = 0, on choisit e0 = r (la racine de l’arbre) qui par hypothèse
est la racine d’un arbre infini.
(Étape inductive). On suppose avoir construit e0 , . . . , en et que P (n) est vraie, c’est-à-dire que
le sous arbre issu de en est infini. Considérons les successeurs immédiats de en , appelons-les
en1 , . . . , enk ; si tous étaient racines de sous-arbres finis, de cardinalité p1 , . . . , pk , alors il en
serait de même de en (le sous-arbre issu de en aurait alors cardinalité 1 + p1 + ... + pk ),
contradiction. Donc l’un d’entre eux est racine d’un sous-arbre infinis, ce noeud étant le en+1
cherché.
Nous aurons besoin du Lemme dans la forme suivante :
Lemme 1.39. Tout arbre a branchement fini et dont toutes les branches sont finies, est fini.

Théorème 1.40 (Compacité). Un ensemble de formules propositionnelles Γ est satisfaisable ssi

tout sous-ensemble fini de Γ est satisfaisable.

Par contraposée, le Théorème de compacité peut s’énoncer de la façon suivante :

Théorème 1.41 (Compacité). Un ensemble de formules propositionnelles Γ est contradictoire
si, et seulement si, il existe un sous-ensemble fini de Γ contradictoire.

Remarquons que l’implication « si un sous-ensemble fini de Γ est contradictoire, alors Γ est

contradictoire » est trivialement vraie. Nous nous limiterons à prouver l’implication inverse.
Démonstration (du Théorème 1.41). On fait la preuve dans le cas où Prop = {p0 , p1 , p2 , . . . , pn , . . .}
est un ensemble dénombrable.
Nous avons besoin d’une construction importante appelée « arbre sémantique » ou « arbre de
Herbrand ». L’arbre sémantique associé est un arbre binaire infini dont toutes les arêtes à gauches
sont étiquetées par 0 (le « faux ») et celles à droites sont étiquetées par 1 (le « vrai »). Chaque
niveau de l’arbre est associé à un symbole propositionnel. La racine (le niveau 0) est associé à p0 :
chaque fois que l’on descend d’un noeud de niveau i, ceci revient à poser pi faux si l’on descend à
gauche, et pi vrai si l’on descend à droite. Remarquons que :
1. chaque chemin infini π partant de la racine correspond à une valuation vπ de l’ensemble des
propositions ;
2. chaque noeud e à profondeur n correspond à une valuation ve des variables {p0 , . . . pn−1 }.
Nous appelons un noeud e de l’arbre noeud d’échec (par rapport à Γ) s’il existe une formule ϕe ∈ Γ
telle que Prop(ϕe ) ⊆ { p0 , . . . pn−1 } et ve (ϕe ) = 0, où n est la profondeur du noeud e.

On suppose que Γ est inconsistante et on montre qu’il existe un sous-ensemble Γ0 ⊆ Γ fini et

inconsistant.

27 / 92
16 Chapitre 1. Calcul propositionnel

p0
0 1

p1
0 1 0 1

p0 ⇒ p1 p2

Figure 1.3 – Début de l’arbre sémantique avec le noeud d’échec 10 étiqueté

On commence par remarquer que chaque branche contient un noeud d’échec. En effet, si une
branche n’en contient pas, elle définit un modèle de Γ, ce qui est contradictoire à l’hypothèse.
On peut donc faire la construction suivante : prenons le premier noeud d’échec de chaque
branche et étiquetons ce noeud par une formule de Γ fausse sur ce noeud, puis coupons l’arbre
au niveau du noeud d’échec. (Plus formellement : si π est une branche de l’arbre sémantique,
dénotons par e(π) le premier noeud d’échec sur cette branche, et choisissons ϕe(π) ∈ Γ tel que
ve(π) (ϕe(π) ) = 0 ; ensuite, coupons l’arbre de façon que les noeuds e(π) deviennent des feuilles de
l’arbre.)
L’arbre obtenu en tronquant ainsi toutes les branches est un arbre à branchement fini, ses
branches sont finies, et donc il est fini par le Lemme de König. Le sous-ensemble Γ0 = { ϕe(π) |
π une branche de l’arbre sémantique } des formules de Γ étiquetant les feuilles de l’arbre est donc
fini. Or toutes les feuilles de l’arbre sont des noeuds d’échec et donc chacune des valuations rend
fausse au moins une des formules de Γ0 . (Si v ∈ Val, alors v = vπ pour une branche π de l’arbre, et
donc v(ϕe(π) ) = vπ (ϕe(π) ) = ve(π) (ϕe(π) ) = 0.) L’ensemble Γ0 ⊆ Γ est donc fini et inconsistant.
Exemple 1.42. Supposons que Γ soit de la forme { p0 ∧ ¬p1 , p0 ⇒ p1 , . . . }. Alors le noeud e = 10
de l’arbre sémantique est un noeud d’échec par rapport à cet ensemble Γ, car p0 ⇒ p1 ∈ Γ and
ve (p0 ⇒ p1 ) = 0. (Le debut de) l’arbre sémantique, avec le noeud 10 étiqueté par la formule
témoignant son échec, est représenté en Figure 1.3.
Remarque 1.43. On peut donner une preuve plus simple du théorème de compacité en utilisant
les propriétés des systèmes de preuves. Nous la donnerons par la suite, lorsque nous aurons les
outils nécessaires.
Corollaire du théorème de compacité :

Corollaire 1.44. Une formule ϕ est conséquence d’un ensemble de formules Γ si et seulement
s’il existe un sous-ensemble fini Γf ini de Γ tel que Γf ini |= ϕ.

Démonstration.

Γ |= ϕ ssi Γ ∪ {¬ϕ} est contradictoire par la Proposition 1.31

ssi il existe Γf ⊆ Γ ∪ {¬ϕ} fini et contradictoire par le Théorème de compacité
ssi il existe Γf ⊆ Γ fini tel que Γf ∪ {¬ϕ} est contradictoire
ssi il existe un sous-ensemble fini Γf ⊆ Γ tel que Γf |= ϕ .

1.3.3 Décidabilité du calcul propositionnel

Une logique est décidable s’il existe un algorithme (calcul réalisable sur un ordinateur qui
termine toujours pour toute donnée) qui permet de savoir pour chaque formule si elle est une
tautologie (i.e. si |= ϕ) ou pas.

Théorème 1.45. Le calcul propositionnel est décidable.

Démonstration. Méthode des tables de vérité : calculer la table de vérité prenant en argument

28 / 92
1.3 Sémantique du calcul propositionnel 17

les symboles propositionnels de ϕ et calculer pour chaque valuation possible la valeur de ϕ.

Coût : O(2n ) avec n le cardinal de Prop(ϕ) (nombre de symboles propositionnels dans ϕ).

Nous verrons par la suite qu’il y a de meilleurs algorithmes, mais qu’il ont tous un coût ex-
ponentiel. La plupart de ces algorithmes débutent par une première phase de normalisation de la
formule, c’est à dire qu’on modifie la syntaxe de la formule de manière à la mettre sous une forme
normalisée, tout en conservant la sémantique de la formule, c’est-à-dire l’ensemble de ses modèles.

29 / 92
18 Chapitre 1. Calcul propositionnel

1.4 Equivalence entre formules

Il est courant de souhaiter modifier une formule, de façon à rendre son expression plus simple,
ou plus facile à manipuler, et ceci en gardant bien sûr la sémantique de la formule, c’est-à-dire,
sans modifier l’ensemble de ses modèles.

1.4.1 La substitution
La substitution d’une formule ψ par une formule ψ 0 dans une troisième formule ϕ (notée ϕ[ψ←ψ0 ] )
consiste à remplacer chaque occurrence de ψ dans ϕ par ψ 0 .
Prenons par exemple les formules ϕ = (¬p ∨ q) ∧ (¬p ∨ ¬r), ψ = ¬p et ψ 0 = q ⇒ p, alors

ϕ[ψ←ψ0 ] = ((q ⇒ p) ∨ q) ∧ ((q ⇒ p) ∨ ¬r).

Plus formellement, la substitution est définie de la façon suivante :

Définition 1.46 (Substitution). Soient ϕ, ψ, et ψ 0 trois formules du calcul propositionnel,

— si ψ n’est pas une sous-formule de ϕ, alors ϕ[ψ←ψ0 ] = ϕ
— sinon si ϕ = ψ alors ϕ[ψ←ψ0 ] = ψ 0
— sinon
— si ϕ = ¬ϕ0 alors ϕ[ψ←ψ0 ] = ¬(ϕ0[ψ←ψ0 ] )
— si ϕ = ϕ1 ◦ ϕ2 (où ◦ est un connecteurs ∧, ∨, ⇒) alors ϕ[ψ←ψ0 ] = ϕ1 [ψ←ψ0 ] ◦ ϕ2 [ψ←ψ0 ] .
Proposition 1.47. Soient ϕ, ψ, et ψ 0 trois formules du calcul propositionnel, si ψ ≡ ψ 0 alors
ϕ ≡ ϕ[ψ←ψ0 ] .
Démonstration. Voir TD 3.

Attention, dans le cas général, la substitution ne conserve pas la sémantique de la formule. Par
exemple, p et q ∧ ¬q ne sont pas équivalentes ; ainsi, les formules p et p[p ← q ∧ ¬q] ne sont pas
équivalentes.

1.4.2 Equivalences classiques

Nous avons vu que remplacer une sous-formule ψ d’une formule ϕ par une formule équivalente
ψ 0 donne une formule notée ϕ[ψ ← ψ 0 ] équivalente à ϕ. C’est-à-dire que cette substitution préserve
les modèles, i.e., mod(ϕ) = mod(ϕ[ψ ← ψ 0 ]).
Voici quelques règles d’équivalences courantes, qui permettent de telles substitutions.

ϕ∧ψ ≡ψ∧ϕ ϕ∨ψ ≡ψ∨ϕ (Commutativité)

ϕ ∧ (ψ1 ∧ ψ2 ) ≡ (ϕ ∧ ψ1 ) ∧ ψ2 ϕ ∨ (ψ1 ∨ ψ2 ) ≡ (ϕ ∨ ψ1 ) ∨ ψ2 (Associativité)
>∧ϕ≡ϕ∧>≡ϕ ⊥ ∨ϕ ≡ ϕ∨ ⊥≡ ϕ (Élements neutres)
ϕ∧ϕ≡ϕ ϕ∨ϕ≡ϕ (Idempotence)
ϕ ∧ (ϕ ∨ ψ) ≡ ϕ ϕ ∨ (ϕ ∧ ψ) ≡ ϕ (Absorption)
ϕ∧ ⊥ ≡⊥ ∧ϕ ≡⊥ ϕ∨>≡>∨ϕ≡> (Elément absorbant)
ϕ ∧ (ψ1 ∨ ψ2 ) ≡ (ϕ ∧ ψ1 ) ∨ (ϕ ∧ ψ2 ) ϕ ∨ (ψ1 ∧ ψ2 ) ≡ (ϕ ∨ ψ1 ) ∧ (ϕ ∨ ψ2 )
(Distributivité)
ϕ ∧ ¬ϕ ≡ ¬ϕ ∧ ϕ ≡⊥ ϕ ∨ ¬ϕ ≡ ¬ϕ ∨ ϕ ≡ > (Complément)
¬¬ϕ ≡ ϕ (Involution)
¬(ϕ ∧ ψ) ≡ ¬ϕ ∨ ¬ψ ¬(ϕ ∨ ψ) ≡ ¬ϕ ∧ ¬ψ (Lois de De Morgan)
ϕ ⇒ ψ ≡ ¬ϕ ∨ ψ ≡ ¬(ϕ ∧ ¬ψ) (Implication matérielle)
ϕ ⇒ ψ ≡ ¬ψ ⇒ ¬ϕ (Contraposition)
ϕ1 ⇒ (ϕ2 ⇒ ϕ3 ) ≡ (ϕ1 ∧ ϕ2 ) ⇒ ϕ3 (Curryfication)

30 / 92
1.4 Equivalence entre formules 19

Nous observons ici que la formule suivante :

[(ϕ1 ⇒ ϕ2 )∧(ϕ2 ⇒ ϕ3 )] ⇒ [ϕ1 ⇒ ϕ3 ] (Transitivité)

est une tautologie, et que ϕ ≡ > si et seulement si ϕ est une tautologie.

Observez que, dans les exemples d’équivalences ci-dessus, si ϕ ≡ ψ et ϕ, ψ sont des formules
sans implication, alors on a aussi l’équivalence ϕ0 ≡ ψ 0 où ϕ0 et ψ 0 sont les formules obtenues de
ϕ et ψ en échangeant la conjonction avec la disjonction et vice-versa (donc, en échangeant aussi le
vrai par le faux). C’est un principe tout à fait général que l’on peut énoncer ici :
Proposition 1.48 (Principle de dualité). Si ϕ ≡ ψ où ϕ et ψ sont des formules sans implication,
alors ϕ0 ≡ ψ 0 où ϕ0 et ψ 0 sont les formules obtenues de ϕ et ψ en échangeant la conjonction avec
la disjonction et vice-versa.
Exemple 1.49. Nous pouvons argumenter que ϕ ∧ (ψ ∨ χ) ≡ ϕ ∧ (χ ∨ ψ) de façon précise de cette
façon :
ϕ ∧ (ψ ∨ χ) ≡ (ϕ ∧ p)[p ← ψ ∨ χ]
≡ (ϕ ∧ p)[p ← χ ∨ ψ] (par commutativité, et en utilisant la proposition 1.47)
≡ ϕ ∧ (χ ∨ ψ) .

1.4.3 Formes normales

La mise sous forme normale transforme une formule en une formule équivalente (que l’on dit
« normalisée ») plus adaptée au traitement algorithmique.

Notations. Remarquons que, à cause des lois d’associativité et commutativité, toutes les formules
possibles construites à partir des formules ϕ1 , . . . , ϕn via l’application du connecteur logique ∧, sont
équivalentes. Par exemple
((ϕ1 ∧ ϕ2 ) ∧ ϕ3 ) ∧ ϕ4 , ϕ1 ∧ ((ϕ2 ∧ ϕ3 ) ∧ ϕ4 ) , ϕ1 ∧ (ϕ2 ∧ (ϕ3 ∧ ϕ4 )) , (ϕ2 ∧ ϕ4 ) ∧ (ϕ3 ∧ ϕ1 ) ,
sont des formules équivalentes. On peut faire la remarque analogue pour le connecteur logique ∨.
Ainsi, si ϕ1 , . . . , ϕn sont des formules, nous pouvons utiliser les notations :
n
^ n
_
ϕi = ϕ1 ∧ . . . ∧ ϕn et ϕi = ϕ1 ∨ . . . ∨ ϕn
i=1 i=1

pour dénoter un parenthésage arbitraire de ϕ1 ∧ . . . ∧ ϕn (resp. ϕ1 ∨ . . . ∨ ϕn ). Les choix de l’ordre

et du parenthésage ne sont donc pas significatifs, au moins du point de vue sémantique.
Nous pouvons même étendre ces considérations plus loin : si ψ possède plus que deux occurrences
dans la liste ϕ1 , . . . , ϕn , nous pouvons effacer les doublons de cette liste pour obtenir des formules
équivalentes. Par exemple, les formules
ϕ1 ∧ ϕ2 ∧ ϕ1 ∧ ϕ3 , ϕ1 ∧ ϕ2 ∧ ϕ3 ,
sont équivalentes.
La conclusion de l’ensemble de ces remarques est la suivante : puisque ni l’ordre, ni le paren-
thésage, ni la multiplicité n’influent sur la sémantique de la formule, ce qui compte dans une telle
formule est sa structure d’ensemble.
Nous allons donc considérer des conjonctions et disjonctions de liste de formules (avec ou sans
répétitions) ; la longueur n de la liste pourra aussi prendre les valeurs 0 et 1, en posant :

0
^ 0
_
ϕi := > , ϕi := ⊥ , pour n = 0,
i=1 i=1
1
^ 1
_
ϕi := ϕ1 , ϕi := ϕ1 , pour n = 1.
i=1 i=1

31 / 92
20 Chapitre 1. Calcul propositionnel

Définition 1.50 (Littéral). Un littéral est une formule atomique ou la négation d’une for-
mule atomique. Autrement dit, c’est une formule ` de la forme p ou ¬p, où p est un symbole
propositionnel.
Wn
Définition 1.51 (Clause). Une clause disjonctive est une disjonction de littéraux : V i=1 `i où
n
les `i sont des littéraux. Une clause conjonctive est une conjonction de littéraux : i=1 `i où
les `i sont des littéraux.
Remarque 1.52. Comme d’usage, quand le mot « clause » est utilisé sans spécifications ulté-
rieures, l’adjectif « disjonctive » est sous-entendu. Ainsi, clause tout-court est synonyme de clause
disjonctive.

Définition 1.53 (Forme normale conjonctive). Une formule conjonctive (ou formule sous
forme normale Vm conjonctive (FNC), ou sous forme clausale) est une V conjonction
m W nj
de clauses
disjonctives : j=1 Cj où les Cj sont des clauses disjonctives, ou encore j=1 i=1 `ji où les `ji
sont des littéraux.

Exemple 1.54. La formule suivante est sous forme clausale :

(¬p ∨ q ∨ r) ∧ (¬q ∨ p) ∧ s

Définition 1.55 (Forme normale disjonctive). Une formule disjonctive (ou formule
Wm sous
forme normale disjonctive (FND)) est une disjonction de clauses conjonctives : j=1 Cj où
W m V nj j
les Cj sont des clauses, ou encore j=1 i=1 `i , où les `ji sont des littéraux.

Exemple 1.56. La formule suivante est sous forme normale disjonctive :

(¬p ∧ q ∧ r) ∨ (¬q ∧ p) ∨ s

La forme normale conjonctive est en général la plus adaptée lorsqu’on cherche un modèle
d’une formule car il faut chercher une valuation satisfaisant chacune des clauses de la formule
(le Lemme 1.57 ci-dessous précise ce point). Dans l’exemple 1.54, on voit que si v est un modèle,
alors forcément v(s) = 1 ; pour satisfaire la deuxième clause, il faut que v(p) = 1 ou v(q) = 0, mais
alors la seule façon de satisfaire la première clause est r = 1. Il y a donc deux modèles.
V
Lemme 1.57. Soit ϕ une formule en FNC : ϕ = i=1,...,n Ci où Ci sont des clauses. Pour tout
v ∈ Val, v ∈ mod(ϕ) ssi, pour tout i = 1, . . . , n, il existe un littéral l in Ci tel que v(l) = 1.

La preuve de ce lemme étant immédiate, elle est laissée au lecteur.

[Link] Mise sous forme clausale, en préservant l’équivalence

L’algorithme consiste en l’application des 3 étapes suivantes :

Etape 1 (élimination de l’implication). Appliquer, tant que possible, la substitution sui-
vante :

ϕ ⇒ ψ ← ¬ϕ ∨ ψ .

Etape 2 (pousser la négation vers les symboles propositionnels). Appliquer, tant que
possible, les substitutions suivantes (en remplaçant le membre gauche par le membre droit) :

¬¬ϕ ← ϕ , ¬(ϕ ∧ ψ) ← ¬ϕ ∨ ¬ψ , ¬(ϕ ∨ ψ) ← ¬ϕ ∧ ¬ψ .

32 / 92
1.4 Equivalence entre formules 21

Etape 3 (pousser la disjonction vers les littéraux). Appliquer, tant que possible, les sub-
stitutions suivantes (en remplaçant le membre gauche par le membre droit) :

ϕ ∨ (ψ1 ∧ ψ2 ) ← (ϕ ∨ ψ1 ) ∧ (ϕ ∨ ψ2 ) .

Exemple 1.58. Considérons ϕ = (¬(p ∧ (q ⇒ (r ∨ s)))) ∧ (p ∨ q).

— Etape 1 :
Remplacer q ⇒ (r ∨ s) par ¬q ∨ (r ∨ s) dans ϕ :
ϕ ≡ (¬(p ∧ (¬q ∨ (r ∨ s)))) ∧ (p ∨ q)
— Etape 2 :
ϕ ≡ (¬p ∨ ¬(¬q ∨ (r ∨ s))) ∧ (p ∨ q)
ϕ ≡ (¬p ∨ (¬¬q ∧ ¬(r ∨ s))) ∧ (p ∨ q)
ϕ ≡ (¬p ∨ (q ∧ ¬(r ∨ s))) ∧ (p ∨ q)
ϕ ≡ (¬p ∨ (q ∧ ¬r ∧ ¬s)) ∧ (p ∨ q)
— Etape 3 :
ϕ ≡ (¬p ∨ q) ∧ (¬p ∨ ¬r) ∧ (¬p ∨ ¬s) ∧ (p ∨ q)

Proposition 1.59. Le calcul précédent termine et donne une formule en forme clausale équiva-
lente à la formule initiale.
Remarque 1.60. Il n’y a pas unicité de la forme clausale.

[Link] Mise sous forme clausale, en préservant la satisfaisabilité

Considérons une formule ϕ du calcul propositionnel ayant ψ comme sous-formule : on peut
toujours considérer que ϕ de la forme ϕ0 [p ← ψ], pour un p choisi tel que p 6∈ Prop(ϕ).

Proposition 1.61. Soit ϕ, ψ ∈ Fcp and soit p 6∈ Prop(ψ) ; supposons que ϕ ne contient pas de
négations. On a alors

mod(ϕ[p ← ψ]) 6= ∅ ssi mod(ϕ ∧ (p ⇒ ψ)) 6= ∅ .

C’est-à-dire, les deux formules sont equisatisfaisables.

Démonstration. Soit v une valuation telle que v(ϕ[p ← ψ]) = 1, et v 0 la valuation satisfaisant,
v 0 (q) = v(p) pour tout q 6= p et v 0 (p) = v(ψ). On a alors v 0 (ϕ ∧ (p ⇒ ψ)) = 1. On a donc
mod(ϕ[p ← ψ]) 6= ∅ implique mod(ϕ ∧ (p ⇒ ψ)) 6= ∅ .

Nous montrons l’implication inverse par induction sur la structure de ϕ : on prouve que si v est
un modèle de ϕ ∧ (p ⇒ ψ) alors v est un modèle de ϕ[p ← ψ].
Avant de débuter l’induction, remarquons que si v(ϕ∧p ⇒ ψ) = 1, alors v(ϕ) = 1 et v(p) ≤ v(ψ).
Induction :
— cas de base :
— si ϕ = q où q 6= p est un symbole propositionnel, alors v(ϕ[p ← ψ]) = q = 1 ;
— si ϕ = p, alors v(p) = 1 (car v(ϕ) = 1) et donc v(ψ) = 1 (car par hypothèse v(p) ≤ v(ψ)).
On obtient donc v(ϕ[p ← ψ]) = v(ψ) = 1 ;
— pas d’induction : supposons que la propriété est vraie pour deux formules ϕ1 et ϕ2 .
— si ϕ = ϕ1 ∧ϕ2 , alors puisque v(ϕ) = 1, on a forcément v(ϕ1 ) = 1 et v(ϕ2 ) = 1. Puisqu’on a
également supposé que v(p) ≤ v(ψ), v(ϕ1 ∧p ⇒ ψ) = 1 et v(ϕ2 ∧p ⇒ ψ) = 1. Appliquons
l’hypothèse d’induction à ϕ1 et ϕ2 , nous obtenons v(ϕ1 [p ← ψ]) = 1 et v(ϕ2 [p ← ψ]) = 1.
En conclusion, v(ϕ[p ← ψ]) = min{v(ϕ1 [p ← ψ]), v(ϕ2 [p ← ψ])} = 1
— le cas ϕ = ϕ1 ∨ ϕ2 est similaire au précédent. Les cas ϕ = ¬ϕ1 et ϕ = ϕ1 ⇒ ϕ2
sont interdits par l’hypothèse que ϕ ne contient pas la négation (la négation apparait
implicitement dans l’implication).

33 / 92
22 Chapitre 1. Calcul propositionnel

Exercice 1.62. Montrez que l’hypothèse que la négation n’apparaît pas dans ϕ est nécessaire.

Exercice 1.63. Montrez que les deux formules ϕ[p ← ψ] et ϕ ∧ (p ⇒ ψ) ne sont pas équivalentes.

Exemple 1.64. Considerez la formule

n
_
pi,0 ∧ pi,1 . (1.1)
i=1

L’algorithme de mise en forme normale conjonctive construit la formule

^
p1,f (1) ∨ p2,f (2) ∨ . . . ∨ pn,f (n) .
f :[1,n]→{0,1}

Dans cet exemple le nombre de clauses produites a taille exponentielle par rapport au nombre de
clauses originaires.
La Proposition 1.61 montre que la formule (1.1) est equisatisfaisable avec la formule
n
^
(q1 ∨ . . . ∨ qn ) ∧ (¬qi ∨ pi,0 ) ∧ (¬qi ∨ pi,1 ) ,
i=1

une formule en FNC, avec un nombre de clauses de taille linéaire par rapport au nombre de clauses
originaires.
La Proposition 1.61 suggère donc une méthode de mise en forme clausale, préservant la satisfai-
sabilité, qui accélère le calcul de la forme clausale. La méthode s’applique si nous sommes intéressés
seulement à l’existence d’un modèle, et non pas à énumérer tous les modèles. Parmi les défauts
de la méthode, on peut noter que le fait introduire des nouveaux symboles propositionnels alourdi
évidemment les calculs de recherche d’un modèle.

1.5 Le problème SAT

1.5.1 Définition du problème

Définition 1.65 (Problème SAT). Le problème SAT est le problème de décision qui consiste à
déterminer si ϕ ∈ Fcp donnée en entrée admet, ou non, un modèle.

Le plus souvent, on suppose que la formule ϕ en entrée est en forme normale conjonctive.
La plupart des algorithmes de résolution de SAT ne se contentent pas de répondre par oui ou
par non, il peuvent fournir aussi un modèle, ou même l’ensemble des modèles.

Exemple 1.66. Donnée : Une formule booléenne mise sous forme FNC :

ϕ = (¬x1 ∨ x2 ∨ x3 ) ∧ (x1 ∨ x2 ) ∧ (¬x2 ∨ x3 ) ∧ (¬x3 ∨ ¬x1 ) .

Question : Est-ce que la formule ϕ admet au moins un modèle ?

Réponse : Pour cet exemple, la réponse est oui : la valuation v(x1 ) = 0, v(x2 ) = 1, v(x3 ) = 1
satisfait la formule ϕ, c’est-à-dire v ∈ mod(ϕ).

1.5.2 Un problème NP-complet

Théorème 1.67. Le problème SAT est décidable.

Démonstration. Algorithme : Etant donné une formule ϕ ayant n variables propositionnelles.

Calculer les 2n valuations possibles. Pour chacune d’entre-elles, calculer la valeur de vérité de ϕ.
Si au moins une est vraie, alors ϕ est satisfaisable.

34 / 92
1.5 Le problème SAT 23

Il existe des algorithmes plus performants, mais ces améliorations ne changent pas fondamen-
talement la difficulté du problème. On est devant la situation suivante. Étant donnée une formule
ϕ, on se demande si ϕ admet un modèle ou non, i.e., s’il existe des valeurs de vérité attribuables
aux variables propositionnelles qui satisferaient ϕ :
— une recherche exhaustive comme dans l’algorithme précédent peut demander jusqu’à 2n vé-
rifications si ϕ possède n variables propositionnelles. Cette démarche est dite déterministe,
mais son temps de calcul est exponentiel.
— d’un autre côté, si ϕ est satisfiable, il suffit d’une vérification à faire, à savoir tester précisé-
ment la configuration qui satisfait ϕ. Cette vérification demande un simple calcul booléen,
qui se fait en temps polynomial (essentiellement linéaire en fait). Le temps de calcul cesse
donc d’être exponentiel, à condition de savoir quelle configuration tester. Celle-ci pourrait
par exemple être donnée par un être omniscient auquel on ne ferait pas totalement confiance.
Une telle démarche est dite non déterministe.
La question de la satisfiabilité de ϕ, ainsi que tous les problèmes qui se résolvent suivant
la méthode que nous venons d’esquisser, sont dits NP (pour polynomial non déterministe). Par
exemple, tester si la formule ϕ est une tautologie équivaut, par des calculs très simples en temps
polynomial, à tester que sa négation n’est pas satisfaisable (par la Proposition 1.23).
Le problème SAT joue un rôle fondamental en théorie de la complexité, puisqu’on peut montrer
que la découverte d’un algorithme déterministe en temps polynomial pour ce problème permettrait
d’en déduire des algorithmes déterministes en temps polynomial pour tous les problèmes de type
NP (théorème de Cook). On dit que SAT (et donc également le problème de la non-démontrabilité
d’une proposition) est un problème NP-complet.

1.5.3 Modélisation - Réduction à SAT

Bien que le problème soit très difficile, nous verrons que nous disposons de logiciels très perfor-
mants permettant de résoudre le problème de satisfaction d’une formule. Il est donc important pour
tout informaticien de savoir profiter de ces outils. L’étape préalable est la suivante : étant donné
un problème qui peut-être apparemment complètement dissocié de la logique, réduire la résolution
de ce problème à la satisfaction d’une formule du calcul propositionnel. Il est bien sûr nécessaire
que la réduction elle-même soit réalisable en un temps raisonnable (en temps polynomial).

[Link] Comment modéliser

La plupart du temps, les problèmes sont énoncés en français (dans un fragment du français plus
ou moins ambigu). La première étape est d’identifier les propositions atomiques d’un énoncé,
il s’agit des plus petites briques de l’énoncé qui soient indécomposables et qui peuvent prendre la
valeur vraie ou faux.
Il faut ensuite construire une formule traduisant les énoncés à partir des propositions, en utili-
sant les connecteurs booléens. On utilise pour cela la table de correspondance suivante
et, mais ∧
ou ∨
ne pas, non ¬
il n’est pas vrai que ¬
si p alors q, p seulement si q p⇒q
p si et seulement si q p⇔q

Exemple 1.68 (suite).

Si et seulement si : Considérons l’énoncé

« J’irai à la plage si, et seulement si, il y a du soleil. »

et posons :
— plage : j’irai à la plage
— soleil : il y a du soleil

35 / 92
24 Chapitre 1. Calcul propositionnel

L’enoncé se traduit par plage ⇔ soleil . En effet, décomposons l’énoncé :

— « J’irai à la plage si il y a du soleil » se traduit par soleil ⇒ plage.
— « J’irai à la plage seulement si il y a du soleil » signifie que si je vais à la plage, alors il a
forcément du soleil et se traduit donc par plage ⇒ soleil .
On a donc soleil ⇒ plage ∧ plage ⇒ soleil , ce qui est équivalent à soleil ⇔ plage.

Implication versus équivalence Il est d’usage, lors de la définition de concepts mathématiques,

d’utiliser "si" à la place de "si et seulement si". Par exemple la définition du triangle équilatéral a
souvent la forme suivante :

« Un triangle est équilatéral s’il a trois coté égaux. »

Pourtant il faut entendre un "si et seulement si". Il s’agit d’une convention à laquelle vous devez
vous habituer.

Condition nécessaire et suffisante : Cette expression est une autre version du "si et seulement
si". Posons :
— note : avoir une bonne note
— travail : travailler
et considérons l’énoncé :

« Pour avoir une bonne note, il faut et il suffit de travailler »

ou de façon équivalente :

« Pour avoir une bonne note, il est nécessaire et suffisant de travailler »

Décomposons l’énoncé :
— P1 = « Pour avoir une bonne note il faut travailler » signifie qu’il faut nécessairement
travailler pour avoir une bonne note. On a donc la table suivante :
note travail P1
1 1 1
1 0 0
0 0 1
0 1 1
Donc P1 ≡ note ⇒ travail.
— P2 = « Pour avoir une bonne note, il suffit de travailler » signifie que si on travaille, on a
une bonne note :
note travail P1
1 1 1
1 0 1
0 0 1
0 1 0
Donc P2 ≡ travail ⇒ note.

[Link] Formalisation du problème du Sudoku pour la réduction à SAT

Soit ` un entier, et n`2 . Une grille de Sudoku de taille n × n, divisée en une grille ` × ` de façon
à former n blocs. Généralement, la grilles a les dimensions n = 9 et ` = 3. Au départ certaines
cases sont remplies par des nombres compris entre 1 et n, et d’autres sont vides. Le but du jeu est
de remplir les cases vides avec des nombres dans [1, n] en respectant les règles suivantes :
— On ne doit pas avoir deux nombres identiques sur une même ligne ;
— On ne doit pas avoir deux nombres identiques sur une même colonne ;
— Il ne doit pas y avoir deux nombres identiques dans l’un des blocs.

36 / 92
1.5 Le problème SAT 25

Pour être un Sudoku, la grille doit accepter une et une seule solution.

Formalisation. Pour représenter le problème sous forme de problème SAT, nous avons besoin
de beaucoup de variables propositionnelles. En effet il faut n3 variables Vxyz avec x, y, z ∈ [1, n].
La variable Vxyz sera vraie si et seulement si la case (x, y) contient la valeur z. Par exemple, si V135
est vraie, alors la case (1, 3) contient 5. Si on prend n = 4, il faudra 64 variables, pour n = 9 il en
faut 729. Voici la formulation des règles de remplissage d’un Sudoku.
« Chaque case contient un et un seul nombre » : pour tout i ∈ [1, n], pour tout j ∈ [1, n], il
existe k ∈ [1, n] tel que la case (i, j) contient k et pour tout k 0 6= k dans [1, k] : la case (i, j)
ne contient pas k 0 .
^ ^ _ ^
A= ( Vijk ∧ ¬Vi,j,k0 )
i∈[1,n] j∈[1,n] k∈[1,n] k0 ∈ [1, k]
k0 6= k

« On ne doit pas avoir deux nombres identiques sur une même colonne » : pour toute colonne
i ∈ [1, n], pour toute ligne j 6= j 0 dans [1, n], pour toute valeur k ∈ [1, n] : si la case (i, j)
contient k, alors la case (i, j 0 ) ne contient pas k.
^ ^ ^ ^
B= (Vi,j,k ⇒ ¬Vi,j 0 ,k )
i∈[1,n] j∈[1,n] j 0 ∈ [1, n] k∈[1,n]
j 0 6= j

« On ne doit pas avoir deux nombres identiques sur une même ligne » : pour toute ligne
j ∈ [1, n], pour toute colonne i 6= i0 dans [1, n], pour toute valeur k ∈ [1, n] : si la case (i, j)
contient k, alors la case (i0 , j) ne contient pas k.
^ ^ ^ ^
C= (Vi,j,k ⇒ ¬Vi0 ,j,k )
j∈[1,n] i∈[1,n] i0 ∈ [1, n] k∈[1,n]
i0 6= i

« On ne doit pas y avoir deux nombres identiques dans le même bloc » : pour tous x, x0 ∈ [1, `],
^ ^ ^ ^
D= (Vi,j,k ⇒ ¬Vi0 ,j 0 ,k )
x,y∈[0,`−1] i, i0 ∈ [1 + `x, ` + `x] j, j 0 ∈ [1 + `y, ` + `y] k∈[1,n]
i 6= i0 j 6= j 0

Pour assurer qu’une grille donnée est un Sudoku, il faut indiquer les chiffres déjà inscrits et
vérifier qu’il y a une et une seule solution au problème. Par exemple, pour la grille donnée en
exemple, on crée la formule :
E = V1,9,5 ∧ V2,9,3 ∧ V5,9,7 ∧ . . .
On cherche alors les modèles de la formule A ∧ B ∧ C ∧ D ∧ E. Si il n’y a qu’un seul modèle, alors
la grille est un Sudoku dont la solution est donnée par ce modèle.

37 / 92
26 Chapitre 1. Calcul propositionnel

1.5.4 Algorithmes de résolution de SAT

De nombreux algorithmes ont été proposés pour résoudre SAT, nous en présentons quelques-
uns, en nous focalisant sur le cas où la formule dont il faut décider la satisfaisabilité est déjà en
forme normale conjonctive.
Nous allons donc présenter ici quelques calculs sur les formules en FNC qui nous utiliserons
dans le cadres de ces algorithmes qui suivent.
Remarque 1.69. Nous pouvons identifier une formule en forme normale conjonctive ϕ avec l’en-
semble Cϕ des ses clauses, car évidemment nous avons mod(ϕ) = mod(Cϕ ) (voir la Proposition 1.34).
Par exemple, si
ϕ = (¬x1 ∨ x2 ) ∧ (¬x2 ∨ x3 ) ∧ (¬x3 ∨ x4 ) ∧ (¬x1 ∨ ¬x4 )
(donc ϕ est en FNC), alors son ensemble de clauses associé est

Cϕ = { ¬x1 ∨ x2 , ¬x2 ∨ x3 , ¬x3 ∨ x4 , ¬x1 ∨ ¬x4 } .

Evidemment, étant donné un ensemble de clauses C, nous pouvons poser

^
ϕ= C
C∈C

de sorte que C = Cϕ . Les algorithmes que nous allons considérer manipulent plutôt des ensembles
des clauses, que des formules en FNC.

Remarque 1.70 (Simplifications). Avant chercher de un (ou plusieurs) modèle(s) d’une formule
sous forme clausale (ou d’un ensemble de clauses), nous pouvons optimiser les calculs qui suivront
en appliquant les règles suivantes :
Tiers exclu : Les clauses comportant deux littéraux opposés (par ex. p∨q ∨¬r ∨¬q) sont valides
(par le tiers-exclu) et peuvent donc être supprimées.
Fusion (ou factorisation) : On peut supprimer les répétitions d’un littéral au sein d’une même
clause (par ex. ¬p ∨ q ∨ ¬r ∨ ¬p équivaut à ¬p ∨ q ∨ ¬r).
Subsumption : Etant données deux clauses C et C 0 , on dit que C subsume C 0 si C est incluse
dans C 0 , c’est-à-dire, si tout littéral apparaissant dans C apparaît aussi dans C 0 .
Si un ensemble de clauses C contient deux clauses C et C 0 telles que C subsume C 0 , alors
la clause C 0 peut être supprimée de C. En effet, on a dans ce cas C |= C 0 et donc mod(C) =
mod(C \ { Cj }), par la Proposition 1.35.
Par exemple Ci = p ∨ q ∨ r est incluse dans Cj = p ∨ ¬s ∨ t ∨ q ∨ r, donc on peut supprimer
Ci d’une formule clausale de la forme C1 ∧ . . . Ci ∧ . . . Cj ∧ . . . Cn .

Remarque 1.71 (Substitutions simples). Soit ψ une formule sous forme clausale, et C l’ensemble
de ses clauses. Le calcul d’une formule équivalente à ψ[p ← ϕ], où ϕ ∈ { ⊥, > }, peut se faire
aisément via une procédure purement syntaxique sur l’ensemble C. Définissons cette procedure :
Chp ← >i : est l’ensemble obtenu de C en supprimant toutes les clauses contenant p, et en sup-
primant ¬p de toutes les clauses contenant ¬p.
Chp ← ⊥i : est l’ensemble obtenu de C en supprimant toutes les clauses contenant ¬p, et en
supprimant p de toutes les clauses contenant p.
Clairement, nous avons que
^
ψ[p ← ϕ] ≡ C.
C∈Chp←ϕi

Si ` ∈ { p, ¬p } est un littéral, nous utiliserons la notation Ch` ← >i pour Chp ← >i si ` = p, sinon,
si ` = ¬p, alors cette notation sera utilisée pour Chp ← ⊥i. C’est donc la substitution qui force ce
littéral à être vrai. Nous utiliserons la notation Ch` ← ⊥i pour Ch` ← ⊥i, ` est le littéral opposé
de ` : ` = ¬p si ` = p, et ` = p si ` = ¬p.

38 / 92
1.5 Le problème SAT 27

[Link] Algorithme de Quine

Nous présentons d’abord la méthode de Quine dans le cas restreint de formules mises au préa-
lable sous forme normale conjonctive, assimilées donc à des ensembles de clauses. La discussion
de la méthode de Quine nous aidera à comprendre de près le fonctionnement de l’algorithme de
Davis-Putnam-Logemann-Loveland.
La méthode ne fait rien d’autre que parcourir l’arbre de toutes les solutions (l’arbre dont les
branches complètes sont les valuations, appelé arbre sémantique ou arbre de Herbrand dans la
preuve du Théorème 1.41). Chaque fois qu’une variable est affectée à la valeur x ∈ { 0, 1 }, le calcul
se fait recursivement avec Chp ← ⊥i, si x = 0, et avec Chp ← >i, sinon.

Algorithme de Quine
entrée : un ensemble de clauses C
sortie : vrai si C est satisfaisable ou f aux sinon
simplifier l’ensemble de clauses (cf. Remarque 1.70) ;
si C = ∅ retourner vrai
si C contient la clause ⊥ retourner f aux
choisir le prochain p ∈ Prop apparaissant dans une clause
si Quine(Chp ← ⊥i) = vrai alors retourner vrai
sinon retourner Quine(Chp ← >i)
Exemple 1.72. Considerons { p1 ∨ p2 , ¬p1 ∨ p2 , p3 }. L’algorithme explore l’arbre de Herbrand
selon un parcours en profondeur gauche comme suit :

p1 ∨ p2
¬p1 ∨ p2
p3

p2
p3

⊥
p3 p3
f aux

⊥
f aux vrai

Observons dans l’exemple précédent que nous sommes contraintes par l’algorithme de Quine à
essayer d’abord p1 , ensuite p2 , et puis p3 ; de façon similaire, l’algorithme demande d’évaluer un
symbole propositionnel d’abord à faux, et puis à vrai. Cette stratégie nous amène le plus souvent à
des calculs inutiles : par exemple, dans l’exemple précédent, nous construisons des noeuds suite aux
évaluations de p2 et p3 à faux, quand il est tout à fait évident que ces évaluations nous amènerons
à un échec.
En principe, nous ne sommes pas obligés à suivre un ordre fixé au début. Un algorithme pourra
donc essayer d’améliorer la performance de l’algorithme de Quine, en construisant à la volée un
ordre d’exploration des symboles propositionnels et des affectations des valeurs de vérité, qui soit
optimisé pour l’ensemble des clauses passé en entrée.

[Link] Algorithme de Davis-Putnam-Logemann-Loveland

L’algorithme DPLL est considéré, à ce jour, comme l’une des méthodes les plus efficaces parmi
celles permettant de résoudre le problème SAT ; la plupart des outils de satisfaction de contraintes

39 / 92
28 Chapitre 1. Calcul propositionnel

(« SAT solvers », en anglais) implémentent une variante de cet algorithme. Il peut être vu comme
un raffinement de la méthode de Quine ; l’amélioration principale qu’il apporte est
— la réduction du branchement via la propagation des clauses unitaires ;
— l’utilisation d’heuristiques pour accélérer le parcours des solutions.

Algorithme DP LL
entrée : un ensemble de clauses C
sortie : vrai si C est satisfaisable ou f aux sinon
simplifier l’ensemble de clauses (cf. Remarque 1.70) ;
si C = ∅ retourner vrai
si C contient la clause ⊥ retourner f aux
si C contient la clause unitaire ` retourner DP LL(Ch` ← >i) propagation des
!
contraintes boo-
léennes
choisir un littéral ` depuis une clause et x, y ∈ {>, ⊥}, x 6= y décision des lit-
 
avec la bonne heuristique ! téraux
si DP LL(Ch` ← xi) = vrai alors retourner vrai
sinon retourner DP LL(Ch` ← yi) ( backtracking )

Heuristiques. Les heuristiques sont très importantes car elles permettent de réduire rapide-
ment la taille de l’arbre de recherche. Parmi les heuristiques possibles :
Littéraux purs. Si une variable propositionnelle apparaît seulement sous forme positive ou
seulement sous forme négative alors ses littéraux sont dits purs. On choisit un littéral pur
` parmi ceux qui apparaissent dans le plus de clauses, et on choisit x tel que `[` ← x] = >.
Littéraux fréquents. On appelle cette heuristique DLIS, acronyme pour l’anglais « dynamic
largest individual sum of literals ». Elle consiste à choisir un littéral parmi ceux apparaissant
les plus ; choisir x = >.
Littéraux “courts”. On appelle cette heuristique MOM’s, acronyme pour l’anglais « maximum
occurrence in clauses of minimum size ». Elle consiste à choisir un littéral parmi ceux
apparaissant les plus, dans les clauses les plus courtes ; choisir x =⊥.
Fréquence des variables. Choisir un symboles propositionnels parmi ceux qui apparaissent le
plus, dans les clauses les plus courtes ; choisir x =⊥.

Les heuristiques précédentes peuvent se formaliser en définissant des fonctions qui donnent une
pondération à chaque littéral. Par exemple, pour donner un sens à l’heuristique « choisir un symbole
propositionnel apparaissant le plus, dans les clauses les plus courtes », nous pouvons définir, pour
un littéral `,
X 1
ranklit (`, C) = ,
2cardC
`∈C,C∈C

et, pour un symbole propositionnel p,

rankprsym (p, C) = ranklit (p, C) + ranklit (¬p, C) ,

et ainsi choisir un symbole propositionnel qui maximise la fonction rankprsym . Ensuite, nous pouvons
choisir le littéral p si ranklit (p, C) > ranklit (¬p, C), et ¬p sinon.
Notez que la définition que nous avons proposé n’est pas la seule. Par exemple, nous aurions

40 / 92
1.5 Le problème SAT 29

pu tout simplement définir

ranklit (`, C) = card{ C ∈ C | cardC est mimimum dans l’ensemble { cardC | C ∈ C } }

card{ C | ` ∈ C }
ranklit (`, C) = α · card{ C | ` ∈ C } + β · ,
`∈C cardC
P

ou, si l’on souhaite aussi prendre en compte la fréquence du littéral opposé ¬`,

X 1
ranklit (`, C) = α · card{ C | ¬` ∈ C } + β · ,
2cardC
`∈C,C∈C

pour des pondérations α et β bien choisies.

Remarque 1.73. Pour qu’une heuristique soit effectivement implantée dans un SAT-solveur, il
faut disposer de structures de données permettant de calculer le littéral choisi de façon efficace.
Ainsi, certaines heuristiques décrites ci-dessus (en particulier, celle du littéral pur) ne sont pas
implémentées dans les solveurs existants les plus avancés (et performants). Voir [Sil99] pour une
comparaison des heurististiques dans les SAT-solveurs.

Exemple 1.74. Considérons l’ensemble de clauses C = { ¬x1 ∨x2 , ¬x2 ∨x3 , ¬x3 ∨x4 , ¬x1 ∨¬x4 }.
L’algorithme DPLL construit l’arbre suivant :

¬x1 ∨ x2
¬x2 ∨ x3
¬x3 ∨ x4
¬x1 ∨ ¬x4
x1 := 0, car ¬x3 est un littéral pur

¬x2 ∨ x3
¬x3 ∨ x4
x3 := 0, car x3 maximise rankprsym
et ranklit (x3 , C) = ranklit (¬x3, C)

¬x2
x2 := 0, par propagation de la
clause unitaire ¬x2

vrai

La valeur de vérité de x4 n’est pas affecté sur cette branche : cela veut dire que chaque valeur pour
x4 donne un modèle, si v(x1 ) = v(x3 ) = v(x2 ) = 0.

Exemple 1.75. Nous pouvons modifier l’algorithme DPLL (et bien sur, l’algorithme de Quine
aussi), afin qu’il trouve tous les modèles d’un ensemble de clauses. Avec le même C de l’exemple

41 / 92
30 Chapitre 1. Calcul propositionnel

précédent, l’algorithme produira le parcours suivant :

¬x1 ∨ x2
¬x2 ∨ x3
¬x3 ∨ x4
¬x1 ∨ ¬x4
x1 = 0 x1 = 1

¬x2 ∨ x3 x2
¬x3 ∨ x4 ¬x2 ∨ x3
heuristique : ¬x3 ∨ x4
x3 apparaît le plus ¬x4
x3 = 0 x3 = 1

¬x2 x4 x2 = 1

x2 = 0 x4 = 1 x3
¬x3 ∨ x4
¬x4
VRAI VRAI
x3 = 1

x4
FAUX
¬x4

Les modèles de cette formule sont donc les suivants :

x1 x3 x2 x4
0 0 0 0
0 0 0 1
0 1 0 1
0 1 1 1
On remarque dans cet exemple que :
— dans la branche de droite, la propagation des clauses unitaires permet de ne suivre qu’un
seul chemin ;
— dans la branche de gauche, l’heuristique, faisant choisir x3 plutôt que x2 ou x4 , réduit
l’exploration car elle produit plus vite des clauses unitaires.
L’exécution est meilleure que si on avait fait une simple exploration de toutes les solutions (Algo-
rithme de Quine).
Exercice 1.76. Montrez que, pour tout n ≥ 1, il existe un ensemble de clauses Cn , dont les
symboles propositionnels sont { p1 , . . . , pn } tel que l’arbre construit par l’algorithme de Quine
est un arbre complet de profondeur n (donc, avec 2n noeuds) où, par contre, l’arbre exploré par
l’algorithme DPLL est une branche de longueur n (donc, seulement n + 1 noeuds sont explorés par
l’algorithme).

[Link] Algorithmes incomplets

Il existe aussi des semi-algorithmes (ou algorithmes incomplets) très performants, ceux-ci ne
parcourent pas l’ensemble des solutions et peuvent donc ne pas répondre. En général, il ne répondent
pas à la question de l’insatisfaisabilité. Ils ont l’avantage de trouver souvent rapidement un modèle

42 / 92
1.5 Le problème SAT 31

lorsqu’il existe, mais il n’en trouvent pas toujours (même si la formule est satisfiable). Par contre,
si la formule est non-SAT, on n’obtient aucune réponse.

Algorithme de Hill Climbing (optimisation stochastique) : Au départ, on choisit une

valuation aléatoire et on dispose d’un critère de qualité (par exemple le nombre de clauses non
satisfaites). A chaque étape, on choisit une variable, on inverse la variable si cela améliore le
critère, sinon on l’inverse avec une probabilité faible (pour éviter les optimum locaux).

Algorithmes génétiques : Ces algorithmes sont inspirés de la sélection naturelle. Au départ,

on se donne aléatoirement un certain nombre de valuations qui forme la population initiale, puis
à chaque étape, on fait évoluer la population par brassage génétique en essayant de tendre vers
des modèles de la formule : par croisement des meilleurs individus, par mutation d’individus et
élimination des solutions les plus faibles.

[Link] Conclusion
Il existe donc de nombreux algorithmes, certains sont des améliorations de ceux présentés ci-
dessus, souvent par des heuristiques par exemple sur l’ordre d’utilisation des règles. Les meilleurs
complexités atteintes pour ces algorithmes oscillent entre O(1.5n ) et O(1.3n )

1.5.5 Sous-classes de SAT

[Link] 2-SAT
Le problème 2-SAT est celui de la satisfaisabilité d’une formule sous forme clausale dont les
clauses sont d’ordre 2 (i.e., chaque clause est une disjonction d’au plus deux littéraux).
Exemple : ϕ = (p1 ∨ p2 ) ∧ (¬p1 ∨ p3 ) ∧ (¬p2 ∨ p1 ) ∧ (¬p2 ∨ p3 ) ∧ (¬p1 ∨ ¬p3 ) est sous forme
clausale d’ordre deux.
Problème 2-SAT
entrée : un ensemble de clauses C d’ordre 2
sortie : vrai si C est satisfaisable ou f aux sinon
Contrairement à SAT, ce problème est solvable en temps polynomial.

Algorithme 2-SAT :
Une clause d’ordre deux `1 ∨ `2 est équivalente à (¬`1 ⇒ `2 ) ∧ (¬`2 ⇒ `1 ). Pour résoudre SAT
pour une formule ϕ d’ordre 2, on construit le graphe orienté G(ϕ) = (S, A) dual (appelé graphe
2-SAT) selon les deux règles suivantes :
— l’ensemble des sommets est S = {¬p | p ∈ Prop(ϕ)}∪Prop(ϕ) (où Prop(ϕ) est l’ensemble
des variables propositionnelles de la formule ϕ ). C’est l’ensemble des littéraux sur Prop(ϕ)
— l’ensemble des arcs est A = {(`1 , `2 ) | ϕ contient une clause équivalente à `1 ⇒ `2 }.
Chaque clause `1 ∨ `2 est donc associée à deux arcs (¬`1 , `2 ) et (¬`2 , `1 ).
Alors, la formule ϕ est insatisfaisable ssi il existe une variable p telle qu’il existe dans G(ϕ)
un chemin allant de p à ¬p et un chemin allant de ¬p à p. En effet, cela signifie alors que
ϕ |= (p ⇒ ¬p) ∧ (¬p ⇒ p) ce qui est équivalent à ⊥.

Une autre formulation est la suivante : la formule ϕ est satisfaisable si et seulement si pour
chaque variable propositionnelle p, les sommets p et ¬p du graphe 2-SAT sont dans deux com-
posantes fortement connexes distinctes. On rappelle qu’une composante fortement connexe d’un
graphe orienté G est un sous-graphe maximal de G tel que pour toute paire de sommets u et v
dans ce sous-graphe, il existe un chemin de u à v et un chemin de v à u.)
L’algorithme de Tarjan permet de calculer les composantes fortement connexes d’un graphe
orienté en O(|S| + |A|) , donc 2-SAT est bien polynomial.

Exemple 1.77. ϕ = (p1 ∨ p2 ) ∧ (¬p1 ∨ p3 ) ∧ (¬p2 ∨ p1 ) ∧ (¬p2 ∨ p3 ) ∧ (¬p1 ∨ ¬p3 )

On a :
— (p1 ∨ p2 ) ≡ (¬p1 ⇒ p2 ) ∧ (¬p2 ⇒ p1 )

43 / 92
32 Chapitre 1. Calcul propositionnel

— (¬p1 ∨ p3 ) ≡ (p1 ⇒ p3 ) ∧ (¬p3 ⇒ ¬p1 )

— (¬p2 ∨ p1 ) ≡ (p2 ⇒ p1 ) ∧ (¬p1 ⇒ ¬p2 )
— (¬p2 ∨ p3 ) ≡ (p2 ⇒ p3 ) ∧ (¬p3 ⇒ ¬p2 )
— (¬p1 ∨ ¬p3 ) ≡ (p1 ⇒ ¬p3 ) ∧ (p3 ⇒ ¬p1 )

On construit le graphe G(ϕ) = (S, A) :

p1 ¬p1

p2 ¬p2

p3 ¬p3
On remarque qu’il existe un cycle passant par p1 et ¬p1 , donc la formule est insatisfaisable.
Si on considère maintenant la formule ϕ0 = (¬p1 ∨ p3 ) ∧ (¬p2 ∨ p1 ) ∧ (¬p2 ∨ p3 ) ∧ (¬p1 ∨ ¬p3 ).
Le graphe est alors le suivant :

p1 ¬p1

p2 ¬p2

p3 ¬p3
On voit sur le graphe que ϕ0 |= p1 ⇒ ¬p1 , ϕ0 |= p2 ⇒ ¬p2 et ϕ0 |= p3 ⇒ ¬p3 . Il n’y a donc
qu’un seul modèle : v(p1 ) = v(p2 ) = v(p3 ) = 0.

[Link] 3-SAT
Le problème 3-SAT est lui aussi NP-complet (c’est à dire qu’il est aussi difficile que le problème
SAT). Pour le démontrer, il suffit de prouver que le problème SAT est polynomialement réductible
à 3-SAT : cela signifie que répondre à la question SAT revient à répondre à 3-SAT et que le temps
nécessaire à transformer SAT en 3-SAT est polynomial.
Preuve : On remarque que toute clause ϕn = `1 ∨ `2 ∨ . . . ∨ `n avec n ≥ 3 peut se mettre sous
la forme :
ψn = (`1 ∨ `2 ∨ q1 ) ∧ (`3 ∨ ¬q1 ∨ q2 ) ∧ . . . ∧ (`n−2 ∨ ¬qn−4 ∨ qn−3 ) ∧ (`n−1 ∨ `n ∨ ¬qn−3 ) où les
qi sont de nouveaux symboles propositionnels.
Donc le problème SAT est polynomialement réductible à 3-SAT. On conclut que 3-SAT est
NP-complet.
Tous les problèmes n-SAT avec n supérieur ou égal à 3 sont également des problèmes NP-
complets.

[Link] Horn-SAT
Une clause de Horn est une clause comportant au plus un littéral positif. C’est donc une
disjonction de la forme ¬p1 ∨ . . . ∨ ¬pn ∨ p, où les pi et p sont des variables propositionnelles. Selon
qu’elles comportent ou non un littéral positif (resp. négatif), les clauses de horn sont de l’une des
trois formes suivantes :

44 / 92
1.5 Le problème SAT 33

(a) ¬p1 ∨ . . . ∨ ¬pn ∨ p avec n > 0 ;

(b) ¬p1 ∨ . . . ∨ ¬pn avec n > 0 ;
(c) p ;
(d) ⊥ ;

Le problème Horn-SAT s’énonce de la façon suivante :

Horn-SAT
Entrée : un ensemble C de clauses de Horn
Question : C est-il satisfiable ?
Ce problème est résolvable en temps polynomial.

Algorithme : Il convient d’abord de remarquer les équivalences suivantes :

— ¬p1 ∨ . . . ∨ ¬pn ∨ p ≡ (p1 ∧ p2 ∧ . . . ∧ pn ) ⇒ p (avec n > 0) ;
— ¬p1 ∨ . . . ∨ ¬pn ≡ (p1 ∧ p2 ∧ . . . ∧ pn ) ⇒ ⊥ avec n > 0 ;
Si q est une variable propositionnelle, et C est une clause de Horn, on note C/q la clause de
Horn définie par
— C/q = (p2 ∧ . . . ∧ pn ) ⇒ p si C = (p1 ∧ p2 ∧ . . . ∧ pn ) ⇒ p, p1 = q et n > 0 ;
— C/q = vrai si C = (p1 ∧ p2 ∧ . . . ∧ pn ) ⇒ p, p = q et n > 0 ;
— C/q = (p2 ∧ . . . ∧ pn ) si C = (p1 ∧ p2 ∧ . . . ∧ pn ), p1 = q et n > 0 ;
— C/q = p si C = p et p 6= q
— C/q = > si C = q
— C/q = ⊥ si C = ⊥
On étend cette notation à l’ensemble de clauses : C/q = {C/q | C ∈ C}.
Les clauses réduites à une variable propositionnelle sont appelés faits.

Algorithme :
Données : Un ensemble C0 de clauses de Horn
Sortie : C0 est-il satisfaisable ?

C = C0
tant que faits(C) 6= ∅
Choisir p ∈ faits(C)
C = C/p ;
si ⊥ ∈ C alors Retourner "inconsistant"
sinon Retourner "satisfaisable" ;
En effet, tout ensemble de clauses ne contenant pas de faits ni la clause ⊥ est satisfaisable :
il suffit de mettre à 0 toutes les variables apparaissant dans les clauses.

1.5.6 Les SAT-solvers

Puisque le problème SAT est présent dans de nombreux domaines de l’informatique, le déve-
loppement de SAT-solvers efficaces est un des défis majeur de l’informatique. De nouveaux solvers
sont constamment développés pour répondre à des besoins spécifiques. Des concours mondiaux de
SAT-solvers sont d’ailleurs organisés chaque année (voir [Link]
On peut citer parmis ces nombreux solvers : zChaff datant de 2001 qui utilise l’agorithme
de Chaff qui est une amélioration de DP, Siege en 2003, MiniSAT en 2005 logiciel open-source,
picoSAT dont les méthodes s’inspirent de l’algorithme de Chaff, SARzilla en 2009 qui a gagné de
nombreux prix.
Enfin remarquons que les solvers modernes exploitent les techniques les plus recentes de l’infor-
matique, comme l’apprentissage, la programmation parallèle exploitant l’architecture multicoeur
des processeurs récents, etc.

45 / 92
34 Chapitre 1. Calcul propositionnel

1.5.7 Applications
[Link] Vérification d’un circuit logique
On encode le circuit et les entrées/sorties désirées et on teste SAT

[Link] Satisfaction de contraintes

Les problèmes de satisfaction de contraintes (CSP) sont des problèmes mathématiques où l’on
cherche des états ou des objets satisfaisant un certain nombre de contraintes ou de critères. Ici on
sort un peu du contexte simple de la décidabilité, il ne suffit plus de dire qu’une formule est vraie,
il faut en exhiber un modèle.
Les problèmes d’emploi du temps, de coloration de graphe, ou les sudoku.

Emploi du temps Pour choisir un créneau horaire pour le cours de Logique, on doit respecter
les contraintes suivantes :
— Pas en même temps que les TP de RO du M1 informatique
— Pas avant 10h30 le matin
— Pas en même temps que les autres enseignements de L3 info
— Pas en même temps que les autres enseignements obligatoires de L3 math
— Pas en même temps que tout autre cours en amphi.

[Link] Diagnostic
Le diagnostic est une discipline de l’intelligence artificielle qui vise le développement d’algo-
rithmes permettant de déterminer si le comportement d’un système est conforme au comportement
espéré. Si il ne l’est pas, il faut être capable de trouver le dysfonctionnement.
Le diagnoser doit déterminer si un système a un comportement défectueux étant donnée l’ob-
servation des entrées et sorties du système et d’observation d’états internes. Le modèle du système
peut être traduit en un ensemble de contraintes (disjonctions) : pour chaque composant S du
système, une variable propositionnelle Ab(S) est créée qui est évaluée à vraie si le composant a
un comportement anormal (Abnormal). Les observations peuvent être également traduites par un
ensemble de disjonctions. L’assignation trouvée par l’algorithme de satisfaisabilité est un diagnostic.
On peut simplifier la modélisation par des formules comme les suivantes :
¬Ab(S) ⇒ Int1 ∧ Obs1
Ab(S) ⇒ Int2 ∧ Obs2
Les formules se lisent de la manière suivante : si le système n’a pas un comportement anormal,
alors il produira le comportement interne Int1 et le comportement observable Obs1. Dans le cas
d’un comportement anormal, il produira le comportement interne Int2 et les observations Obs2.
Étant données les observations Obs, il faut déterminer si le comportement du système est normal
ou non (¬Ab(S) ou Ab(S) )

[Link] Planification
La planification est une discipline de l’intelligence artificielle qui vise le développement d’algo-
rithmes pour produire des plans (en d’autre termes, une planification), typiquement pour l’exécu-
tion par un robot ou tout autre agent.
Un planificateur typique manipule trois entrées (toutes codées dans un langage formel qui utilise
des prédicats logiques) :
— une description de l’état initial d’un monde,
— une description d’un but à atteindre et
— un ensemble d’actions possibles (parfois appelés opérateurs)
Chaque action spécifie généralement des préconditions qui doivent être présentes dans l’état
actuel pour qu’elle puisse être appliquée, et des postconditions (effets sur l’état actuel). Le problème
de planification classique consiste à trouver une séquence d’actions menant d’un état du système à
un ensemble d’états. Par exemple, voici un problème de planification simple. On dispose de boites
sur une tables, dans une configuration initiale, et on souhaite obtenir une nouvelle configuration

46 / 92
1.5 Le problème SAT 35

(par exemple passer de conf 1 de la figure à a conf 2). La seule action possible est de déplacer une
boite non recouverte par une autre sur la table ou sur une autre boite.

A B

C B C

table table

configuration 1 configuration 2

[Link] Model checking

Le Model Checking désigne une famille de techniques de vérification automatique des systèmes
dynamiques (souvent d’origine informatique ou électronique). Il s’agit de vérifier algorithmiquement
si un modèle donné, le système lui-même ou une abstraction du système, satisfait une spécification,
souvent formulée en termes de logique temporelle.
Représentation formelle : M |=? ϕ
— M : (modèle du) programme sous observation
— ϕ : propriété à vérifier
— pré-requis : sémantique (opérationnelle), langage de spécification
Exemple : voici la modélisation à partir d’une machine à état, d’une machine à café très sim-
plifiée.

cette machine est le modèle M, sur lequel on veut vérifier des propriétés ϕ (exprimées par des
formules de logique) telles que "on obtient un café seulement si on paie 2 euros".
Un exemple de model checker : POEM est un model checker développé au LIF par Peter Niebert
qui utilise un SAT-solver pour finaliser ses calculs.

[Link] Cryptographie
La complexité du problème SAT est une composante essentielle de la sécurité de tout système
de cryptographie.
Par exemple une fonction de hachage sécurisée constitue une boîte noire pouvant être formulée
en un temps et un espace fini sous la forme d’une conjonction de clauses normales, dont les variables
booléennes correspondent directement aux valeurs possibles des données d’entrée de la fonction de
hachage, et chacun des bits de résultat devra répondre à un test booléen d’égalité avec les bits de
données d’un bloc de données d’entrées quelconque. Les fonctions de hachages sécurisées servent
notamment dans des systèmes d’authentification (connaissance de données secrètes d’entrée ayant
servi à produire la valeur de hachage) et de signature (contre toute altération ou falsification "facile"
des données d’entrée, qui sont connues en même temps que la fonction de hachage elle-même et de
son résultat).

47 / 92
36 Chapitre 1. Calcul propositionnel

[Link] Bio-informatique
Certains problèmes de traitement du génome se modélisent par des formules propositionnellse
et sont résolus à l’aide de SAT-solvers.

1.5.8 Sur la modélisation

Tous les applications citées ci-dessus ont un point commun : partant d’un problème qui semble
complètement éloigné de la logique, on obtient une solution à ce problème en résolvant le problème
SAT. La phase important de ce travail est donc la modélisation, qui permet par abstraction d’un
objet concret d’obtenir un modèle représentant son fonctionnement et/ou ses propriétés. Dans le
cas cas qui nous intéresse, le modèle est une formule du calcul propositionnel.
Ce mécanisme est très puissant, il permet de résoudre des problèmes très concrets, d’ingénierie
par exemple, en utilisant des résultats théoriques existant sur des objets mathématiques.

48 / 92
1.6 Systèmes de preuves 37

1.6 Systèmes de preuves

1.6.1 La notion de système formel
Un système de preuves définit des règles d’inférence entre formules qui simulent le raisonnement.
Il est défini par :
— le langage et les formules sur ce langage,
— les axiomes, c’est-à-dire les formules supposées être toujours vraies,
— les règles d’inférence. Une règle d’inférence permet de déduire une nouvelle formule, la
conclusion, à partir d’un ensemble de formules, les prémisses ou hypothèses.
On note ` ϕ si ϕ peut se déduire grâce au système de preuves, i.e., s’il est possible de l’obtenir
à partir des axiomes, en appliquant itérativement les règles d’inférence du système. Si Γ est un
ensemble de formules, on note alors Γ ` ϕ si ϕ peut se déduire dans le système de preuve à partir
des axiomes et des formules dans Γ.
Deux questions fondamentales sont systématiquement posées pour relier le calcul et la sé-
mantique dans une logique : existe-il un système de preuve qui soit
1. correct : toute formule déduite est une tautologie ;
2. complet : toute tautologie peut se déduire.
Par extension, un système formel est un ensemble de règles permettant d’inférer des nouvelles
conclusions à partir des prémisses. Les objets inférés peuvent être de nature différente des formules.
Par exemple, le calcul des séquents (voir Section 1.7) est un système formel qui permet de déduire
des couples de la forme (Γ, ∆) (notée comme habituellement par Γ ` ∆), où Γ et ∆ sont des multi-
ensembles (i.e. des listes, mais où l’ordre ne compte pas) de formules, à partir d’autres couples
du même type. Les théorèmes de correction et complétude pour le calcul des séquents montrent
qu’on peut déduire le couple (Γ, ∆) dans le calcul si est seulement si la formule δ∈∆ δ est une
W
conséquence logique de Γ.

1.6.2 La méthode de la coupure

Introduite en 1965 par Robinson, la résolution est un système formel pour le calcul des prédicats
qui utilise des formules sous formes de clauses ; nous présenterons ce système plus tard (Section 2.7).
Ici, nous allons présenter la méthode de la coupure, qui n’est rien d’autre que la restriction de la
résolution à la logique propositionnelle.

[Link] Le système

Ce système formel dérive des nouvelles clauses à partir de clauses données. Il n’a pas
d’axiomes, et comporte deux règles d’inférence (voir aussi la Figure 1.4) :
Factorisation : si une clause contient deux fois le même littéral, on en supprime une copie :
on infère la clause C ∨ ` à partir de la clause C ∨ ` ∨ `.
Coupure (ou règle de résolution) : si deux clauses contiennent l’une un symbole proposi-
tionnel et l’autre sa négation (C ∨p et C 0 ∨¬p), on infère la clause C ∨C 0 , appelée résultante
ou résolvante de C ∨ p et C 0 ∨ ¬p (on utilisera la notation ρ(p, C ∨ p, C ∨ ¬p) pour dénoter
cette clause).

C ∨`∨`
factorisation
C ∨`

C ∨` C 0 ∨ ¬` ` ¬`
coupure coupure (cas particulier)
0
C ∨C ⊥

Figure 1.4 – Règles d’inférence pour la méthode de la coupure

49 / 92
38 Chapitre 1. Calcul propositionnel

On peut utiliser ce système formel pour :

1. montrer qu’une formule (ou un ensemble de formules) est contradictoire (ou admet un
modèle) ;
2. montrer qu’une formule est une tautologie (ou non) : on montre que sa négation est contra-
dictoire. On dit que la méthode de la coupure est réfutationnelle : pour prouver la formule
ϕ, on suppose ¬ϕ et on montre que cela conduit à une contradiction ;
3. montrer qu’une formule ϕ est une conséquence logique d’un ensemble de formules Γ : on
montre que l’ensemble Γ ∪ { ¬ϕ } est contradictoire.

Exemple 1.78. Soit la formule ϕ = (p ∨ r ∨ s) ∧ (r ∨ ¬s) ∧ ¬r ∧ ¬p ; cette formule s’écrit comme

l’ensemble de clauses C = {(p ∨ r ∨ s), (r ∨ ¬s), ¬r, ¬p}. Voici une dérivation par résolution à
partir de cet ensemble de clauses :
p∨r∨s r ∨ ¬s
coupure
p∨r∨r
factorisation
p∨r ¬r
coupure
p ¬p
coupure
⊥
Puisqu’on arrive à dériver la clause vide, la formule ϕ est insatisfaisable.
Exemple 1.79. L’exemple suivant montre qu’on peut avoir besoin d’utiliser deux fois une clause
pour dériver la clause vide. Soit ϕ la formule ((p ⇒ q) ∧ (q ⇒ p) ∧ (p ∨ q)) ⇒ (p ∧ q). On veut
montrer que ϕ est est une tautologie, on met donc ¬ϕ sous forme clausale, on obtient l’ensemble
de clause C = {(p ∨ ¬q), (¬p ∨ q), (p ∨ q), (¬p ∨ ¬q)}. Une preuve par la méthode de la coupure est
la suivante :
p ∨ ¬q ¬q ∨ ¬p
coupure
¬q ∨ ¬q
factorisation
¬q ¬p ∨ q
coupure
¬p p∨q
coupure
q ¬q
coupure
⊥
Donc nous avons montré qu’on peut dériver ⊥ à partir de C = {(p ∨ ¬q), (¬p ∨ q), (p ∨ q), (¬p ∨ ¬q)}.
Remarquez que la clause ¬q est utilisée deux fois ; aussi, l’exemple montre que la règle de
factorisation est nécessaire, sans elle toutes les résolvantes ont deux littéraux et on ne peut donc
jamais dériver la clause vide.
Remarque 1.80. L’exemple précédent montre que l’ordre de littéraux dans une clause n’est pas
important quand on applique la règle de coupure. Nous avons en fait inféré comme suit :
p ∨ ¬q ¬q ∨ ¬p
coupure
¬q ∨ ¬q
au lieu d’avoir, dans la première prémisse, ¬q ∨ p.
De façon semblable, l’ordre de littéraux n’est pas important afin d’appliquer la règle de facto-
risation.

[Link] Correction et complétude

Notation 1.81. Nous allons écrire C `R ψ si nous pouvons dériver la clause ψ à partir des clauses
de l’ensemble C, par application successive des règles de la méthode de la coupure. C’est-à-dire,
C `R ψ signifie qu’il existe une suite finie d’ensembles de clauses C0 , C1 , . . . , Cn vérifiant :
1. C0 = C ;

50 / 92
1.6 Systèmes de preuves 39

2. pour tout i ∈ [0, n−1], Ci+1 = Ci ∪{ ψi+1 }, où ψi+1 est la conséquence d’une règle du système
(factorisation ou coupure) dont les prémisses appartiennent à Ci ;
3. Cn = Cn−1 ∪ { ψn }, avec ψn = ψ.

Théorème 1.82. La résolution est correcte ; c’est-à-dire, si C `R ⊥, alors C est insatisfaisable.

Démonstration. C `R ⊥ signifie qu’il existe une suite finie d’ensembles de clauses C0 , C1 , . . . , Cn

vérifiant :
— C0 = C ;
— pour tout i ∈ [0, n − 1], on obtient Ci+1 en appliquant une des deux règles de la méthode de
la coupure à Ci ;
— Cn contient la clause ⊥.
On remarque facilement qu’alors pour tout i ∈ [0, n − 1], Ci+1 a exactement les mêmes modèles
que Ci . En effet,
— si la règle appliquée est la coupure, alors il existe une variable p et deux clauses C1 , C2 dans
Ci telles que Ci+1 = Ci ∪ {R(p, C1 , C2 )}, où R(p, C1 , C2 ) est la résolvante de C1 et C2 par
rapport à p. Trivialement, R(p, C1 , C2 ) est une conséquence logique de {C1 , C2 } et donc une
conséquence logique de Ci . La Proposition 1.35 permet donc de conclure immédiatement que
Ci+1 et Ci ont exactement les mêmes modèles.
— si la règle appliquée est la factorisation, il est évident que la modèles de Ci+1 et Ci sont les
mêmes.
En conclusion, C0 et Cn ont exactement les mêmes modèles, Cn contient la clause ⊥, il est donc
est insatisfaisable, donc C = C0 est insatisfaisable.

Définition 1.83. Un ensemble de clauses est dit saturé si on ne peut pas produire des nouvelles
clauses par application de la règle de coupure.
Théorème 1.84. La résolution est complète. C’est-à-dire : si C est insatisfaisable, alors C `R ⊥.

Démonstration. Par le théorème de compacité, nous pouvons assumer que C est un ensemble fini ;
donc les symboles propositionnels apparaissant dans ses clauses sont en nombre fini.
Nous allons montrer que si C 6`R ⊥, alors C est satisfaisable. Or la condition C 6`R ⊥ revient à
dire que ⊥ 6∈ S, où S = { C | C `R C }. Il est facile à voir que S est un ensemble saturé ; même
si potentiellement infini, l’ensemble des variables propositionnelles qui ont une occurrence dans S
est fini. Nous allons donc montrer qu’un tel ensemble S
— saturé,
— avec un nombre fini de variables propositionnelles,
— tel que ⊥ 6∈ S,
est satisfaisable ; le résultat découle ensuite du fait que C ⊆ S et donc mod(S) ⊆ mod(C).
On suppose donc que S est saturé et ne contient pas la clause ⊥ et on montre que S a un
modèle. On fait la preuve par récurrence sur le nombre n de symboles propositionnels de S.
Cas de base : n = 1. Soit donc p le seul symbole propositionnel qui a une occurrence dans S.
Car il est saturé, S ne peut contenir à la fois les deux clauses unitaires p et ¬p, sinon il
contiendrait aussi la clause vide. Donc S admet un modèle.
Pas d’induction. Supposons la propriété vraie pour n et que S contient n + 1 symboles propo-
sitionnels. Soit p un symbole propositionnel apparaissant dans une clause de S. On définit :
S0 := { C ∈ S | ¬p 6∈ C } , S00 := S0 [p ← ⊥] ,
S1 := { C ∈ S | p 6∈ C } , S10 := S1 [p ← >] .
En utilsant la notation introduite avec la Remarque 1.71, on a S00 = S[p ← ⊥] et S10 = S[p ←
>]. Remarquez que ⊥ ∈ S00 implique que p ∈ S0 ; aussi S00 est saturé. Par exemple, pour
q 6= p, on a bien
R(q, C1 [p ← ⊥], C2 [p ← ⊥]) = R(q, C1 , C2 )[p ← ⊥] ,

51 / 92
40 Chapitre 1. Calcul propositionnel

C1 ∨ q C2 ∨ ¬q C1 [p ← ⊥] ∨ q C2 [p ← ⊥] ∨ ¬q
C1 ∨ C2 C1 [p ← ⊥] ∨ C2 [p ← ⊥]

Figure 1.5 – Commutation de la coupure par rapport à la substitution

comme suggéré par la Figure [Link]. De même, S10 est saturé, et ⊥ ∈ S10 implique ¬p ∈ S1 .
En particulier, si ⊥ ∈ S00 ∩ S10 , alors p ∈ S0 ⊆ S et ¬p ∈ S1 ⊆ S ; car S est saturé, alors on
obtient ⊥ ∈ S, une contradiction.
Par conséquent, un parmi Si0 , i = 0, 1, est saturé et ne contient pas la clause vide ; sans perte
de généralité, nous pouvons supposer qu’il s’agit de S10 . Par hypothèse d’induction, soit v un
modèle de S10 . Soit u la valuation telle que u(p) = 1 et u(q) = v(q) pour p 6= q ; alors u est
un modèle de S. En fait, si C ∈ S1 , alors p 6∈ C, et
1 = v(C[p ← >]) = u(C[p ← >]) ≤ u(C ∨ ¬p) = max(u(C), 0) = u(C) ;
sinon C 6∈ S1 , donc p ∈ C, et 1 = u(p) ≤ u(C).

[Link] L’algorithme de résolution

On peut extraire, de le méthode de la coupure, un (semi)-algorithme pour décider si une formule
ϕ est une tautologie : pour prouver qu’une formule ϕ est une tautologie, on peut procéder en trois
étapes :
1. mettre ¬ϕ sous forme clausale, ¬ϕ = C1 ∧ · · · ∧ Cn , où toute clause est factorisée ;
2. remplacer la conjonction de clauses C1 ∧ . . . ∧ Cn par l’ensemble C = {C1 , . . . , Cn } ;
3. saturer l’ensemble en rajoutant à C les clauses (factorisés) qu’on peut déduire à partir des
deux règles de résolution.
L’algorithme termine lorsque :
(a) soit on vient d’ajouter la clause ⊥ et donc la formule initiale est insatisfaisable ;
(b) soit l’application des règles ne modifie plus l’ensemble de clauses.
Malheureusement, seulement (a) — l’ensemble des clauses contient ⊥ — peut être considéré
comme un vrai critère de terminaison. Si la formule à démontrer n’est pas un théorème, il faut soit
montrer à la main qu’il n’est pas possible d’engendrer des résolvantes qui ne sont pas déjà dans
l’ensemble de clauses, soit avoir un critère permettant d’arrêter de générer de nouvelles résolvantes.
A la main, sur des exemples simples on peut souvent arrêter la résolution car on obtient un
ensemble de clauses (clauses initiales plus toutes les clauses déduites) pour lequel on trouve un
modèle. Ce modèle est donc un contre-exemple à la formule initiale qui n’est donc pas prouvable
(c’est une conséquence des propriétés de complétude et correction).
Exemple 1.85. Si on considère l’ensemble de clauses C = {p ∨ ¬q, q ∨ ¬p}. La méthode engendre
{p ∨ ¬p, q ∨ ¬q, p ∨ ¬q, q ∨ ¬p} (et rien de plus, mais il faut un raisonnement pour le prouver !) qui
a un modèle v(p) = 1, v(q) = 1. Donc la formule ¬((p ∨ ¬q) ∧ (q ∨ ¬p)) n’est pas une tautologie.
On voit sur l’exemple suivant que la méthode de la coupure peut engendrer un ensemble infini
de clauses et donc ne pas terminer.
Exemple 1.86. C = {p ∨ ¬p ∨ ¬q}. On commence par appliquer la règle de coupure, et on obtient
la clause p ∨ ¬p ∨ ¬q ∨ ¬q, si lui applique la règle de factorisation, on retombe sur la clause initiale
p ∨ ¬p ∨ ¬q, ce qui est inutile. On ne peut donc que réappliquer la coupure aux clauses p ∨ ¬p ∨ ¬q
et p ∨ ¬p ∨ ¬q ∨ ¬q.

p ∨ ¬p ∨ ¬q p ∨ ¬p ∨ ¬q
coupure
p ∨ ¬p ∨ ¬q ∨ ¬q p ∨ ¬p ∨ ¬q
coupure
p ∨ ¬p ∨ ¬q ∨ ¬q ∨ ¬q p ∨ ¬p ∨ ¬q
coupure
..
.

52 / 92
1.7 Les règles du calcul des séquents 41

La méthode va générer les clauses de la forme p ∨ ¬p ∨ ¬q ∨ ¬q ∨ . . . ¬q et aucune autre (la

encore un raisonnement est à faire). Donc la méthode ne termine pas et engendre un ensemble de
clauses infini qui ne contient pas la clause vide. On peut conclure soit en trouvant directement un
modèle (on peut en trouver plusieurs ici) soit en appliquant le résultat démontré dans la preuve de
complétude : un ensemble de clauses saturé qui ne contient pas la clause vide a un modèle. Donc
la formule ¬(p ∨ ¬p ∨ ¬q) n’est pas une tautologie.

On peut modifier la méthode pour obtenir un algorithme qui se termine toujours, si on se

restreint à considérer les clauses factorisées.
Définition 1.87. Une clause C est factorisée si elle ne contient pas deux occurrences du même
littéral.
Si C est une clause, nous allons dénoter par f(C) la clause factorisée obtenue de C par une suite
de règles de factorisation. L’algorithme se présente donc comme en Figure 1.6. La terminaison de
l’algorithme est assurée par le fait que le nombre de clauses factorisées ayant au plus n symboles
propositionnels est borné supérieurement par une fonction de n.

Algorithme Res
entrée : un ensemble de clauses C factorisés
sortie : insatisfaisable si C |= ⊥ ou satisfaisable sinon
si ⊥ ∈ C, alors retourner : insatisfaisable ;
(réduire l’ensemble C via la règle de subsumption ;)
si C ∨ p, C 0 ∨ ¬p ∈ C, avec f(R(p, C ∨ p, C 0 ∨ ¬p)) 6∈ C,
alors retourner Res(C ∪ { f(R(p, C ∨ p, C 0 ∨ ¬p)) }) ;
sinon retourner : satisfaisable.

Figure 1.6 – L’algorithme de coupure (ou de résolution)

Exercice 1.88. Estimer cette borne supérieure.

L’algorithme peut aussi être optimisé si on maintient un ensemble de clauses tel que, chaque
fois que C0 , C1 ∈ C, alors ni C0 subsume C1 , ni C1 subsume C0 . Rappelons qu’une clause C0
subsume une clause C1 si C0 ⊆ C1 (i.e., si C1 ≡ C0 ∨ C10 , ou encore tout littéral apparaissant
dans C0 apparaît aussi dans C1 ) ; si C0 subsume C1 , alors C0 |= C1 , et donc si C0 , C1 ∈ C, alors
mod(C) = mod(C \ { C1 }).

1.7 Les règles du calcul des séquents

Règles structurelles

Γ, ϕ, ϕ ` ∆ Γ ` ∆, ϕ, ϕ
(GContr ) (DContr )
Γ, ϕ, ` ∆ Γ ` ∆, ϕ
Γ`∆ Γ`∆
(GAf f ) (DAf f )
Γ, ϕ ` ∆ Γ ` ∆, ϕ

Règles logiques

53 / 92
42 Chapitre 1. Calcul propositionnel

Γ ` ϕ, ∆ Γ, ϕ ` ∆
(G¬ ) (D¬ )
Γ, ¬ϕ ` ∆ Γ ` ¬ϕ, ∆

Γ, ϕ, ψ ` ∆ Γ ` ϕ, ∆ Γ ` ψ, ∆
(G∧ ) (D∧ )
Γ, ϕ ∧ ψ ` ∆ Γ ` ϕ ∧ ψ, ∆

Γ, ϕ ` ∆ Γ, ψ ` ∆ Γ ` ϕ, ψ, ∆
(G∨ ) (D∨ )
Γ, ϕ ∨ ψ ` ∆ Γ ` ϕ ∨ ψ, ∆

Γ ` ϕ, ∆ Γ, ψ ` ∆ Γ, ϕ ` ψ, ∆
(G⇒ ) (D⇒ )
Γ, ϕ ⇒ ψ ` ∆ Γ ` ϕ ⇒ ψ, ∆

Règle de coupure

Γ1 ` ϕ, ∆1 Γ2 , ϕ ` ∆2
(C)
Γ 1 , Γ 2 ` ∆1 , ∆2

54 / 92
1.8 Résumé 43

1.8 Résumé

Formules propositionnelles
Les briques de base des formules propositionnelles sont les propositions appelées aussi sym-
boles propositionnels ou atomes ou formules atomiques ou variables propositionnelles.
On note Prop l’ensemble des propositions. L’ensemble Prop0 des formules propositionnelles
est le plus petit ensemble contenant Prop et clos par l’application des connecteurs ∧, ∨, ¬, ⇒.
Un littéral est une formule atomique ou la négation d’une formule atomique. Une clause
disjonctive est une disjonction de littéraux. Une clause conjonctive est une conjonction de
littéraux. Une formule conjonctive, ou formule sous forme normale conjonctive (FNC),
est une conjonction de clauses disjonctives. Une formule disjonctive, ou formule sous forme
normale disjonctive (FND), est une disjonction de clauses conjonctives. En résumé, ces quatres
notions recouvrent les formes suivantes :
n
^ n
_
Clause conjonctive : `i ; Clause disjonctive : `i ;
i=1 i=1

m _
n n
m ^
`ji `ji .
^ _
FNC : ; FND :
j=1 i=1 j=1 i=1

où les `i et `ji sont des littéraux.

Modèles d’une formule

Une valuation est une application de Prop dans {0, 1}. La notion de valuation peut-être
étendue aux formules, ce qui permet de calculer la valeur d’une formule en fonction de la valeur de
ses atomes. L’ensemble des valuation d’un ensemble de propositions Prop est noté Val(Prop) (ou
juste Val lorsqu’il n’y a pas d’ambiguité sur Prop). Un modèle d’une formule ϕ est une valuation
v telle que v(ϕ) = 1. Si v est un modèle de ϕ on note v |= ϕ. On note mod(ϕ) l’ensemble des
modèles de ϕ.
Une formule est satisfaisable si elle admet un modèle, insatisfaisable dans le cas contraire.
Une tautologie (ou formule valide) est une formule vraie pour toute valuation. On note |= ϕ
pour dire que ϕ est une tautologie.
Une formule ψ est conséquence logique d’une formule ϕ si tout modèle de ϕ est un modèle
de ψ. On note alors ϕ |= ψ. Deux formules ϕ et ψ sont dites équivalentes si mod(ϕ) = mod(ψ),
on note alors ϕ ≡ ψ.

Modèles d’un ensemble de formules

Un modèle d’un ensemble de formules Γ est une valuation v telle que v(ϕ) = 1 pour tout
ϕ ∈ Γ. On note mod(Γ) l’ensemble des modèles de Γ. Un ensemble de formules Γ est satisfaisable
ou consistant si il admet au moins un modèle, contradictoire (ou insatisfaisable) dans le cas
contraire.
Une formule ϕ est conséquence logique d’un ensemble Γ de formules si et seulement si
mod(Γ) ⊆ mod(ϕ)). On note alors Γ |= ϕ. On note cons(Γ) l’ensemble des conséquences logiques
de Γ. On a : (i) Γ |= ϕ ssi Γ ∪ {¬ϕ} est contradictoire. (ii) Σ ⊆ Γ alors mod(Γ) ⊆ mod(Σ).
Compacité : Un ensemble Γ de formules est consistant si et seulement si chaque partie finie de
Γ est consistante. Un ensemble Γ de formules est inconsistant si et seulement il existe une partie
finie de Γ consistante.

55 / 92
44 Chapitre 1. Calcul propositionnel

Système de preuve.
Une logique comporte une syntaxe (pour définir les formules), une sémantique (pour définir
le sens d’une formule), un système formel (un calcul pour prouver une formule). Un système
formel est correct s’il ne prouve pas de formules qui ne sont pas vraies ; il est complet s’il
permet de prouver tout ce qui est vrai. La résolution et la déduction naturelle sont corrects
et complets.

56 / 92
Chapitre 2

Calcul des prédicats

2.1 Introduction
Le calcul des propositions est bien trop limité pour décrire des situations réelles. En effet il ne
permet que de décrire des phrases dont la vérité ne dépend pas des individus (par exemple « Il
pleut ») ; il ne peut pas représenter des phrases qui mettent en jeu des individus ou des objets (par
exemple « Si x est le père de y et si z est le père de x alors z est un grand-père de y » ou « Tout
individu a un père »).
Le calcul des prédicats (ou Logique du Premier Ordre) permet d’exprimer de telles relations
entre individus, il est donc bien plus riche que le calcul propositionnel. En premier lieux, il contient
des individus (ou entités) (donnés par des symboles de variables x, y, z, . . .). Il contient des fonctions
(f, g, . . . , s, . . .) permettant de transformer des entités en autres entités (par exemple la fonction qui
associe une personne à son père), et des relations (. . . , P, Q, R, . . .) permettant de lier les individus
entre eux.
Les relations appliquées aux entités (par exemple R(x, f (y))) peuvent être évaluées à vrai ou
faux (selon les valeurs attribuées aux entités, aux fonctions et aux relations) et servent de briques de
base à un langage du premier ordre obtenu à l’aide des connecteurs logiques du calcul propositionnel
et de deux autres connecteurs appelés quantificateurs.
Le calcul des prédicats est donc très similaire à celui des propositions. On aura des formules
définies inductivement à partir des symboles de prédicats et de fonctions. On les interprétera dans
divers mondes possibles et alors elles deviendront vraies ou fausses. On aura également un système
formel correct et complet pour démontrer ou réfuter des formules.
Il y a néanmoins une différence algorithmique importante : le calcul des prédicat est indécidable :
il est absolument impossible de vérifier qu’une formule est vraie pour toute interprétation. Ceci
vient du fait que :

1. il existe un nombre non borné d’interprétations possible. Il n’est donc pas possible de toutes
les tester une à une

2. les interprétations comportent en général une infinité d’individus, il est donc pas toujours
possible de vérifier qu’une interprétation donnée est modèle d’une formule (par exemple de
vérifier que ∀xϕ puisque x peut prendre une infinité de valeurs différentes).

2.2 Préliminaires - Exemple introductif

Nous rappelons ici les notions de base sur les relations et fonctions.

47

57 / 92
48 Chapitre 2. Calcul des prédicats

2.2.1 Produit d’un ensemble

Si D est un ensemble, alors Dn dénotera le produit cartésien de D avec lui-même n-fois. C’est
l’ensemble des tuplets de longueur n dont les éléments sont tous tirés de D. Soit :

Dn = D × D × . . . × D := { (d1 , d2 , . . . , dn ) | di ∈ D, pour i = 1, . . . , n } .
| {z }
n-fois

Remarquez que nous pouvons donner un sens à l’ensemble Dn avec n = 0 :

D0 := { () } .

Notez que D0 ne désigne pas l’ensemble vide !

2.2.2 Les relations

Etant donné un ensemble E, et n ≥ 0 un entier. Une relation n-aire (ou d’arité n) sur E est
un sous-ensemble de E n .

Exemple 2.1.
1. E = {1, 2, 3} et R est la relation binaire (d’arité 2) définie par R = {(1, 1), (2, 2), (3, 3)}.
2. E = N et S est la relation d’arité 2 définie par S = {(n, n + 1) | n ∈ N}.
3. E = {1, 2, 3} et R est la relation unaire (d’arité 1) définie par R = {1, 2}.

Si R est une relation d’arité n, on note R(a1 , . . . , an ) ssi (a1 , . . . , an ) ∈ R.

2.2.3 Les fonctions

Etant donné un ensemble E, et n un entier positif, une fonction n-aire (ou d’arité n) sur E
est une fonction de E n dans E. Une fonction n’est pas une forcément une application : elle peut
être non définie pour certains éléments de E n , dans ce cas on dira que c’est une fonction partielle.
Exemple 2.2.
1. E = {1, 2, 3} et f est la fonction binaire (d’arité 2) définie pour tout couple (a, b) ∈ E 2
par :
— f (a, b) = 1 si a = 1 et b = 2,
— f (a, b) = 2 si a = 2 et b = 3,
— f (a, b) = 3 si a = 3 et b = 1,
— f (a, b) est indéfinie sinon (i.e., pour les couples (1, 1), (2, 2), (3, 3)(3, 2), (2, 1), (1, 3)).
2. E = N et f est la fonction d’arité 1 définie pour tout n ∈ N par f (n) = n + 1.
Remarque 2.3. En particulier, le lecteur observera que les fonctions d’arité 0, f : D0 → D sont
en bijection avec les éléments d ∈ D (via l’évaluation f () = d ∈ D). Nous allons donc identifier
une fonction d’arité 0 à une constante, c’est-à-dire à un élément d ∈ D.

2.2.4 Un exemple
Avant d’en venir aux définitions formelles, voici quelques formules du premier ordre. Ici, P
et Q désignent deux relations binaires et f une fonction unaire. Les lettres x, y et z désignent
des variables. Vous pouvez reconnaitre également les connecteurs logique introduits dans le calcul
propositionnel, ainsi que deux quantificateurs que vous connaissez certainement ∀ qui se lit « pour
tout » et ∃ qui se lit « il existe ».
ϕG : ∀x∀y∀z(P (x, y) ∧ P (y, z)) ⇒ G(x, z)
ϕP : ∀x∃yP (y, x)
ϕC : ∀x∃yG(y, x)
ϕD : ∀x∀zP (z, f (x)) ⇒ G(z, x)

58 / 92
2.2 Préliminaires - Exemple introductif 49

ϕF : (ϕG ∧ ϕP ) ⇒ ϕC .
Il est ici impossible de donner une valeur de vérité à toutes ces formules, et ce pour différentes
raisons :
— on ne sait pas dans quel ensemble D sont prises les valeurs x, y, z
— on ne connait pas la valeur de la fonction f : D → D
— on ne connait pas la valeur des relations P ⊆ D × D, et G ⊆ D × D
Il est donc nécessaire de choisir une interprétation pour évaluer ces formules. Toutefois, nous
verrons que c’est inutile pour la formule ϕF qui est vraie pour toute interprétation (c’est une
tautologie, ou un théorème).
Considérons donc diverses interprétations de ces formules.

[Link] Interprétation 1
Les individus sont les êtres humains. La relation P (x, y) signifie que x est le père de y. La
relation G(x, y) signifie que x est un grand-père de y. La fonction f associe à un individu sa mère.
ϕG signifie alors : pour tous êtres humains x, y, z, si (x est le père de y et y est le père de z)
alors (x est un grand-père de z).
ϕP signifie : « pour tout individu x il existe un individu y tel que y est le père de x » soit, plus
simplement, « tout individu a un père ».
ϕC signifie que « pour tout individu x il existe un individu y tel que y est le grand-père de x »
soit, plus simplement, « tout individu a un grand-père ».
ϕD dit que si z est le père de la mère de x alors z est un grand père de x.
Ces quatre formules sont vraies dans cette interprétation 1 .
L’implication ϕF : ((ϕG ∧ ϕP ) ⇒ ϕC ) est donc vraie dans cette interprétation.
On remarquera que les deux formules ϕP et ϕG sont loin de modéliser toutes les propriétés des
relations G et P . On n’a pas dit que « le père de chaque individu est unique », ni qu’« un individu
x peut-être le grand-père d’un autre z sans qu’il existe un individu dont x soit le père et qui soit
le père de z » (le grand-père maternel).

[Link] Interprétation 2
a → b
Les individus sont les quatre sommets a, b, c, d du graphe suivant : ↑ ↓
d ← c
P (x, y) signifie que x précède immédiatement y sur le graphe.
G(x, y) signifie que x suit immédiatement y sur le graphe.
La formule ϕP signifie que tout point a un prédécesseur immédiat, et elle vraie.
La formule ϕG signifie que pour tous points x, y, z, si x précède immédiatement y et si y précède
immédiatement z, alors x suit immédiatement z. Elle est fausse. Finalement la formule ϕC signifie
que tout point a un successeur immédiat. Elle est également vraie.
L’implication ((ϕP ∧ ϕG ) ⇒ ϕC ) est donc vraie dans cette interprétation.

[Link] Interprétation 3
Les individus sont les nombres entiers positifs.
P (x, y) signifie que y = x + 1. Par exemple P (4, 5) est vraie, mais P (5, 4) est fausse.
G(x, y) signifie que y = x + 2. Par exemple P (4, 6) est vraie, mais P (6, 4) est fausse.
La formule ϕP signifie alors que pour tout entier y, il existe un entier x tel que y = x + 1. Elle
est fausse : pour y = 0 un tel entier positif n’existe pas.
La formule ϕG signifie que pour tous entiers x, y, z, si y = x + 1 et z = y + 1 alors z = x + 2.
Elle est vraie.
Finalement la formule ϕC signifie que pour tout entier x, il existe un entier z tel que x = z + 2.
Elle est fausse : pour x = 0 il n’existe pas de tel entier positif.
L’implication ((ϕP ∧ ϕG ) ⇒ ϕC ) est donc vraie dans cette interprétation.
1. Sauf peut-être ϕP : soit il y a un premier homme et celui-ci n’a pas de père, soit on se retrouve peu à peu, en
remontant l’évolution, à inclure dans le genre humains des singes, des poissons, des bactéries, . . .

59 / 92
50 Chapitre 2. Calcul des prédicats

[Link] Comparaison des interprétations

On est donc tout à fait libre d’interpréter les formules dans un « monde » de son choix, de
sorte que certains énoncés deviennent vrais ou faux. On remarque néanmoins que pour chacune
des interprétations considérées, l’implication ((ϕP ∧ ϕG ) ⇒ ϕC ) est vraie. Ce n’est pas un hasard,
cette formule est une tautologie du calcul des prédicats. Elle est vraie dans toute interprétation.

2.3 Expressions et formules

2.3.1 Les termes

Définition 2.4 (Signature). Une signature est un ensemble S de symboles muni d’une application
ρ : S → N, appelée arité.
On écrira une signature comme un ensemble de couples. Par exemple, { (f, 2), (g, 1), (h, 0) }
est la signature dont les symboles sont f, g, h, d’arité 2, 1 et 0, respectivement. Formellement, on
a ici S = { f, g, h }, ρ(f ) = 2, ρ(g) = 1, ρ(h) = 0. Un symbole f ∈ S tel que ρ(f ) = 0 est appelé
constante.
Définition 2.5 (Termes). Étant donné une signature S et un ensemble X (de variables indivi-
duelles), l’ensemble TS (X) des termes est le plus petit ensemble tel que :
— x ∈ TS (X) pour toute variable x ∈ X
— si f ∈ S est d’arité n ≥ 0 et si t1 , . . . , tn ∈ TS (X), alors f (t1 , . . . , tn ) ∈ TS (X).
C’est-à-dire qu’un terme est une expression formée à partir de X en utilisant les symboles de
S de sorte qu’un symbole f soit appliqué à un nombre de termes égal à ρ(f ). En particulier,
si f ∈ S est une constante, alors elle s’applique a une liste vide de termes : f () est un terme ;
pour simplifier la notation, on écrit également f . Un terme est dit clos si il ne contient aucune
variable.

Exemple 2.6. La signature de l’arithmétique contient la constante 0, le symbole s d’arité 1 (qui

représente la fonction « successeur »), et les symboles + et × d’arité 2. On emploie la notation
S = {(0, 0), (s, 1), (+, 2), (×, 2)} pour représenter cette signature. Ainsi, pour x, y ∈ X, l’expression
+(×(s(s(0)), x), s(y)) (que nous nous autoriserons à écrire (s(s(0)) × x) + s(y)) est un terme de
TS (X) qu’on peut représenter par l’arbre suivant :

× s

s x y

En fait, tout terme est un arbre à branchements finis. Leur hauteur (et donc leur taille) n’est par
contre pas bornée car, par exemple,

sn (0) := s(s(. . . s(0) . . .))

| {z }
n-fois

est un terme, pour tout n ≥ 1.

Exemple 2.7. Le signature de la théorie des groupes est { (e, 0), (inv, 1), (∗, 2) }, où ∗ est l’opéra-
teur de composition et inv est l’opérateur « inverse » qui est habituellement noté x−1 .

60 / 92
2.3 Expressions et formules 51

2.3.2 Le langage

Définition 2.8 (Langage). Un langage (ou vocabulaire) du premier ordre est la donnée d’un
couple de signatures S = (Sf , Sr ) disjointes (i.e. avec Sf ∩ Sr = ∅).
On dit que :
— Les elements de Sf sont les symboles de fonction du langage.
— Les elements de Sr sont les symboles de relation (ou de prédicat) du langage.

Remarque 2.9.
1. Rappelons qu’une constante est un symbole (de fonction) d’arité 0.
2. On considérera (sauf mention contraire) que chaque langage contient le symbole de relation
binaire = et un symbole de relation d’arité 0, ⊥ qui représentera le faux. Un langage contenant
le symbole binaire = sera appelé langage égalitaire.
3. Le rôle des relations et des fonctions est très différent. Les fonctions et constantes seront
utilisés pour construire les termes (i.e., les objets du langage) tandis que les relations serviront
à construire des formules (i.e., des propriétés sur ces objets)
Par exemple 1 + 2 est un terme, il désigne un objet, tandis que 1 + 2 = 3 désigne une formule
logique.

Exemple 2.10.
1. Le langage L1 de la théorie des groupes contient les symboles
— de constante : e ;
— de fonction : ∗ (binaire) et inv (unaire) ;
— de relation : = (binaire).
2. Le langage L2 de la théorie des ensembles contient les symboles
— de constante : ∅ ;
— de fonction : ∩ et ∪ binaires, C unaire (le complément) ;
— de relation : =, ∈ et ⊂, tous binaires. 2

2.3.3 Les formules du calcul des prédicats

Etant donné un langage S = (Sf , Sr ), on construit les formules de la logique du premier ordre
en utilisant les connecteurs de la logique propositionnelle et deux quantificateurs : ∀ et ∃.
Les formules sont construites à partir des formules atomiques, qui sont elles mêmes construites
à partir des termes. Une formule atomique est obtenue en appliquant un symbole de relation à des
termes.
On se fixe pour toute la suite un ensemble X = {x, x0 , x1 , . . . , y, y0 , y1 , . . . , z, z0 , z1 , . . .} de
variables.

Définition 2.11 (Formules atomiques). Soit S = (Sf , Sr ) un langage, une formule atomique sur
S est une expression de la forme suivante :
— r(t1 , . . . , tn ) où r ∈ Sr est d’arité n ≥ 0 et t1 , t2 , . . . , tn ∈ TSf (X) sont des termes.
Définition 2.12 (Formules). Etant donné un langage S, l’ensemble Fpo (S) des formules du
premier ordre sur S est le plus petit ensemble tel que :
1. toute formule atomique sur S appartient à Fpo (S),
2. si ϕ, ψ ∈ Fpo (S) sont deux formules alors :
— ϕ ∧ ψ ∈ Fpo (S),
— ϕ ∨ ψ ∈ Fpo (S),
— ϕ ⇒ ψ ∈ Fpo (S),
— ¬ϕ ∈ Fpo (S),

2. En fait, en théorie des ensembles, seulement les symboles = et ∈ sont considérés élémentaires. Les autres se
définissent à partir de ces deux.

61 / 92
52 Chapitre 2. Calcul des prédicats

3. si ϕ ∈ Fpo et x ∈ X alors
— ∀xϕ ∈ Fpo (S),
— ∃xϕ ∈ Fpo (S).

Exemple 2.13. Reprenons les langages de l’exemple 2.10 :

1. Dans L1 , x ∗ y = e, y ∗ x = e, x = e, y = e et y ∗ x = e sont des formules atomiques. Par
conséquent, ∀x∃y((x ∗ y = e) ∧ (¬(y ∗ x = e))) et ∀x((x = e) ∨ ∃y((¬(y = e)) ∧ (y + x = e)))
sont des formules.
2. Dans L2 , ∀x∀y(x ∩ y = ∅ ⇒ (x = ∅ ∧ y = ∅)) est une formule.
Remarquez que, comme pour les termes, les formules peuvent être vues comme des arbres dont
les feuilles sont des formules atomiques et les noeuds sont les connecteurs et quantificateurs. Par
exemple, la formule

[(∃xP (x)) ⇒ (R(f (y, x), g(x)) ∨ [∃xQ(g(x))])] ∧ [(∃yS(x, g(y))) ∨ P (h(y))] (2.1)

sera représentée de façon unique par l’arbre suivant :

⇒ ∨

∃x ∨ ∃y P (h(y))

P (x) R(f (y, x), g(x)) ∃x S(x, g(y))

Q(g(x))

2.3.4 Occurrences libres et liées d’une variable

Lorsqu’une variable x appartient à une sous-formule précédée d’un quantificateur, ∀x ou ∃x ,
elle est dite liée par ce quantificateur. Si une variable n’est liée par aucun quantificateur, elle est
libre.
La distinction entre variable libre et variable liée est importante. Une variable liée ne possède
pas d’identité propre et peut être remplacée par n’importe quel autre nom de variable qui n’apparaît
pas dans la formule. Ainsi, ∃x(x < y) est identique à ∃z(z < y) mais pas à ∃x(x < z) et encore
moins à ∃y(y < y).
L’ensemble des variables libres FV(ϕ) (depuis l’anglais, free variable), et l’ensemble des va-
riables liées BV(ϕ) (depuis l’anglais, bound variable) 3 d’une formule ϕ sont définis par induction
sur la structure de ϕ :
— si ϕ est une formule atomique, alors tout occurrence d’une variable x dans ϕ est libre :
FV(ϕ) = V ar(ϕ) et BV(ϕ) = ∅.
— si ϕ est ∃xψ ou ∀xψ, alors FV(ϕ) = FV(ψ)−{x} ; BV(ϕ) = BV(ϕ)∪{x} (et toute occurrence
de x libre dans ψ devient liée dans ϕ par le quantificateur introduit) ;
— si ϕ = ϕ1 ◦ ϕ2 (où ◦ ∈ { ∧, ∨, ⇒ }) alors FV(ϕ) = FV(ϕ1 ) ∪ FV(ϕ2 ), BV(ϕ) = BV(ϕ1 ) ∪
BV(ϕ2 ) ;
— si ϕ = ¬ψ, alors FV(ϕ) = FV(ψ) et BV(ϕ) = BV(ψ).
Définition 2.14 (Formule close). Une formule ϕ est dite close ssi FV(ϕ) = ∅.

Exemple 2.15. Une variable liée est attachée à une et une seule occurence d’un quantificateur
dans la formule : celui qui dans l’arbre est son ancêtre le plus proche. Par exemple, considérons la
formule ∃xP (x) ∧ ∀xQ(x). Les variables sont liées de la façon suivante :

62 / 92
2.4 Sémantique 53

6 ∃x

P (x) ∀xZ

Q(x)

Exemple 2.16. Considérons la formule (2.1) et son arbre :

⇒ ∨

∃x ∨ ∃y P (h(y))

P (x) R(f (y, x), g(x)) ∃x S(x, g(y))

Q(g(x))

Une variable est liée si elle a une occurrence dans une feuille qui est descendant d’un noeud
étiqueté par un quantificateur avec cette variable. Depuis l’exemple precedent, nous observons
qu’il peut bien etre le cas que FV(ϕ) ∩ BV(ϕ) 6= ∅. Nous verrons par la suite que les variables liées
peuvent être renommée sans modifier la sémantique d’une formule, ceci par exemple pour éviter
les ambiguités. Ainsi, nous pourrons toujours supposer que FV(ϕ) ∩ BV(ϕ) = ∅. Par exemple, la
formule précédente peut-être renommée de la façon suivante :
∧

⇒ ∨

∃x1 ∨ ∃x3 P (h(y))

P (x1 ) R(f (y, x), g(x)) ∃x2 S(x, g(x3 ))

Q(g(x2 ))

La nouvelle formule est donc

( [ ∃x1 P (x1 ) ] ⇒ [ (∃x2 Q(g(x2 ))) ∨ R(f (y, x), g(x)) ] ) ∧ [ (∃x3 S(x, g(x3 ))) ∨ P (h(y)) ] .

2.4 Sémantique
Jusqu’ici nous nous sommes contentés de définir la syntaxe des langages. Les formules n’ont
encore aucune signification, en partie car nous n’avons pas donné de signification aux symboles des
langages. Une signature ne donne qu’un ensemble de symboles, sans en donner d’interprétation.

63 / 92
54 Chapitre 2. Calcul des prédicats

2.4.1 Structures
Pour donner une sémantique aux formules, il faut donc commencer par donner une signification
aux éléments de la signature du langage. On fait cela en associant une structure au langage.

Définition 2.17. Soit S = (Sr , Sf ) un langage. Une S-structure (ou S-interprétation) M

est la donnée d’un ensemble DM et
ρ(R)
(a) d’une relation RM ⊆ DM , pour chaque symbole de relation R ∈ Sr ;
ρ(f )
(b) d’une fonction totale (application) f M : DM → DM , pour chaque symbole de fonction
f ∈ Sf .

Remarque 2.18. A cause de la remarque 2.3, la clause (b) dans la définition d’une S-structure
peut se rephraser comme suit :
(b.1) d’un élément cM de DM , pour chaque symbole de constante (symbole de fonction d’arité
0) c ∈ Sf ,
ρ(f )
(b.2) d’une fonction totale (application) f M : DM → DM , pour chaque symbole de fonction
f ∈ Sf , tel que ρ(f ) ≥ 1.
Exemple 2.19. Supposons que le langage soit composé de la constante o et de la fonction unaire
s. On peut choisir, par exemple, les structures suivantes :
1. DM est l’ensemble des entiers naturels, oM est le nombre 0 et sM est la fonction donnant le
successeur, c’est-à-dire sM (n) = n + 1 ;
2. DM est un ensemble de personnes, oM c’est Paul et sM est la fonction donnant le père d’une
personne.
Exemple 2.20. Supposons que Sf = { (o, 0), (s, 1) } et Sr = { (Even, 1) }. Comme auparavant,
on peut choisir DM est l’ensemble des entiers naturels, oM est le nombre 0 et sM est la fonction
donnant le successeur. Pour compléter la définition de S-structure nous pouvons poser

EvenM := { n ∈ N | n mod 2 = 1 } .

Bien que la S-structure ainsi définie puisse apparaître bien drôle (ou inappropriée), la définition
de cette structure n’est pas incorrecte : rien nous oblige à donner à un symbole une interprétation
par défaut.
La situation est assez différente quand le symbole d’égalité est parmi les symboles de relation.
Dans ce cas, on interprétera, par défaut, la relation d’égalité sur l’image de la fonction diagonale :

=M := { (d, d) | d ∈ DM } .

Exemple 2.21. Supposons que le langage est composé du symbole de relation B d’arité 2.
On peut choisir par exemple les interprétations suivantes :
1. DM , le domaine, est l’ensemble des sommets du graphe
a b

d c
et B est interprété comme la relation "flèche" : B M = {(a, b), (b, c), (c, d), (d, a)}
2. DM , le domaine, est le même qu’aupravant, mais maintenant B est interprété comme la
relation "ne pas être voisin direct" : B M = {(b, d), (d, b), (a, c), (c, a)}. Cette structure est
différente de la précédente, même si elles partagent le même domaine.
3. Le domaine est l’ensemble des triangles et B est la relation "avoir la même aire"
Exemple 2.22. Supposons que ρ(R) ≤ 2 pour tout R ∈ Sr , et que ρ(f ) ≤ 1 pour tout f ∈ Sf . On
peut représenter une S-structure M comme un (sorte de) graphe orienté étiqueté :
— les noeuds du graphe sont les éléments du domaine DM ;
— un noeud d ∈ DM est étiqueté par P ∈ Sr si d ∈ P M ;

64 / 92
2.4 Sémantique 55

— un noeud d ∈ DM est étiqueté par un symbole de constante c ∈ Sf si d = cM ;

— on met une arête de d vers d0 si (d, d0 ) ∈ RM , pour un quelque symbole de relation R ∈ Sr ;
une arête d → d0 est étiqueté par les symboles R ∈ Sr tels quel (d, d0 ) ∈ R ;
— on met une arête pointillée de d vers d0 si f (d) = d0 ; une arête pointillée d → d0 est étiqueté
par les symboles f ∈ Sf tels quel f (d) = d0 ;
Par exemple, si Sr = { (P, 2) } et Sf = { (f, 1) }, alors la structure M = hDM , P M , f M i avec
— DM = {a, b, c},
— P M = {(a, b), (b, c), (c, a)},
— f M : a 7→ a, b 7→ b, c 7→ a ;
peut se représenter comme le graphe étiqueté de la figure 2.1.
Exemple 2.23. Voici quelques exemples de structures importantes :

Domaine Fonctions Relations Nom

N 0, s, + =, ≤ Arithmétique de Presburger
N 0, s, +, × =, ≤ Arithmétique de Peano
R 0, s, +, × =, ≤ Théorie des rééls
{0} ∅ {p0 , . . . , pn , . . .} Structure propositionnelle
TSf (∅) Sˆf Sˆr Modèle de Herbrand

Dans le cas des modèle de Herbrand, le domaine est l’ensemble des termes définis sur un
ensemble de variables vide. Une fonction fˆ ∈ Sˆf d’arité n associe aux termes t1 , . . . , tn le nouveau
terme f (t1 , . . . , tn ), et les relations sont quelconques.

2.4.2 Evaluation (des termes et) des formules

Comme pour le calcul des propositions, nous allons définir l’interprétation d’une formule en
fonction de l’interprétation des formules élémentaires (ici les formules atomiques). Pour qu’une
formule soit évaluable à vrai ou faux (1 ou 0), il faut non seulement dire comment s’interprètent les
prédicats et les symboles de fonctions, (ce qui est l’analogue d’interpréter les propositions pour le
calcul propositionnel) mais aussi ce que valent les variables : en effet les formules peuvent contenir
des variables libres, et on a besoin de connaître leur valeur pour que la formule soit évaluable. Bien
sûr la valeur des variables liées n’intervient en rien dans le calcul de la valeur d’une formule.
Par exemple pour connaître la valeur de P (x, y) il faut non seulement connaître la signification
de P (donnée par la structure), mais aussi la valeur de x et de y qui sera donnée par une valuation.
Dans la formule ∃xP (x, y) il faut connaître la valeur P et celle de y (mais celle de x n’a aucune
importance). Cependant, comme la valeur de ∃xP (x, y) va être définie en fonction de la valeur de
P (x, y), on fera aussi intervenir la valeur de x, ou plus précisément les valeurs de P (x, y) pour
toutes les valeurs de x.
Nous allons donc définir la valeur d’une formule ϕ d’un langage (S, X) en fonction d’une S-
structure M et d’une valuation des variables.

Définition 2.24. Une valuation de l’ensemble X des variables individuelles dans une structure
M est une fonction V de l’ensemble X vers le domaine de M, soit V : X → DM .
On définit maintenant la valeur J ϕ KM,V d’une formule ϕ en fonction d’une structure M et
d’une valuation V. On commence naturellement par donner la valeur des termes.
Définition 2.25. Soit M une S-structure et V une valuation de X dans DM ; la valeur d’un
terme t ∈ TSf (X), notée J t KM,V est un élément de DM défini (par induction) par :
— pour toute variable x ∈ X, J x KM,V = V(x) ;
— pour tout f ∈ Sf d’arité n ≥ 0, pour tous termes t1 , . . . tn ,

J f (t1 , . . . , tn ) KM,V := f M (J t1 KM,V , . . . , J tn KM,V ) .

Remarque 2.26. La définition de l’évaluation pour un terme construit via un symbole de fonc-
tion peut se séparer en deux cas, selon l’arité du symbole :

65 / 92
56 Chapitre 2. Calcul des prédicats

— pour toute constante c ∈ Sf (c’est-à-dire symbole de fonction d’arité 0), J c() KM,V =
J c KM,V := cM ;
— pour tout f ∈ Sf d’arité n ≥ 1, pour tous termes t1 , . . . tn , J f (t1 , . . . , tn ) KM,V :=
f M (J t1 KM,V , . . . , J tn KM,V ).
Si M et V sont fixées, toute formule atomique prend la valeur 0 ou 1, selon la définition
formelle suivante, qui suit l’intuition :
Définition 2.27. La valeur J ϕ KM,V d’une formule atomique ϕ est définie par :
— pour tout R ∈ Sr d’arité n, pour tous termes t1 , . . . , tn ,

J R(t1 , . . . , tn ) KM,V = 1 ssi (J t1 KM,V , . . . , J tn KM,V ) ∈ RM .

Pour évaluer une formule contenant des quantificateurs, il nous faudra la notion de variante
d’une valuation.

Notation 2.28. Nous allons noter V[x := a] la valuation V 0 telle que V 0 (x) = a et V(y)0 = V(y)
pour tout y ∈ X \ { x }. Autrement, pour tout y ∈ X :
(
a, si y = x ,
V[x := a](y) =
V(y) , sinon.

On dira alors que V[x := a] est une variante en x de V.

Enfin, la valeur d’une formule est définie par induction sur la structure de la formule :
Définition 2.29 (Valeur d’une formule). Etant donné un langage S et une formule ϕ de Fpo (S),
la valeur de ϕ pour la S-structure M et la valuation V est notée J ϕ KM,V et est définie de la
façon suivante :
— J ϕ ∧ ψ KM,V = 1 ssi J ϕ KM,V = 1 et J ψ KM,V = 1 ;
— J ϕ ∨ ψ KM,V = 1 ssi J ϕ KM,V = 1 ou J ψ KM,V = 1 ;
— J ¬ϕ KM,V = 1 ssi J ϕ KM,V = 0 ;
— J ϕ ⇒ ψ KM,V = 0 ssi J ϕ KM,V = 1 et J ψ KM,V = 0 ;
— J ∀xϕ KM,V = 1 si et seulement si pour tout a ∈ DM , J ϕ KM,V[x:=a] = 1 ;
— J ∃xϕ KM,V = 1 si et seulement s’il existe a ∈ DM tel que J ϕ KM,V[x:=a] = 1.

Remarque 2.30. Le quantificateur universel peut se considérer comme une sorte de grande
conjonction. En fait, on a

J ∀x.ϕ KM,V = min{ J ϕ KM,V[x:=a] | a ∈ DM } .

De façon similaire, le quantificateur existentiel est une sorte disjonction :

J ∃x.ϕ KM,V = max{ J ϕ KM,V[x:=a] | a ∈ DM } .

Par ailleurs, il devient possible remplacer un quantificateur universel par une conjonction (de façon
à simuler la logique du premier ordre par la logique propositionnelle) seulement si le domaine DM
est fini, et en plus il est fixé. Que dire si DM est N (ici, le domaine est infini) ou si on se pose
la question si ∀x(x = x) est vraie dans n’importe quelle structure (ici, on ne peut pas fixer le
domaine) ?
On notera souvent M, V |= ϕ à la place de J ϕ KM,V = 1.

Remarque 2.31. La valeur de J ∀xϕ KM,V ou J ∃xϕ KM,V ne dépend pas de V(x). Par suite, la
valeur de J ϕ KM,V , où ϕ est une formule quelconque ne dépend pas de V(x) lorsque x n’est pas
une variable libre. En particulier, si ϕ est une formule close (sans variables libres), alors J ϕ KM,V
ne dépend pas de V et par conséquent on écrira J ϕ KM à la place de J ϕ KM,V et M |= ϕ à la place

66 / 92
2.4 Sémantique 57

f
a f
P P

b c
P
f

Figure 2.1 – Structure en forme de graphe étiqueté

de M, V |= ϕ.
L’ordre d’apparition des quantificateurs dans une formule est important. Il détermine le sens
de la formule.
Par exemple, si nous donnons au prédicat p(x, y) la signification "x aime y", alors, nous obtenons
des significations différentes pour la formule Q1 xQ2 yp(x, y) (où Q1 et Q2 sont des quantificateurs).
— ∀x∀yp(x, y) tout le monde aime tout le monde
— ∃x∀yp(x, y) il existe des personnes qui aiment tout le monde
— ∃y∀xp(x, y) il existe des personnes aimées de tous
— ∀x∃yp(x, y) toute personne aime quelqu’un
— ∀y∃xp(x, y) toute personne est aimée par quelqu’un
— ∃x∃yp(x, y) il y a une personne qui aime quelqu’un.
On peut remarquer que les seuls cas où on peut échanger l’ordre des quantificateurs sans
modifier le sens de la formule sont ceux où les quantificateurs sont identiques : ∃x∃yϕ ≡ ∃y∃xϕ et
∀x∀yϕ ≡ ∀y∀xϕ. C’est pourquoi en mathématique on écrit souvent ∃xyϕ ou ∀xyϕ.

Exemple 2.32. Considérons la formule

ϕ := ∀x∃y( P (x, f (y)) ∨ P (y, f (x)) ) ,

à évaluer dans M = hDM , P M , f M i où :

— DM = {a, b, c},
— P M = {(a, b), (b, c), (c, a)},
— f M : a 7→ a, b 7→ b, c 7→ a.
Cette structure, étant sur un langage relationnel d’arité au plus 2 et sur un langage fonctionnel
d’arité au plus 1, est représentée en forme de graphe étiqueté en figure 2.1.
Pour calculer J ϕ KM,V on peut d’abord considérer toutes les valuations possibles de x et de y,
soit 9 valuations. Pour chaque valuation, nous pouvons évaluer la formule P (x, f (y)) ∨ P (y, f (x)),
en évaluant d’abord les termes x, f (x), y, f (y), pour ensuite évaluer la disjonction selon les règles
usuelles de la logique propositionnelle. Nous avons donc :
Vaa : x = a, y = a :

J P (x, f (y)) ∨ P (y, f (x)) KM,Vaa = max(J P (x, f (y)) KM,Vaa , J P (y, f (x)) KM,Vaa ) = 0

car J f (y) KM,Vaa = J f (x) KM,Vaa = a et donc

J P (x, f (y)) KM,Vaa = J P (y, f (x)) KM,Vaa = 0 , car (a, a) 6∈ P M .

Dans la suite, nous allons abréger l’exposition, tous ces calculs seront sous-entendus. Avec un
abus de notation, nous allons simplement écrire :

J P (x, f (y)) ∨ P (y, f (x)) KM,Vaa = J P (a, a) ∨ P (a, a) KM = 0 .

Vab : x = a, y = b :

J P (x, f (y)) ∨ P (y, f (x)) KM,Vab = J P (a, b) ∨ P (b, a) KM = 1;

67 / 92
58 Chapitre 2. Calcul des prédicats

Vac : x = a, y = c :

J (P (x, f (y)) ∨ P (y, f (x))) KM,Vac = J P (a, a) ∨ P (c, a) KM = 1;

Vba : x = b, y = a :

J P (x, f (y)) ∨ P (y, f (x)) KM,Vba = J P (b, a) ∨ P (a, b) KM = 1 ;

Vbb : x = b, y = b :

J P (x, f (y)) ∨ P (y, f (x)) KM,Vbb = J P (b, b) ∨ P (b, b) KM = 0 ;

Vbc : x = b, y = c :

J P (x, f (y)) ∨ P (y, f (x)) KM,Vbc = J P (b, a) ∨ P (c, b) KM = 0 ;

Vca : x = c, y = a :

J P (x, f (y)) ∨ P (y, f (x)) KM,Vca = J P (c, a) ∨ P (a, a) KM = 1 ;

Vcb : x = c, y = b :

J P (x, f (y)) ∨ P (y, f (x)) KM,Vcb = J P (c, b) ∨ P (b, a) KM = 0 ;

Vcc : x = c, y = c :

J P (x, f (y)) ∨ P (y, f (x)) KM,Vcc = J P (c, a) ∨ P (c, a) KM = 1 .

Commençons par étudier les valeurs possibles de la sous-formule ∃y(P (x, f (y)) ∨ P (y, f (x))) :
Va : x := a :

J ∃y(P (x, f (y)) ∨ P (y, f (x))) KM,Va = 1 , car J P (x, f (y)) ∨ P (y, f (x)) KM,Vab = 1.

Donc pour toute valuation V telle que V(x) = a, J ∃y(P (x, f (y)) ∨ P (y, f (x))) KM,V = 1.
Vb : x := b :

J ∃y(P (x, f (y)) ∨ P (y, f (x))) KM,Vb = 1 , car J P (x, f (y)) ∨ P (y, f (x)) KM,Vba = 1.

Donc pour toute valuation V telle que V(x) = b, J ∃y(P (x, f (y)) ∨ P (y, f (x))) KM,V = 1.
Vc : x := c :

J ∃y(P (x, f (y)) ∨ P (y, f (x))) KM,Vc = 1 , car J P (x, f (y)) ∨ P (y, f (x)) KM,Vca = 1.

Donc pour toute valuation V telle que V(x) = c, J ∃y(P (x, f (y)) ∨ P (y, f (x))) KM,V = 1.

Donc pour toute valuation V, nous avons M, V |= ∃y(P (x, f (y)) ∨ P (y, f (x))), i.e.,

M |= ∀x∃y(P (x, f (y)) ∨ P (y, f (x))) .

Remarque 2.33. Observons que la notation P (a, a) et les notations similaires sont impropres,
mais très utiles en pratique, et aussi très utilisés par les logiciens ! ! ! En fait, P (a, a) n’est pas
une formule (atomique) du premier ordre, car ici a n’est pas un terme, mais plutôt un élément
du domaine DM . Pour pouvoir justifier cette notation il faut ajouter au langage un symbole de
constante ca , pour tout élément du domaine a ∈ DM ; il faut de plus étendre l’interprétation en
posant cM
a = a.

68 / 92
2.4 Sémantique 59

Vocabulaire

Définition 2.34 (Modèle). Soit ϕ ∈ Fpo (S) une formule close (i.e., qui ne contient pas de
variable libre) et M une S-structure. La structure M est un modèle de ϕ si M |= ϕ.
Soit Γ ⊆ Fpo (S) un ensemble de formules closes (i.e., qui ne contient pas de variable libre)
et M une S-structure. La structure M est un modèle de Γ si M |= ϕ pour tout ϕ ∈ Γ.
Définition 2.35 (Tautologie). Une formule close ϕ ∈ Fpo (S) est une tautologie si M |= ϕ pour
toute S-structure M.
Définition 2.36 (Formule insatisfaisable). Une formule close ϕ ∈ Fpo (S) est insatisfaisable si
elle n’a pas de modèle.
Définition 2.37 (Conséquence logique). Une formule close ϕ est conséquence logique d’un
ensemble de formules closes Γ si tout modèle de Γ est un modèle de ϕ. On écrit alors Γ |= ϕ.
Définition 2.38 (Théorie). Une théorie est l’ensemble des conséquences logiques d’un ensemble
de formules closes.
Par exemple, la théorie des groupes est l’ensemble des formules logiques qui sont vraies dans
tous les groupes.
Définition 2.39 (Equivalence). Deux formules ϕ et ψ de Fpo (S) sont équivalentes (noté ϕ ≡ ψ)
si pour toute S-structure M et toute valuation V : X → DM , on M, V |= ϕ ssi M, V |= ψ.

Attention : on peut parler d’équivalence entre deux formules même quand celles-ci ne sont pas
de formules closes.
On peut par ailleurs noter que ϕ et ψ sont équivalentes lorsque M, V |= ϕ ⇔ ψ pour tout M
et V, de façon qu’elles sont équivalentes ssi ∀(ϕ ⇔ ψ) est une tautologie. Ici, ∀(ϕ) est la clôture
universelle de la formule ϕ, obtenue de ϕ en lui ajoutant une suite de quantificateurs universels
∀x1 ∀x2 . . . ∀xn , où x1 , . . . , xn est la liste des variables libres de ϕ.

69 / 92
60 Chapitre 2. Calcul des prédicats

2.5 Manipulation de formules

2.5.1 Substitution de variables

Dans la suite, nous allons préciser ce que veut dire qu’une formule ψ ∈ Fpo (S) est obtenue
d’une formule ϕ ∈ Fpo (S) en substituant toute occurrence d’une variable libre x par un terme (ce
qui sera noté par ψ = ϕ{x→t} ).

Remarque 2.40. Bien que la notion soit intuitive, il ne faut pas que des variables libres deviennent
liées par cette substitution. Considérons ce qu’il se passe si l’on substitue de façon naïve x par le
terme y dans ∃yR(x, y). La formule ∃yR(y, y) n’est pas le résultat souhaité. On souhaite plutôt
avoir comme résultat la formule suivante : ∃zR(y, z). On devine donc la nécessite de renommer les
variables de sorte qu’une substitution ne crée pas des nouvelle variables liées.

Si σ est la substitution {x1 → t1 , . . . , xn → tn }, on note ϕσ la formule ϕ dans laquelle toutes

les occurrences libres de x1 , . . . , xn ont été remplacées respectivement par t1 , . . . , tn . Pour définir
formellement la notion de substitution dans une formule, on commence par la définir pour les
termes. Soit t un terme de TS (X) et σ une substitution :
— si t = x et x ∈ Dom(σ) alors tσ = σ(x), (et tσ = x si x 6∈ Dom(σ)) ;
— si t = c alors tσ = c ;
— si t = f (t1 , . . . , tn ) alors tσ = f (t1σ , . . . , tnσ ).
On définit maintenant la substitution par récurrence sur la structure de la formule :

R(t1 , . . . , tn )σ := R(t1σ , . . . , tnσ ) ,

(ϕ ◦ ψ)σ := (ϕσ ) ◦ (ψσ ), pour tout connecteur binaire ◦ ,
(
Qx.(ϕσ[x→x] ) , si x ∈
/ Im(σ)
(Qx.ϕ)σ :=
Qy.(ϕ{x→y} )σ , si x ∈ Im(σ), où y ∈ / V ar(ϕ) ∪ Dom(σ) ∪ Im(σ) ,

où Q ∈ { ∃, ∀ }, et σ[x → x] est la substitution σ 0 telle que σ 0 (x) = x, et σ 0 (y) = σ(y) pour y 6= x.

Proposition 2.41. Si y ∈
/ V ar(ϕ), alors ∃xϕ ≡ ∃y(ϕ{x→y} ).
Grâce à cette proposition, on pourra supposer désormais, sans perte de généralité, que les
différentes occurrences liées d’une variables sont toutes liées au même quantificateur et qu’aucune
variable n’admet à la fois des occurrences libres et des occurrences liées.

2.5.2 Equivalences classiques

Les équivalences données dans le cadre du calcul propositionnel restent vraies. Nous en donnons
d’autres ici, les preuves sont laissées en exercice.

— Lois de conversion des quantificateurs :

¬∀xϕ ≡ ∃x¬ϕ , ¬∃xϕ ≡ ∀x¬ϕ .

— Lois de distribution des quantificateurs :

∀x(ϕ ∧ ψ) ≡ (∀xϕ ∧ ∀xψ) , ∃x(ϕ ∨ ψ) ≡ (∃xϕ ∨ ∃xψ) .

— Lois de permutation des quantificateurs de même sorte :

∀x∀yϕ ≡ ∀y∀xϕ , ∃x∃yϕ ≡ ∃y∃xϕ .

70 / 92
2.5 Manipulation de formules 61

— Lois de passage : si x ne figure pas à titre d’occurence libre dans ψ, on a les lois suivantes :

∀x(ϕ ∧ ψ) ≡ (∀xϕ) ∧ ψ ∃x(ϕ ∧ ψ) ≡ (∃xϕ) ∧ ψ

∀x(ϕ ∨ ψ) ≡ (∀xϕ) ∨ ψ ∃x(ϕ ∨ ψ) ≡ (∃xϕ) ∨ ψ
∀x(ϕ ⇒ ψ) ≡ (∃xϕ) ⇒ ψ ∃x(ϕ ⇒ ψ) ≡ (∀xϕ) ⇒ ψ
∀x(ψ ⇒ ϕ) ≡ ψ ⇒ (∀xϕ) ∃x(ψ ⇒ ϕ) ≡ ψ ⇒ (∃xϕ)

Remarquez le changement de quantificateur dans les équivalences ∀x(ϕ ⇒ ψ) ≡ (∃xϕ) ⇒ ψ

et ∃x(ϕ ⇒ ψ) ≡ (∀xϕ) ⇒ ψ.
La règle qui établit l’équivalence entre ∃x(ϕ ∧ ψ) et (∃xϕ) ∧ ψ (lorsque x n’est pas une
variable libre de ψ) est aussi connue sous le nom de loi de Frobenius.
— Lois de réalphabétisation (renommage) des variables.
On peut toujours renommer une variable liée et la variable du quantificateur au sein d’une
formule. Cependant, le nouveau nom ne doit pas être un nom déjà utilisé pour une variable
libre ou liée de la formule.
Par exemple, dans ∃x(∀xF (x, y) ⇒ (G(x)∨q)), on peut opérer deux renommages : on peut
renommer d’abord l’occurrence de x dans F (x, y) à t, en obtenant ainsi ∃x(∀tF (t, y) ⇒
(G(x) ∨ q)), et ensuite renommer le x restant à z ; on obtient ∃z(∀tF (t, y) ⇒ (G(z) ∨ q)).
Soit { x → t } la substitution qui remplace la variable x par la variable t. La loi de
réalphabétisation peut se déduire de la regle élémentaire de réalphabétisation suivante :

Qxϕ ≡ Qt(ϕ{ x→t } ) où Q ∈ { ∀, ∃ }

pourvu que t n’est pas une variable libre de ϕ (en particulier, quand t n’a aucune occurrence
dans t) et toutes les occurrences de x sont libres dans ϕ.

Exemple 2.42. Nous pouvons démontrer l’équivalence entre les formules ¬∀xϕ(x) et ∃x¬ϕ(x) de
la façon suivante. Soient M une S-structure et V une valuation fixés.
(a) Supposons que J ∃x¬ϕ KM,V = 1 et montrons que J ¬∀xϕ KM,V = 1. De maxa∈DM J ¬ϕ KM,V[x:=a] =
1, nous déduisons que J ¬ϕ KM,V[x:=a] = 1 pour un quelque a ∈ DM , donc J ϕ KM,V[x:=a] = 0
et J ∀xϕ KM,V = mina∈DM J ϕ KM,V[x:=a] = 0, donc J ¬∀xϕ KM,V = 1.
(b) Supposons, par contre, que J ¬∀xϕ KM,V = 1 et montrons que J ∃x¬ϕ KM,V = 1. On a bien que
J ∀xϕ KM,V = 0 ; depuis

0 = J ∀xϕ KM,V = min J ϕ KM,V[x:=a] = 0

a∈DM

nous déduisons que ce minimum est réalisé : donc J ϕ KM,V[x:=a] = 0 pour un quelque a ∈ DM ,
d’où J ¬ϕ KM,V[x:=a] = 1, et J ∃x¬ϕ KM,V = 1.

Les argumentaires ci-dessus sont acceptés dans un cadre classique. L’argumentaire (b) se révèle
par contre insatisfaisante, si depuis une preuve d’existence d’un objet avec une certaine propriété,
nous souhaitons être capable de construire l’objet. Supposons, par exemple, que nous avons réussi à
montrer que « non pour tout n, si n est premier, alors n = 2k −1 pour un nombre k ». L’argumentaire
(b) prétend qu’il est possible déduire de l’existence d’un nombre n qui n’est pas de la forme 2k − 1,
mais ne spécifie d’aucune façon comment le construire. Pour cette raison, en logique intuitionniste
(du premier ordre), qui se construit autour de l’idée qu’une preuve logique d’existence doit donner
aussi un moyen de construire un objet témoignant de son existence, la formule ∃x¬ϕ ⇒ ¬∀xϕ est
considérée comme une tautologie, mais la formule ¬∀xϕ ⇒ ∃x¬ϕ ne l’est pas. Voir par exemple
[Miq05].

Exercice 2.43. Montrez que les formules ∀x(ϕ ∨ ψ) et ∀xϕ ∨ ∀xψ ne sont pas, en général,
équivalentes. Argumentez de façon similaire pour ∃x(ϕ ∧ ψ) et ∃xϕ ∧ ∃xψ.

71 / 92
62 Chapitre 2. Calcul des prédicats

2.5.3 Formes Normales

Établir la consistance d’une formule du calcul des prédicats est un problème difficile. On peut
alors essayer de travailler sur une version de forme plus simple mais de consistance équivalente à la
formule initiale. Nous introduisons dans cette section la forme clausale pour la logique des prédicats.
Toute formule de la logique des prédicats du premier ordre admet une représentation sous forme
de clause qui préserve sa satisfiabilité. À la différence des formes normales, une clause n’est pas
logiquement équivalente à la formule dont elle dérive. Nous décrivons, à présent, les différentes
étapes qui mènent à une représentation sous forme clausale.

[Link] Forme prénexe

Définition 2.44 (Forme prénexe). Une formule ϕ est sous forme prénexe lorsqu’elle a la forme :

Q1 x1 Q2 x2 . . . Qn xn ψ

où chaque Qi est un quantificateur (existentiel ou universel) et ψ est sans quantificateurs. La

partie Q1 x1 Q2 x2 . . . Qn xn est appelée le préfixe et ψ étant qualifiée de matrice.
Mettre une formule sous forme prénexe consiste donc à renvoyer tous les quantificateurs au
début de la formule.

Théorème 2.45 (Forme prénexe équivalente). Pour toute formule ϕ ∈ Fpo il existe une formule
équivalente ψ ∈ Fpo en forme prénexe.
L’algorithme de mise sous forme prénexe suit les étapes suivantes :
Etape 1 : Renommer les variables de façon à ce qu’aucune variable n’ait d’occurrence libre et
liée et d’occurrences liées à des quantificateurs différents ;
Etape 2 : Appliquer tant que possible les substitutions suivantes : substitution du membre droit
par le membre gauche pour toutes les lois de passage et de conversion des quantifica-
teurs.

Exemple 2.46. Considérez la formule suivante :

¬∃x∀yR(x, y) ∧ ∀x(∃yR(x, y) ⇒ R(x, x))
La première étape, renommage des variables, donne la formule suivante :
¬∃z0 ∀z1 R(z0 , z1 ) ∧ ∀z2 (∃z3 R(z2 , z3 ) ⇒ R(z2 , z3 )) .
Nous appliquons ensuite la deuxième étape :
¬∃z0 ∀z1 R(z0 , z1 ) ∧ ∀z2 (∃z3 R(z2 , z3 ) ⇒ R(z2 , z2 ))
∀z0 ¬∀z1 R(z0 , z1 ) ∧ ∀z2 (∃z3 R(z2 , z3 ) ⇒ R(z2 , z2 ))
∀z0 ∃z1 ¬R(z0 , z1 ) ∧ ∀z2 (∃z3 R(z2 , z3 ) ⇒ R(z2 , z2 ))
| {z } | {z }
ϕ ψ

∀z0 (∃z1 ¬R(z0 , z1 ) ∧ ∀z2 (∃z3 R(z2 , z3 ) ⇒ R(z2 , z2 )))

| {z } | {z }
ϕ ψ

∀z0 ∃z1 (¬R(z0 , z1 ) ∧∀z2 (∃z3 R(z2 , z3 ) ⇒ R(z2 , z2 )))

| {z } | {z }
ψ ϕ

∀z0 ∃z1 ∀z2 (¬R(z0 , z1 ) ∧ (∃z3 R(z2 , z3 ) ⇒ R(z2 , z2 )))

| {z } | {z }
ϕ ψ

∀z0 ∃z1 ∀z2 (¬R(z0 , z1 ) ∧∀z3 (R(z2 , z3 ) ⇒ R(z2 , z2 )))

| {z } | {z }
ψ ϕ

∀z0 ∃z1 ∀z2 ∀z3 (¬R(z0 , z1 ) ∧ (R(z2 , z3 ) ⇒ R(z2 , z2 ))) .

72 / 92
2.5 Manipulation de formules 63

La nécessite de renommer les variables peut se comprendre si on essaie d’appliquer les règles de
passage sans un renommage préalable. Ainsi :

¬∃x∀yR(x, y) ∧ ∀x(∃yR(x, y) ⇒ R(x, x))

∀x∃y¬R(x, y) ∧ ∀x(∃yR(x, y) ⇒ R(x, x))
∀x∃y(¬R(x, y) ∧∀x(∃yR(x, y) ⇒ R(x, x)))
| {z } | {z }
ψ ϕ

Ici on ne peut pas appliquer la loi de passage, donc on renomme :

∀x∃y(¬R(x, y) ∧∀t(∃yR(t, y) ⇒ R(t, t)))

| {z } | {z }
ψ ϕ

On peut ainsi appliquer la loi de passage :

∀x∃y∀t(¬R(x, y) ∧ (∃yR(t, y) ⇒ R(t, t))) . . .

[Link] Forme de Skolem

Définition 2.47. Une formule est sous forme de Skolem lorsqu’elle est sous forme prenexe et
qu’elle ne contient que des quantifications universelles.
Exemple 2.48. La formule ∀xR(x, f (x)) est sous forme de Skolem. La formule ∀x∃yR(x, y)
est en forme prénexe, mais elle n’est pas sous forme de Skolem, car on trouve un quantificateur
existentiel dans le préfixe.

Pour effectuer une skolémisation, on part donc d’une formule sous forme prenexe et on « sup-
prime » les quantificateurs existentiels, en appliquant de façon itérée la règle suivante.
Règle de Skolémisation. Elle est de la forme
∃yψ
ψ{y→f (z1 ,...,zm )}

où
— z1 , ..., zm sont les variables libres de la formule ∃y.ψ, et
— f un nouveau symbole de fonction (dit de Skolem) d’arité m.

Rappel (cf. Définition 2.14). Une formule est close si elle ne contient pas de variables libres.

Exemple 2.49. Considérons une formule close ϕ = ∃xψ écrite sur un langage S. La règle de
skolémisation donne la formule ψ{x→c} , où c est un nouveau symbole de constante.
Une S-structure M est un modèle de ϕ ssi il existe a ∈ DM tel que J ψ KM,V où V est telle que
V(x) = a. Considérons maintenant le langage S 0 := S ∪ { (c, 0) } (où c est le nouveau symbole de
0
constante) et la S 0 -structure M0 obtenue depuis M en interprétant la constante c par cM := a.
Clairement, M0 est un modèle de la formule ψ{x→c} .
Nous avons donc argumenté que si ϕ a un modèle, alors ψ{x→c} a un modèle ; l’implication
inverse est d’ailleurs aussi vraie. Donc ϕ est satisfaisable ssi ψ{x→c} est satisfaisable.

Exemple 2.50. Considérons maintenant la formule ϕ = ∀y∃xψ écrite sur un langage S. Une S-
structure M est un modèle de ϕ ssi pour chaque b ∈ DM il existe a ∈ DM tel que J ψ KM,[y:=b,x:=a]
ssi il existe une fonction f : DM → DM telle que, pour tout b ∈ DM , J ψ KM,[y:=b,x:=f (b)] .
Donc ϕ admet un modèle ssi ∀yψ{x→f (y)} a un modèle. Remarquez que la formule ∀yψ{x→f (y)}
est construite à partir du langage S ∪ { (f, 1) }.
C’est ce principe qui va être généralisé pour mettre une formule sous forme de Skolem.

73 / 92
64 Chapitre 2. Calcul des prédicats

Définition 2.51. Une formule universelle (c’est-à-dire une formule close contenant seulement
des quantificateurs universels), obtenue par
— mise en forme prenexe, et ensuite
— application itérée de la règle de skolémisation
est appelée forme de skolem ou skolémisée de ϕ.

Exemple 2.52.
1. Soit ϕ = ∀x∃yP (x, y) ⇒ ∀x∃yP (y, x).
La mise sous forme prénexe donne la formule équivalente ϕ0 = ∃x∀y∀x0 ∃y 0 (P (x, y) ⇒ P (y 0 , x0 )).
La skolémisation donne :
∃x∀y∀x0 ∃y 0 (P (x, y) ⇒ P (y 0 , x0 ))
∀y∀x0 ∃y 0 (P (c, y) ⇒ P (y 0 , x0 ))
∀x∀x0 (P (c, y) ⇒ P (f (y, x0 ), x0 ))
2. Considérons la formule ∃x1 ∀x2 ∀x3 ∃x4 ∀x5 ∃x6 P (x1 , x2 , x3 , x4 , x5 , x6 ). On obtient sa formule
de Skolem de la façon suivante :

∃x1 ∀x2 ∀x3 ∃x4 ∀x5 ∃x6 P (x1 , x2 , x3 , x4 , x5 , x6 )

∀x2 ∀x3 ∃x4 ∀x5 ∃x6 P (f1 , x2 , x3 , x4 , x5 , x6 )
∀x2 ∀x3 ∀x5 ∃x6 P (f1 , x2 , x3 , f4 (x2 , x3 ), x5 , x6 )
∀x2 ∀x3 ∀x5 P (f1 , x2 , x3 , f4 (x2 , x3 ), x5 , f6 (x2 , x3 , x5 ))
Dans la formule précédente, ∃x1 n’est précédé par aucun quantificateur universel. C’est pour-
quoi on introduit une nouvelle constante f1 .

Remarque 2.53. La version skolémisée d’une formule ne lui est pas, en général, équivalente. Le
langage étant étendu, donc différent, les modèles des deux formules sont des structures pour des
langages différents. Néanmoins :
— tout modèle de la formule skolémisée est modèle de la formule initiale ;
— tout modèle de la formule initiale peut s’étendre en un modèle de la formule skolémisée,
obtenu en conservant les interprétations des symboles de la signature initiale, et en inter-
prétant correctement les nouveaux symboles de fonction introduits pas la skolemisation ;
— une formule close et sa forme de Skolem sont dites équisatisfaisables : si l’une possède un
modèle, l’autre également et réciproquement.

Proposition 2.54. Si ϕs est obtenue par skolémisation à partir de ϕ alors ϕs est satisfaisable
si et seulement si ϕ est satisfaisable.

[Link] Forme clausale

Définition 2.55 (Forme clausale). Une formule close est sous forme clausale si elle est
1. en forme prenexe,
2. elle est universelle (tous ses quantificateurs sont universels), et
3. sa matrice est sous forme normale conjonctive.
En utilisant la mise en forme prénexe, puis la Skolemisation, puis la mise en forme clausale
du calcul propositionnel, toute formule peut se transformer dans une formule en forme clausale
equisatisfiable.
Définition 2.56.
— Un littéral est une formule atomique ou la négation d’une formule atomique.

74 / 92
2.6 Unification 65

— Soit ψ une formule avec FV(ψ) = { x1 , . . . , xn }. Sa fermeture universelle est la formule

∀x1 . . . ∀xn ψ .

— Une clause universelle ou clause de premier ordre est la fermeture universelle d’une
disjonction de littéraux.

Lorsqu’une formule est sous forme clausale, on peut ensuite la décomposer en une conjonction
de clauses (du premier ordre) en appliquant la règle ∀x(ϕ ∧ ψ) ≡ (∀xϕ) ∧ (∀xψ). On obtient ainsi
un ensemble de clauses (de premier ordre) équisatisfiable à la formule donnée.
Théorème 2.57 (Satisfiabilité d’un ensemble de clauses). Soit S un ensemble de clauses résultant
de la mise sous forme clausale d’une formule ϕ. Alors ϕ est satisfiable si et seulement si S est
satisfiable.

Ce théorème forme la base de nombreux démonstrateurs automatiques utilisant une représen-

tation des formules sous forme de clauses. Il établit que la recherche de l’insatisfiabilité d’une
formule ϕ est équivalente à la recherche d’insatisfiabilité de sa représentation sous forme clausale
S. Cependant ϕ et S ne sont pas logiquement équivalentes : seule la satisfiabilité est préservée.
Exemple 2.58. Soit

ϕ0 := ∀x∃yP (x, y) ⇒ ∀x∃yP (y, x ∧ Q(x) .

La mise sous forme prénexe donne la formule

ϕ1 := ∃x∀y∀z∃w((P (x, y) ⇒ P (w, z)) ∧ Q(x)) .

Par skolémisation, nous obtenons

ϕ2 := ∀y∀z((P (c, y) ⇒ P (f (y, z), z)) ∧ Q(c)) .

Nous pouvons ensuite mettre la matrice sous forme normale conjonctive :

ϕ3 := ∀y∀z((¬P (c, y) ∨ P (f (y, z), z)) ∧ Q(c)) ,

et obtenir ainsi l’ensemble de clauses :

S := { ∀y∀z(¬P (c, y) ∨ P (f (y, z), z)) , ∀y∀zQ(c) } .

Cet ensemble est equisatisfiable avec la formule ϕ0 .

2.6 Unification
2.6.1 Substitions et MGUs
Dans la suite, on fixe Sf une signature composée de symboles de fonctions et X un ensemble
de variables. Nous nous intéresserons pas, dans cette section, aux symboles de relation.

Définition 2.59. Une substitution est une fonction σ : X → TSf (X) telle que l’ensemble
{ x ∈ X | σ(x) 6= x } est fini.

Exemple 2.60. Supposons Sr = { (f, 2), (g, 1) } et X = { x0 , . . . , xn , . . . }. La fonction σ telle que

σ(x0 ) = f (g(x0 ), x1 ), σ(x1 ) = x2 , et σ(xi ) = xi pour i ≥ 2, est une substitution.
On représente (souvent, dans des implémentation sur ordinateur) et on écrit les substitutions
par des listes de couples clef,valeur (en jargon informatique, c’est des listes associatives), notées
d’habitude par :

{ x1 → t1 , . . . , xn → tn } , ou [ t1 /x1 , . . . , tn /xn ] .

75 / 92
66 Chapitre 2. Calcul des prédicats

La convention est la suivante : étant donnée une telle liste on construit la substitution σ
en posant σ(xi ) = ti ; si une variable x n’apparaît pas dans la liste, alors elle est fixée par σ,
c’est-à-dire σ(x) = x. Ainsi, la substitution de l’exemple 2.60, sera notée par

[f (g(x0 ), x1 )/x0 , x2 /x1 ] .

Exercice 2.61. Argumentez que toute substitution peut être représentée par une liste associative.
Montrez que cette représentation n’est pas unique, c’est-à-dire qu’ils existent plusieurs (même une
infinité) de listes représentant la même substitution.

Définition 2.62. Pour tout terme t, on définit l’action de σ sur t comme suit :

x σ = σ(x) ,
f (t1 , . . . , tn ) σ = f (t1 σ, . . . , tn σ) .

Exemple 2.63. On a

f (g(x), y)[z/x, g(y)/y] = f (g(z), g(y)) , g(f (x, f (y, x)))[g(w)/x] = g(f (g(w), f (y, g(w)))) .

Définition 2.64. La substitution identité (ou vide) est celle qui fixe toutes les variables. Elle est
donc notée par []. La composition de deux substitutions σ et τ , notée τ ◦ σ, est la substitution
définie par :

(τ ◦ σ)(x) = (x σ) τ . (2.2)

Observez que, dans la définition ci-dessus, l’expression à la droite est (σ(x)) τ .

Exemple 2.65. Soient

σ = [ f (x, y)/x ] , τ = [ g(y)/x, f (x, z)/y ] .

Calculons τ ◦ σ :

σ τ
x 7→ f (x, y) →7 f (g(y), f (x, z))
y 7 → y 7 → f (x, z)
z 7→ z 7 → z
..
.
On a donc

τ ◦ σ = [ f (g(y), f (x, y))/x, f (x, z)/y ] .

Exercice 2.66. En généralisant l’exemple 2.65, proposez un algorithme qui calcule la composition
de deux substitutions σ et τ passées en paramètre. Les substitutions, en entrée et en sortie, seront
représentées par des listes associatives.
Exercice 2.67. Prouvez les relations suivantes :

t [] = t ,
t (τ ◦ σ) = (t σ) τ . (2.3)

Prouvez ensuite que la composition de substitutions est associative, et que la substitution identité
est son un élément neutre.
Remarque 2.68. La composition τ ◦σ de deux substitution σ, τ revient à une sorte de composition
fonctionnelle—car on applique d’abord σ et puis τ . Cela justifie de dénoter cette composition par
le symbole usuel (le symbole ◦) de la composition de fonctions.

76 / 92
2.6 Unification 67

Par ailleurs, il est costume en logique (et il s’avère éclaircissant) d’écrire la substitution à la
droite du terme dans l’application d’un substitution à un terme, D’ici les relations (2.2) et (2.3)
qui, en renversant gauche et droite, pourraient apparaître à première vue un peu bizarres.

Définition 2.69. Soient σ et τ deux substitutions. On dit que σ est plus générale que τ (et
on écrit σ ≤ τ ), s’il existe une substitution ρ telle que τ = ρ ◦ σ.

Exemple 2.70. Soit

σ = [f (w, x)/x, z/y] , τ = [f (g(y), x)/x, c/y, c/z, g(y)/w] .

On a alors σ ≤ τ , à cause de

ρ = [c/z, g(y)/w] .

En fait, le calcul de la composition donne :

σ ρ
x 7→ f (w, x) 7→ f (g(y), x)
y 7 → z 7 → c
z 7 → z 7 → c
w 7 → w 7→ g(y)

Définition 2.71. Un problème d’unification est une liste (s1 , t1 ), . . . , (sn , tn ) avec si , ti ∈
TSf (X). Une solution de ce problème—appelé unificateur de (s1 , t1 ), . . . , (sn , tn )—est une sub-
stitution σ telle que si σ = ti σ, pour i = 1, . . . , n. On notera Unif[ (s1 , t1 ), . . . , (sn , tn ) ] l’ensemble
des unificateurs (s1 , t1 ), . . . , (sn , tn ).

Exemple 2.72.

1. La substitution

σ = [g(z)/x, g(z)/y] .

est un unificateur de (f (x, g(z)), f (g(z), y)), car

f (x, g(z))[g(z)/x, g(z)/y] = f (g(z), g(z)) = f (g(z), y)[g(z)/x, g(z)/y] .

2. Nous avons Unif[ (f (x, y), g(z)) ] = ∅. De même, Unif[ (x, g(x)) ] = ∅.

Le but de cette section est de montrer le résultat suivant :

Proposition 2.73. Si Unif[ (s1 , t1 ), . . . , (sn , tn ) ] 6= ∅, alors il existe σ ∈

Unif[ (s1 , t1 ), . . . , (sn , tn ) ] tel que σ ≤ τ pour tout τ ∈ Unif[ (s1 , t1 ), . . . , (sn , tn ) ].
On appelle un tel σ un unificateur plus général des couples (s1 , t1 ), . . . , (sn , tn ). On dira
aussi que σ un MGU des couples (s1 , t1 ), . . . , (sn , tn ), où MGU est un acronyme de l’anglais « Most
General Unifier ».

Exemple 2.74. τ = [g(f (w))/x, g(f (w))/y] ∈ Unif[ (f (x, g(z)), f (g(z), y)) ], mais τ n’est pas un
MGU de ce problème. En fait, σ = [g(z)/x, g(z)/y] est un MGU, et on a σ ≤ τ , car τ = ρ ◦ σ, avec
ρ = [f (w)/z].

77 / 92
68 Chapitre 2. Calcul des prédicats

UNIFIER

Entrée : un problème d’unification (s1 , t1 ), . . . , (sn , tn )

Sortie :
un MGU de (s1 , t1 ), . . . , (sn , tn ) si Unif[ (s1 , t1 ), . . . , (sn , tn ) ] 6= ∅
ECHEC, sinon

1 Si n = 0, retourner la substitution identité

2 Sinon, on analyse le couple (s1 , t1 ) :
3 si s1 = f (r1 , . . . , rk ) et t1 = g(r10 , . . . , rk0 0 ) alors
4 si f 6= g, retourner ECHEC
5 sinon /* f = g implique k = k 0 */
6 retourner UNIFIER( (r1 , r10 ), . . . , (rk , rk0 ), (s2 , t2 ), . . . , (sn , tn ) )
7 si s1 est la variable x, alors :
8 si t1 est aussi la variable x,
9 retourner UNIFIER( (s2 , t2 ), . . . , (sn , tn ) )
10 si x ∈ V AR(t1 ), retourner ECHEC
11 sinon,
12 soit τ le résultat de UNIFIER( (s2 [t1 /x], t2 [t1 /x]), . . . , (sn [t1 /x], tn [t1 /x]) )
13 si τ = ECHEC, retourner ECHEC
14 sinon retourner τ ◦ [t1 /x]
15 si t1 est la variable x, alors
16 traitement comme auparavant, avec s1 à la place de t1

Figure 2.2 – Algorithme d’unification

78 / 92
2.6 Unification 69

2.6.2 Algorithme d’unification

L’algorithme d’unification est illustré en figure 2.6.2. Nous donnons dans la suite des exemples
de calcul de cet algorithme sur des problèmes d’unification.
Exemple 2.75. Considérez le problème suivant :

(f (x, g(z)), f (g(z), x)) , (x, g(z)) .

L’algorithme marche de la facon suivante :

Ligne appel récursif
Entrée Pile des résultats partiels
(ou return)
( f (x, g(z)), f (g(z), x)), (x, g(z) )
6 (x, g(z)), (g(z), x), (x, g(z))
12 (g(z), g(z)), (g(z), g(z)) [g(z)/x]
6 (z, z), (g(z), g(z)) [g(z)/x]
9 (g(z), g(z)) [g(z)/x]
6 (z, z) [g(z)/x]
9 [g(z)/x]
1 [] ◦ [g(z)/x]

Exercice 2.76. Exercez vous maintenant avec les problèmes suivants :

1. (f (g(k(x)), y), f (y, g(x))),
2. (f (g(x), x), f (y, g(z))), (g(x), y)),
3. (f (y, k(y), g(x)), f (k(x), k(y), y)).

Terminaison. Définissons la complexité d’un terme comme suit :

](x) = 1 ,
X
](f (t1 , . . . , tn )) = 1 + ]ti .
i=1,...,n

La complexité d’un problème (que nous noterons par le même symbole ]) est un couple de nombres
entiers (non-négatifs) qui se définit comme suit :
[ X
]((s1 , t1 ), . . . , (sn , tn )) = ( card( V ar(si ) ∪ V ar(ti )) , ](si ) + ](ti ) ) .
i=1,...,n i=1,...,n

Le lecteur notera qu’à chaque appel récursif, le problème en paramètre a complexité strictement
plus petite par rapport à l’ordre lexicographique sur N × N. Donc, l’algorithme ne peut pas faire
une suite infinie d’appels récursifs, et il termine.

2.6.3 Correction et completude

Nous souhaitons prouver les propositions suivantes.

Proposition 2.77 (Correction). Soit π un problème d’unification. Si UNIFIER(π) retourne

ECHEC, alors Unif[ π ] = ∅ ; si UNIFIER(π) retourne une substitution σ, alors σ ∈ Unif[ π ] et, de
plus, σ est un MGU de π.
Proposition 2.78 (Complétude). Soit π un problème d’unification. Si Unif[ π ] = ∅, alors
UNIFIER(π) retourne ECHEC ; si Unif[ π ] 6= ∅, alors UNIFIER(π) retourne un MGU de π.

Afin de prouver ces deux propositions, introduisons quelques notations, ainsi que la Proposi-
tion 2.79, qui est le résultat nécessaire le moins évident à démontrer.
— ∆ = { (t, t) | t ∈ TSf (X) } et ∆n = ∆ × . . . × ∆,
| {z }
n−fois

79 / 92
70 Chapitre 2. Calcul des prédicats

— si π = (s1 , t1 ), . . . , (sn , tn ), alors `(π) = n et πσ = (s1 σ, t1 σ), . . . , (sn σ, tn σ).

Avec cette notation remarquez que

σ ∈ Unif[ π ] ssi πσ ∈ ∆`(π) .

Proposition 2.79. Soient π et ψ deux problemes d’unification, soit σ un MGU de π. Alors

Unif[ π, ψ ] = { ρ ◦ σ | ρ ∈ Unif[ ψσ ] } . (2.4)

Par conséquent, si ρ est un MGU de ψσ , alors τ = ρ ◦ σ un MGU de π, ψ.

Démonstration. Observons que si τ ∈ Unif[ π, ψ ] alors τ ∈ Unif[ π ] et, car σ est un MGU de π,
σ ≤ τ , c’est-à-dire τ = ρ ◦ σ pour une substitution ρ. Car τ ∈ Unif[ ψ ], on remarquera que

(ψσ )ρ = ψρ◦σ = ψτ ∈ ∆`(ψ) ,

donc ρ est un unificateur de ψσ et que τ ∈ { ρ ◦ σ | ρ ∈ Unif[ ψσ ] }.

Nous avons montré que l’ensemble sur la gauche de (2.4) est inclus dans celui de droite. Montrons
donc l’autre inclusion. Si ρ ∈ Unif[ ψσ ], alors

ψρ◦σ = (ψσ )ρ ∈ ∆`(ψσ ) = ∆`(ψ) , car ρ ∈ Unif[ ψσ ]

`(π) `(π)
πρ◦σ = (πσ )ρ ∈ (∆ )ρ ⊆ ∆ , car σ ∈ Unif[ π ]

donc ρ ◦ σ ∈ Unif[ π, ψ ]. Ceci complète la preuve de l’égalité (2.4).

Soient maintenant ρ un MGU de ψσ et soit τ ∈ Unif[ π, ψ ]. Grâce à l’égalité (2.4), nous pouvons
écrire τ = ρ0 ◦ σ avec ρ0 ∈ Unif[ ψσ ] ; on a alors ρ ≤ ρ0 , donc ρ0 = θ ◦ ρ pour une substitution θ et,
par conséquent, τ = θ ◦ ρ ◦ σ, ce qui montre que ρ ◦ σ ≤ τ . Nous avons donc montré que ρ ◦ σ est
un MGU du problème π, ψ.
La preuve de correction et complétude de l’algorithme d’unification repose sur les lemmes
suivants :
Lemme 2.80. Les faits suivants sont vrais :
1. Si f 6= g, alors Unif[ (f (r1 , . . . , rk ), g(r10 , . . . , rk0 0 )) ] = ∅.
2. Si x ∈ V ar(t) et t 6= x, alors Unif[ (x, t) ] = ∅.
3. Unif[ π, ψ ] = Unif[ ψ, π ] ⊆ Unif[ ψ ].
En particulier, si Unif[ (s, t) ] = ∅, alors Unif[ (s, t), (s2 , t2 ), . . . , (sn , tn ) ] = ∅.
Lemme 2.81. On a

Unif[ (f (r1 , . . . , rk ), f (r10 , . . . , rk0 )), (s2 , t2 ), . . . , (sn , tn ) ]

= Unif[ (r1 , r10 ), . . . , (rk , rk0 ), (s2 , t2 ), . . . , (sn , tn ) ] .

Lemme 2.82. Un MGU de

(x, x), (s2 , t2 ), . . . , (sn , tn )
est ρ, où ρ est un MGU de
(s2 , t2 ), . . . , (sn , tn ) .
Si ce dernier problème ne possède pas de solution, alors il en est de même pour (x, x), (s2 , t2 ), . . . , (sn , tn ).
Lemme 2.83. Supposons x 6∈ V ar(t). Un MGU de

(x, t), (s2 , t2 ), . . . , (sn , tn )

est ρ ◦ [t/x], où ρ est un MGU de

(s2 , t2 )[t/x], . . . , (sn , tn )[t/x] .

Si ce dernier problème ne possède pas de solution, alors il en est de même pour (x, t), (s2 , t2 ), . . . , (sn , tn ).

80 / 92
2.6 Unification 71

Les Lemmes 2.82 et 2.83 sont des conséquences de la Proposition 2.79, en raison du fait que
— la substitution identité [] est un MGU du problème (x, x) ;
— [t/x] est évidemment un MGU du problème (x, t) quand x 6∈ V ar(t).
Exercice 2.84. A l’aide des Lemmes 2.80-2.83 complétez une preuve formelle de correction et
complétude de l’algorithme d’unification.

Exemple : démonstration de la Proposition 2.77, correction de l’algorithme. L’algorithme retourne

échec, sans appels recursifs, à cause des lignes 4,10 et 13. Pour les lignes 4 et 10, on utilise le
Lemme 2.80. Pour la ligne 13, on utilise le Lemme 2.83.
Les appels récursifs se trouvent aux lignes 6 et 9. On justifie la ligne 6 par le Lemme 2.81, et la
ligne 9 par le e Lemme 2.82.
Nous argumentons ainsi que si UNIFIER(π) retourne ECHEC, alors Unif[ ( ]π) = ∅.
La preuve que si UNIFIER(π) retourne σ, alors σ est un MGU de π est similaire.

81 / 92
72 Chapitre 2. Calcul des prédicats

2.7 Résolution
2.7.1 Substitution, sur les formules propositionnelles
L’action d’une substitution s’étend aisément aux formules sans quantificateurs :
— R(t1 , . . . , tn )σ = R(t1 σ, . . . , tn σ),
— (¬ϕ)σ = ¬(ϕσ),
— (ϕ ◦ ψ)σ = ϕσ ◦ ψσ, ◦ ∈ { ∨, ∧, ⇒ }.
Rappel (cf. Définition 2.56). Un littéral est ou bien une formule atomique, ou bien la négation
d’une formule atomique. Une clause universelle est la fermeture universelle d’une disjonction de
littéraux.
Désormais, clause sera un synonyme de clause universelle. Bien que une clause soit une formule
de la forme
∀x1 , . . . , ∀xn (l1 ∨ . . . ∨ lk )
avec li des littéraux et { x1 , . . . , xn } = FV({ l1 , . . . , ln }), il est habituel de laisser l’écriture des
quantificateurs implicite. Par exemple, nous allons considérer l’expression

R(x, y) ∨ ¬Q(f (x), z)

comme un raccourci de sa fermeture universelle :

∀x∀y∀z(R(x, y) ∨ ¬Q(f (x), z)) .

Pour de raison de convenance, nous avons donc décidé d’écrire de la même façon une clause
universelle et sa matrice (la sous-formule sans quantificateurs). Au cas nous aurions besoin de
distinguer une clause universelle C de sa matrice, nous allons écrire Cmat pour la matrice.
La substitution s’étend, en particulier, aux littéraux et aux clauses :
1. R(t1 , . . . , tn )σ = R(t1 σ, . . . , tn σ),
2. (¬R(t1 , . . . , tn ))σ = ¬(R(t1 , . . . , tn )σ),
Wn Wn
3. ( i=1 li )σ = i=1 (li )σ.
Notation 2.85. Si C est une clause universelle et σ une substitution, nous allons utiliser la nota-
tion Cσ pour la fermeture universelle de Cmat σ. Évidemment, Cσ est aussi une clause universelle.

Un unificateur de deux litteraux l0 et l1 est une substitution σ telle que l0 σ = l1 σ.

Lemme 2.86. σ est un unificateur de l0 et l1 ssi
1. l0 = R(s1 , . . . , sn ), l1 = R(t1 , . . . , tn ), et σ ∈ Unif[ (s1 , t1 ), . . . , (sn , tn ) ], ou bien
2. l0 = ¬R(s1 , . . . , sn ), l1 = ¬R(t1 , . . . , tn ), et σ ∈ Unif[ (s1 , t1 ), . . . , (sn , tn ) ].
Du Lemme il en découle tout de suite que l’ensemble des unificateurs de deux littéraux,
appelons encore une fois Unif[ l0 , l1 ], ou bien il est vide, ou bien il possède une substitution la
plus générale, qui sera appelé un MGU de l0 et l1 .

2.7.2 Les règles du calcul de la résolution

On peut considérer le calcul de la résolution comme une généralisation de la méthode de la
coupure propositionnelle. Comme dans le cas propositionnel, la méthode de résolution prend en
paramètre un ensemble Γ de clauses (universelles) et essaye de dériver la clause vide ⊥ depuis
les clauses dans Γ. Les deux règles pour dériver des nouvelles clauses à partir des clauses déjà
construites sont les suivantes :
C ∨ A0 C 0 ∨ ¬A1
Résolution
(C ∨ C 0 )σ

82 / 92
2.7 Résolution 73

où σ est un MGU des formules atomiques A0 et A1 , et

C ∨ l0 ∨ l1
Factorisation
(C ∨ l0 )σ

où σ est un MGU des littéraux l0 et l1 .

Exemple 2.87 (Règle de Résolution). La suivante est une instance de la règle de résolution :

¬HabiteCL(x) ∨ T ue(x, Agate) ¬T ue(Charles, y) ∨ Hait(x, y)

¬HabiteCL(Charles) ∨ Hait(Charles, Agate)

Ici l0 = T ue(x, Agate) et l1 = T ue(Charles, y), C = HabiteCL(x), C 0 = Hait(x, y). En fait,

[Charles/x, Agate/y] est un MGU de T ue(x, Agate) et T ue(Charles, y).

Exemple 2.88 (Règle de Factorisation). La suivante est une instance de la règle de factorisation :

¬HabiteCL(x) ∨ Hait(x, y) ∨ T ue(x, Agate) ∨ T ue(Charles, y)

¬HabiteCL(Charles) ∨ Hait(Charles, Agate) ∨ T ue(Charles, Agate)

Le MGU est encore une fois [Charles/x, Agate/y].

2.7.3 Correction du calcul de la résolution

La méthode de résolution est correcte, c’est-à-dire, la conclusion d’une règle est conséquence
logique des prémisses de la règle. Explicitement, chaque fois que M |= Ci , où Ci , i = 1, . . . , n avec
n ∈ { 1, 2 } sont les prémisses d’une règle, alors on a M |= C0 , où C0 est la conclusion de la règle.
En fait, on peut penser que les règles du calcul sont obtenues comme synthèse de deux règles,
l’une qui porte sur les subsitutions (et les quantificateurs universels), et l’autre étant la règle
correspondante propositionnelle :

C ∨ A0 C 0 ∨ ¬A1
σ σ
Cσ ∨ A0 σ C 0 σ ∨ ¬A0 σ
Résolution propositionnelle
Cσ ∨ C 0 σ
où on a A0 σ = A1 σ. De façon semblable :

C ∨ l0 ∨ l1
σ
Cσ ∨ l0 σ ∨ l0 σ
Factorisation propositionnelle
Cσ ∨ l0 σ

Nous allons, dans la suite, justifier ces règles “plus élémentaires”.

Lemme 2.89. Soient ϕ une formule sans quantificateurs, σ une substitution, M une S-structure
et V une valuation. On a que

M, V |= ϕσ ssi M, Vσ |= ϕ , (2.5)

où Vσ est la valuation définie par la règle suivante :

(Vσ)(x) = J σ(x) KM,V .

Notez que si σ = [t1 /x1 , . . . , tn /xn ], alors Vσ = V[x1 := J t1 KM,V , . . . , xn := J tn KM,V ] est la
variante de V satisfaisant aux lois suivantes :
(
J ti KM,V , si y = xi , pour quelques i,
V[x1 := J t1 KM,V , . . . , xn := J tn KM,V ](y) =
V(y), sinon.

83 / 92
74 Chapitre 2. Calcul des prédicats

Démonstration du Lemme 2.89. La preuve de cet énoncé se fait aisément par induction. Nous nous
limiterons à illustrer le cas de base. Pour toute variable y ∈ X, nous avons

J y KM,Vσ = (Vσ)(y) = J σ(y) KM,V .

Ainsi, nous avons

M, V |= R(y1 , . . . , ym )σ ssi M, V |= R(σ(y1 ), . . . , σ(ym ))

ssi (J σ(y1 ) KM,V , . . . , J σ(ym ) KM,V ) ∈ RM
ssi (J y1 KM,Vσ , . . . , J ym KM,Vσ ) ∈ RM
ssi M, Vσ |= R(y1 , . . . , ym ).

Lemme 2.90. Pour toute clause universelle C et toute substitution σ, la règle d’inférence suivante
est correcte :
C
σ
Cσ
C’est-à-dire, si M |= C, alors M |= Cσ, pour toute S-structure M.
Démonstration. Supposons que M |= C ; pour montrer que M |= Cσ, nous devons montrer que
M, V |= (Cσ)mat , où V est une valuation arbitraire. En considération que (Cσ)mat = (Cmat )σ et par
le Lemme 2.89 cela revient à vérifier que M, Vσ |= Cmat ; cette dernière relation et en effet vraie à
cause de l’assomption M |= C.
Pour les règle de factorisation et résolution propositionnelles, nous devons les justifier. En fait,
ces règle manipulent des clauses universelles et non pas simplement des clauses. Par ailleurs, les
démonstrations que ces règles propositionnelles s’étendent au cas des clauses universelles sont assez
faciles.
Lemme 2.91. Pour toute couple de clauses universelles de la forme C1 ∨ l et C2 ∨ ¬l (avec l un
littéral), la règle d’inférence suivante est correcte :
C1 ∨ l C2 ∨ ¬l
Résolution propositionnelle
C1 ∨ C2
C’est-à-dire, si M |= C1 ∨ l et M |= C2 ∨ ¬l, alors M |= C1 ∨ C2 , pour toute S-structure M.
Démonstration. Nous devons montrer que M, V |= (C1 ∨ C2 )mat pour toute valuation V. Cela est
une conséquence de (C1 ∨ C2 )mat = (C1 )mat ∨(C2 )mat , du fait que M, V |= (C1 ∨ l)mat (= (C1 )mat ∨l),
M, V |= (C2 ∨ ¬l)mat (= (C2 )mat ∨ ¬l), et du fait que la règle de la coupure propositionelle est
correcte.
Exercice 2.92. Montrez que la règle de factorisation propositionnelle s’étend aux clauses univer-
selles.

2.7.4 Complètude du calcul de la résolution

Soit Γ un ensemble de clauses universelles. Nous disons que Γ est saturé si toute clause dérivable
(via résolution et factorisation) de formules dans Γ appartient déjà à Γ ; nous disons que Γ est
cohérent si ⊥ 6∈ Γ.
Théorème 2.93. Un ensemble saturé et cohérent de clauses admet au moins un modèle.
En fait, nous allons montrer la proposition suivante :
Proposition 2.94. Si un ensemble saturé de clauses Γ n’admet pas un modèle, alors ⊥ ∈ Γ.
Démonstration. Soit S = (Sf , Sr ) le langage ; nous allons nous intéresser au langage propositionnel
caractérisé par le fait que Prop est l’ensemble de proposition atomiques du langage S.
Remarquons d’abord que, étant donnée une valuation (au sens propositionnel) v : Prop →
{ 0, 1 }, nous pouvons définir une S-structure Mv de la façon suivante :

84 / 92
2.7 Résolution 75

— DMv := TSf (X) ;

— pour tout f ∈ Sf , f Mv est la fonction qui envoie un tuplet (t1 , . . . , tn ) ∈ TSf (X) vers le
terme f (t1 , . . . , tn ) ;
— pour tout R ∈ Sr , nous posons

RMv := { (t1 , . . . , tn ) ∈ TSf (X)n | v( R(t1 , . . . , tn ) ) = 1 } .

La structure Mv ainsi définie a cette propriété importante :

Lemme 2.95. Si C est une clause universelle, alors

Mv |= C ssi v(Cσ) = 1, pour toute substitution σ.

Preuve du Lemme. Une valuation V de l’ensemble de variables vers DMv = TSf (X) n’est rien
d’autre qu’une substitution. En tenant compte que C est implicitement quantifiée universellement,
la condition Mv |= C est vraie quand Mv , σ |= Cmat , pour toute substitution σ. Rappelons que [] est
la substitution identité ; le Lemme 2.89 montre que Mv , σ |= Cmat est équivalent à Mv , [] |= Cmat σ ;
cette condition revient à dire que v(Cσ) = 1 (au sens propositionnel).
Il en découle que l’ensemble de clauses propositionnelles

∆ = { Cσ | C ∈ Γ, σ une substitution }

n’est pas satisfaisable au sens propositionnel. En fait, si v est une valuation vérifiant toutes les
formules de cet ensemble, alors Mv est un modèle satisfaisant toutes les formules de Γ.
Pour le Théorème de compacité, il existe un sous-ensemble fini ∆f ⊆ ∆ tel que ∆f n’est pas
satisfaisable. Car la méthode de la coupure est complète, il existe une suite de clauses D1 , . . . , Dn
avec Dn = ⊥ (c’est-à-dire, Dn est la clause vide), telle que, pour tout i > 0 :
1. Di ∈ ∆f , ou
2. Di est déduite de Dj et Dk (avec j, k < i) via la règle de coupure, ou
3. Di est déduite de Dj (avec j < i) via la règle de factorization (propositionnelle).
Lemme 2.96. Pour tout i = 1, . . . , n, ils existent Ci ∈ Γ et une substitution ρi telle que Di = Ci ρi .
Preuve du Lemme. Par induction (sur i = 1, . . . , n), et par cas.
1. Si Di ∈ ∆f ⊆ ∆, alors cela est vrai par définition de ∆ : Di = C ◦ σ pour une clause C ∈ Γ
et une substitution σ ; on peut donc poser Ci := C et ρi := σ.
2. (Voir la Figure 2.3.) Supposons que Di est déduite de Dj et Dk (avec j, k < i) via la règle de
coupure. Par hypothèse d’induction, ils existent Cj , Ck ∈ Γ et deux substitutions ρj , ρk tels
que Dj = Cj ρj et Dk = Ck σk .
Supposons donc que Dj = D ∨ A, Dk = D0 ∨ ¬A, et Di = D ∨ D0 . On a alors Cj = C ∨ A0 ,
Ck = C 0 ∨ ¬A1 , D = Cρj , D0 = C 0 ρk , et A0 ρj = A = A1 ρk . Sans perte de généralité, nous
pouvons assumer qu’il n’y a pas des variables en commun entre Cj et Ck , que ρj fixe les
variables de Ck , et ρk fixe les variables de Cj . Par conséquent, si ρj = [t1 /x1 , . . . , tn /xn ] et
ρk = [s1 /y1 , . . . , sm /ym ], alors τ = [t1 /x1 , . . . , tn /xn , s1 /y1 , . . . , sm /ym ] est un unificateur de
A0 et A1 , Dj = Cj τ et Dk = Ck τ . Soit σ un MGU de A0 et A1 , on a alors τ = ρ ◦ σ, et

Di = D ∨ D0 = Cτ ∨ C 0 τ = (C ∨ C 0 )τ = [(C ∨ C 0 )σ]ρ .

Nous pouvons alors poser Ci := (C ∨ C 0 )σ et ρi := ρ. Ci ∈ Γ car elle est déduite de Ci et Cj

via la règle de résolution depuis Cj , Ck ∈ Γ, et en plus Γ est saturé.
3. Supposons enfin que la clause Di est déduite de Dj (avec j < i) via la règle de factorisation
propositionnelle. Par hypothèse d’induction, il existe une clause Cj ∈ Γ et une substitution
ρj telle que Dj = Cj ρj .
Si Dj = D ∨ ` ∨ `, alors Cj = C ∨ `0 ∨ `1 avec D = Cρj , et ` = `0 ρj = `1 ρj . La substitution ρj
est donc un unificateur de `0 et `1 ; si σ est un MGU de `0 et `1 , alors il existe une substitution
ρ telle que ρj = ρ ◦ σ.

85 / 92
76 Chapitre 2. Calcul des prédicats

ρj ρk

C ∨ A0 C 0 ∨ ¬A1 D∨A D0 ∨ ¬A
Résolution Coupure
(C ∨ C 0 )σ D ∨ D0
? : σ, ρi

Figure 2.3 – Simulation de la coupure par la résolution

Nous pouvons donc poser Ci := (C ∨ `0 )σ et ρi := ρ ; Ci ∈ Γ car il a été déduit depuis Cj ∈ Γ

via la règle de factorisation (du premier ordre) et Γ saturé ; par ailleurs

Ci ρi = [(C ∨ `0 )σ]ρi = (C ∨ `0 )(ρi ◦ σ) = (C ∨ `0 )ρj = Cρj ∨ `0 ρj = D ∨ ` = Dj .

En particulier, le Lemme dit que Cn ∈ Γ et que Cn ρn = ⊥. Il est facile à voir que si Cn 6= ⊥,

alors Cn ρ 6= ⊥ (pour n’importe quel ρ) ; par conséquent, nous avons Cn = ⊥ ∈ Γ. Cela complète
la démonstration de la Proposition 2.94.

Une analyse fine de la preuve de la Proposition 2.94 amène à une preuve du théorème suivant.

Théorème 2.97. Si un ensemble de clauses Γ n’admet pas un modèle, alors il existe une preuve
de ⊥ à partir de Γ dans le calcul de la résolution.

Exemple 2.98. L’ensemble de clauses universelles Γ défini par

Γ :={ P (x) ∨ Q(f (y)), ¬P (c), ¬Q(f (g(x))) ∨ Q(g(x)), ¬Q(f (g(x))) ∨ Q(g(x)), ¬Q(g(c)) } ,

est insatisfaisable. A l’aide de la méthode de la coupure, on peut donc construire une preuve de
la clause vide à partir de l’ensemble ∆ = { Cσ | C ∈ Γ, σ une substitution }. Cette preuve peut
ensuite être simulée, par le Lemme 2.96, dans le calcul de la résolution, pour produire une preuve
de la clause vide dans ce calcul. La figure 2.4 montre une preuve par coupure de la clause vide de
∆ et sa simulation par résolution depuis Γ.

P (c) ∨ Q(f (g(c))) ¬Q(f (g(c))) ∨ Q(g(c))

Coupure
P (c) ∨ Q(g(c)) ¬P (c)
Coupure
Q(g(c)) ¬Q(g(c))
Coupure
⊥

P (x) ∨ Q(f (y)) ¬Q(f (g(x))) ∨ Q(g(x))

Résolution y 7→ g(x)
P (x) ∨ Q(g(x)) ¬P (c)
Résolution x 7→ c
Q(g(c)) ¬Q(g(c))
Résolution
⊥

Figure 2.4 – Simulation de preuves, exemple

2.7.5 Indecidabilité
Bien que le calcul soit correct et complet, nos résultats n’amènent pas à la construction d’un
algorithme—c’est à un quelque programme qui s’arrête toujours et qui donne la réponse souhaitée
à la fin des calculs—pour décider si un ensemble de clauses universelles est satisfaisable ou non.
Si nous essayons d’adapter l’algorithme de résolution propositionnelle, cf. [Link], on rencontre un
problème majeur : cet algorithme pourrait ne jamais se terminer, en raison de la possibilité de

86 / 92
2.7 Résolution 77

produire une infinité de nouvelles de clauses. Pour s’en apercevoir, il suffit de considerer le langage
S avec SF = { (o, 0), (s, 1) } et SR = { (P, 1) }. Considérons l’ensemble C de clauses donné par

C := { ¬P (x) ∨ P (s(x)), P (o) } .

L’algorithme engendrera, l’une après l’autres, toutes les clauses de la forme

P ( s(. . . s( o) . . .) )
| {z }
n fois

En fait, nous ne pouvons simplement pas trouver un algorithme ; les prochains théorèmes pour-
ront être mieux compris dans le cadre du chapitre suivant, autour de la calculabilité, où nous
formaliserons la notion d’algorithme.

Théorème 2.99. Il n’existe aucun algorithme tel que, étant donné une formule du premier ordre
close ϕ, il répond oui si ϕ admet un modèle, et non si ϕ est insatisfaisable.
Puisque décider de la satisfaisabilité d’une formule du premier ordre se réduit (via la mise
en forme clausale) à décider de la satisfaisabilité d’un ensemble de clauses, nous pouvons déduire
cet autre théorème à partir du précédent :
Théorème 2.100. Il n’existe aucun algorithme qui, étant donné un ensemble fini de clauses C,
répond oui si C admet un modèle, et non si C est insatisfaisable.

2.7.6 Utilisation d’un démonstrateur automatique

Exemple 2.101 (L’île mysterieuse). Écoutez cette histoire.

Chaque habitant de cette île est soit un cavaliers, soit un escroc. Il peut être un loup
garou (il est donc dangereux, car il mange les hommes pendant les nuits de lune pleine).
Un loup garou est lui aussi soit un cavalier soit un escroc. Les cavaliers disent toujours
la vérité, les escrocs mentent toujours. Un explorateur débarque sur cette île et rencontre
Albert, Bernard et Charles. Il est au courant qu’un des trois est un loup garou.
— Albert prétend que Bernard est un loup ;
— Bernard dit qu’il n’est pas un loup ;
— Charles dit qu’au moins deux entre eux sont des escrocs.
Qui doit choisir l’explorateur comme guide de son voyage ?

Nous avons formalisé cette histoire en logique du premier ordre, dans un fichier prêt à être lu par
le démonstrateur automatique Prover9. Ce fichier apparaît dans la Figure 2.5. Le prouveur auto-
matique confirme que Albert est un loup garou, et donc l’explorateur ne choisira pas Albert comme
guide. La preuve construite par le prouveur apparait dans la Figure 2.6. Le lecteur y reconnaîtra
plusieurs instances de la règle de résolution. L’analyse de la preuve montre que l’hypothèse ’Albert
n’est pas un loup garou’ n’a pas été utilisée. Cela veut dire que la connaissances à disposition de
l’explorateur, (qui est modélisée dans la liste des assomptions) est elle même incohérente.
Un procédé analogue peut être utilisé pour montrer que une liste de spécifications d’un pro-
gramme/logiciel est incohérente, et donc ne peut pas être assuré par n’importe quel programme.
Réfléchir avant se mettre à programmer ! ! !

Exemple 2.102 (Le mystère du Château Letot). Écoutez cette autre histoire.

87 / 92
78 Chapitre 2. Calcul des prédicats

set ( bin ary_resolution ).

formulas ( assumptions ).
Cavalier ( x ) | Escroc ( x ).
LoupGarou ( albert ) | LoupGarou ( bernard ) | LoupGarou ( charles ).
Cavalier ( albert ) -> LoupGarou ( bernard ).
Escroc ( albert ) -> - LoupGarou ( bernard ).
Cavalier ( bernard ) -> - LoupGarou ( bernard ).
Escroc ( bernard ) -> LoupGarou ( bernard ).
Cavalier ( charles ) -> (
( Escroc ( albert ) & Escroc ( bernard ))
| ( Escroc ( albert ) & Escroc ( charles ))
| ( Escroc ( bernard ) & Escroc ( charles ))
).
Escroc ( charles ) -> -(
( Escroc ( albert ) & Escroc ( bernard ))
| ( Escroc ( albert ) & Escroc ( charles ))
| ( Escroc ( bernard ) & Escroc ( charles ))
).
end_of_list .

formulas ( goals ).
LoupGarou ( albert ).
end_of_list .

Figure 2.5 – Fichier d’entrée pour Prover9

— Quelqu’un qui habite Château Letot a tué tante Agate.

— Agate, le majordome, et Charles habitent Château Letot, et ils sont les seuls qui
l’habitent.
— Un tueur haït toujours sa victime, et il n’est jamais plus riche que sa victime.
— Charles haït personne que tante Agate haït.
— Agate haït tous sauf le majordome.
— Le majordome haït tous ceux qui ne sont pas plus riches de tante Agate.
— Le majordome haït tous ceux qui tante Agate haït.
— Personne haït tous le monde.
— Agate n’est pas le majordome.
Qui a tué tante Agate ?
Nous avons utilisé le prouveur automatique Prover9 pour montrer que Agate s’est suicidé ; en
fait, ’Agate a tué Agate’ est une conséquence logique des faits décrits concernant le Château Letot.
Le procédé est comme auparavant (voir l’île mystérieuse). Nous avons d’abord modélisé l’histoire
(base de connaissances, ou ontologie) en logique du premier ordre, en construisant ainsi un ensemble
d’assomptions ; la phrase ’Agate a tuée Agate’ étant la formule but à démontrer 4 . Le code qui
a été fourni en entrée à Prover9 apparaît dans la figure 2.7. Prover9 transforme d’abord cet
ensemble de formules dans un ensemble de clauses universelles. Observez donc l’introduction de
nouvelles constantes et de symboles de fonction par élimination de quantificateurs existentiels
(Skolemization), la mise sous forme clausale, et l’inclusion du but parmi les assomptions, via sa
négation (voir figure 2.8). La preuve que le but est une conséquence logique des assomptions
apparaît dans la figure 2.9 Nous avons utilisé les outils gvizify (pour transformer la sortie du
Prover9—très souvent assez difficile à décrypter—vers un graphe décrit dans le langage dot) est
graphviz (pour dessiner des graphes à partir de leur description en langage dot) afin de présenter
cette preuve sous forme de diagramme.
Un dernier remarque s’impose. Parmi les symboles de relation de notre langage nous avons
utilisé le symbole = sans avoir ajouté, parmi les assomptions, aucune hypothèse sur ce symbole.
4. Dans la notation que nous avons utilisé dans le cours, les assomptions correspondent à l’ensemble Γ et le but
à ϕ quand on se pose la question si ϕ est une conséquence logique de Γ (Γ |= ϕ ?)

88 / 92
 2.7 Résolution 79

{3} {1}
Cavalier(bernard) Cavalier(albert)
-> ->
-LoupGarou(bernard) LoupGarou(bernard)

{5}
Cavalier(charles)
{10} {8} -> Escroc(albert)
-Cavalier(bernard) -Cavalier(albert) {9} Cavalier(x) & Escroc(bernard)
| | | Escroc(x) | Escroc(albert)
-LoupGarou(bernard) LoupGarou(bernard) & Escroc(charles)
| Escroc(bernard)
& Escroc(charles)

{6}
Escroc(charles)
->
-(Escroc(albert) {13} {12}
{21} {20}
& Escroc(bernard) -Cavalier(charles) -Cavalier(charles)
-LoupGarou(bernard) LoupGarou(bernard)
| Escroc(albert) | Escroc(bernard) | Escroc(albert)
| Escroc(bernard) | Escroc(albert)
& Escroc(charles) | Escroc(charles) | Escroc(charles)
| Escroc(bernard)
&
Escroc(charles))

{25} {23}
{17} {28}
Escroc(bernard) | Escroc(albert) |
-Escroc(charles) Escroc(bernard)
Escroc(charles) | Escroc(charles) |
| -Escroc(albert) | Escroc(albert)
Escroc(charles) Escroc(charles)

{18}
{29} {26} {4}
-Escroc(charles)
Escroc(bernard) | Escroc(bernard) | Escroc(bernard) ->
|
-Escroc(charles) Escroc(charles) LoupGarou(bernard)
-Escroc(bernard)

{24} {16}
{30}
Escroc(albert) | -Escroc(bernard) |
Escroc(bernard)
Escroc(charles) LoupGarou(bernard)

{2}
{31} {32}
Escroc(albert) ->
-Escroc(charles) LoupGarou(bernard)
-LoupGarou(bernard)

{15}
{33}
-Escroc(albert) |
Escroc(albert)
-LoupGarou(bernard)

{34} $F

Figure 2.6 – Visualisation de la preuve construite par Prover9

89 / 92
80 Chapitre 2. Calcul des prédicats

set ( bin ary_resolution ).

formulas ( assumptions ).
exists x ( HabiteCL ( x ) & Tue (x , agate )).
HabiteCL ( agate ) & HabiteCL ( maj ) & HabiteCL ( charles ) &
( HabiteCL ( x ) -> ( x = agate | x = maj | x = charles )).
Tue (x , y ) -> ( Hait (x , y ) & - PlusRiche (x , y )).
Hait ( agate , z ) -> - Hait ( charles , z ).
( - Hait ( agate , x )) -> x = maj .
x != maj -> Hait ( agate , x ).
- PlusRiche (x , agate ) -> Hait ( maj , x ).
Hait ( agate , x ) -> Hait ( maj , x ).
- ( exists x all y Hait (x , y )).
agate != maj .
end_of_list .

formulas ( goals ).
Tue ( agate , agate ).
end_of_list .

Figure 2.7 – Fichier entrée pour le château Letot

HabiteCL ( c1 ). [ clausify (1)].

Tue ( c1 , agate ). [ clausify (1)].
HabiteCL ( agate ). [ clausify (2)].
HabiteCL ( maj ). [ clausify (2)].
HabiteCL ( charles ). [ clausify (2)].
- HabiteCL ( x ) | agate = x | maj = x | charles = x . [ clausify (2)].
- Tue (x , y ) | Hait (x , y ). [ clausify (3)].
- Tue (x , y ) | - PlusRiche (x , y ). [ clausify (3)].
- Hait ( agate , x ) | - Hait ( charles , x ). [ clausify (4)].
Hait ( agate , x ) | maj = x . [ clausify (5)].
maj = x | Hait ( agate , x ). [ clausify (6)].
PlusRiche (x , agate ) | Hait ( maj , x ). [ clausify (7)].
- Hait ( agate , x ) | Hait ( maj , x ). [ clausify (8)].
- Hait (x , f1 ( x )). [ clausify (9)].
agate != maj . [ assumption ].
- Tue ( agate , agate ). [ deny (10)].

Figure 2.8 – Château Letot : forme clausale

90 / 92
 2.7 Résolution 81

{2}
HabiteCL(agate)
& HabiteCL(maj) &
{1} (exists x
HabiteCL(charles)
(HabiteCL(x) &
& (HabiteCL(x)
Tue(x,agate)))
-> x = agate
| x = maj |
x = charles)

{11} -HabiteCL(x) {3} Tue(x,y) {7}

{12} HabiteCL(c1) | agate = x | maj -> Hait(x,y) & -PlusRiche(x,agate)
= x | charles = x -PlusRiche(x,y) -> Hait(maj,x)

{27} agate = {16}

{18} {19} -Tue(x,y) {8} Hait(agate,x) {9} -(exists x {17} -Tue(x,y) |
c1 | maj = c1 PlusRiche(x,agate)
Tue(c1,agate) | Hait(x,y) -> Hait(maj,x) all y Hait(x,y)) -PlusRiche(x,y)
| charles = c1 | Hait(maj,x)

{28} c1 = agate {4} {5} {22}

{32} {23} {31} Hait(maj,x)
| c1 = maj | c1 Hait(agate,x) -> -Hait(agate,x) -Hait(agate,x)
Hait(c1,agate) -Hait(x,f1(x)) | -Tue(x,agate)
= charles -Hait(charles,x) -> x = maj | Hait(maj,x)

{40} c1 = {20} {21}

{35} {39}
agate | c1 = maj | -Hait(agate,x) | {24} agate != maj Hait(agate,x)
-Hait(agate,f1(maj)) -Tue(f1(maj),agate)
Hait(charles,agate) -Hait(charles,x) | maj = x

{48} c1 =
{41} f1(maj)
agate | c1 = maj | {25} maj != agate
= maj
-Hait(agate,agate)

{49} c1 = agate {43} {10}

| c1 = maj -Tue(maj,agate) Tue(agate,agate)

{26}
{50} c1 = agate
-Tue(agate,agate)

{53} $F

Figure 2.9 – La preuve trouvée par Prover9

91 / 92
82 Chapitre 2. Calcul des prédicats

Notamment, nous aurions du ajouter des clauses explicitant le fait que l’égalité est réflexive, tran-
sitive, symétrique, et congruentielle. Par exemple, nous aurions du expliciter que si x = y et
Hait(x, z) alors Hait(y, z), et tous les inférences de ce type. Prover9 reconnaît qu’il s’agit du
symbole d’égalité et ajoute ces assomptions automatiquement. Car le traitement de l’égalité n’est
pas optimal en utilisant la résolution seulement, on se sert aussi de la réglé de paramodulation,
que nous présentons ci-dessous.

C ∨ t1 = t2 D(t3 )
Paramodulation
(C ∨ D(t2 ))σ

où σ est un unificateur de t1 et t3 .
Dans notre exemple, nous avons que l’inférence de la clause 40,

c1 = agate ∨ c1 = maj ∨ c1 = charles Hait(c1, agate)

c1 = agate ∨ c1 = maj ∨ Hait(charles, agate)

est une instance de la règle de paramodulation.

92 / 92