Poly Inf402
Poly Inf402
Version abrégée
2022/2023
Ce document présente une version abrégée du cours de logique. Ainsi, la plupart des théorèmes sont
admis sans démonstration, et certaines notions sont omises.
Le polycopié complet peut être retrouvé sur
[Link]
Les références du document original ont été préservées, ce qui explique ici des « trous » dans la
numérotation.
Table des matières
I Logique propositionnelle 9
1 Logique propositionnelle 11
1.1 Syntaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.1.1 Formules strictes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.1.2 Formules à priorité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.2 Sens des formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.2.1 Sens des connecteurs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.2.2 Valeur d’une formule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.2.3 Définitions et notions élémentaires de logique . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.2.5 Équivalences remarquables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
1.3 Substitution et remplacement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
1.3.1 Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
1.3.2 Remplacement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
1.4 Formes Normales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
1.4.1 Transformation en forme normale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
1.4.2 Transformation en forme normale disjonctive (somme de monômes) . . . . . . . . . . . . . . . . 23
1.4.3 Transformation en forme normale conjonctive (produit de clauses) . . . . . . . . . . . . . . . . . 24
1.5 Algèbre de Boole . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
1.5.1 Définition et notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
1.5.2 Propriétés . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
1.6 Fonctions booléennes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1.6.1 Fonctions booléennes et somme de monômes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1.6.2 Fonctions booléennes et produit de clauses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1.7 L’outil BDDC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1.8 Exercices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2 Résolution propositionnelle 37
2.1 Résolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
2.1.1 Définitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
2.1.2 Cohérence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
2.1.3 Complétude pour la réfutation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
2.1.4 Réduction d’un ensemble de clauses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
2.2 Stratégie complète . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
2.2.1 Algorithme de la stratégie complète . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
2.2.2 Arrêt de l’algorithme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
2.2.3 Le résultat de l’algorithme est équivalent à l’ensemble initial de clauses . . . . . . . . . . . . . . 45
2.3 Algorithme de Davis-Putnam-Logemann-Loveland . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
2.3.1 Suppression des clauses contenant des littéraux isolés . . . . . . . . . . . . . . . . . . . . . . . . 46
2.3.2 Résolution unitaire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
2.3.3 Suppression des clauses valides . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
2.3.4 L’algorithme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
2.3.5 Solveurs SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
[Link] Heuristique de branchement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
[Link] Ajout de clauses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
4/129 Table des matières
3 Déduction Naturelle 57
3.1 Système formel de la déduction naturelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
3.1.1 Règles de conjonction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
3.1.2 Règles de disjonction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
3.1.3 Règles de l’implication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
3.1.4 Deux règles spéciales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
3.1.5 Preuves en déduction naturelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
[Link] Brouillon de preuve . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
[Link] Contexte des lignes d’un brouillon de preuve . . . . . . . . . . . . . . . . . . . . . . . 60
[Link] Preuves . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
3.2 Tactiques de preuve . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
3.3 Cohérence de la déduction naturelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
3.4 Complétude de la déduction naturelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.5 Outils . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.5.1 Logiciel de construction automatique de preuves . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.5.2 Dessiner des arbres de preuves . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.6 Exercices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
Bibliographie 127
6/129 Table des matières
Introduction
L ES mathématiciens ont raisonné correctement durant des siècles sans connaître la logique formelle. La logique mo-
derne est née de l’ambition de formaliser (mécaniser) le raisonnement mathématique : ce projet a reçu une impulsion
décisive quand il est apparu que l’absence de formalisation pouvait conduire à des contradictions. Le développement
actuel de la logique continue avec
— le besoin de prouver la correction des programmes (particulièrement quand ces programmes sont utilisés dans des
domaines où la sécurité est en jeu)
— l’ambition de représenter en machine l’ensemble des connaissances mathématiques
Cependant la terminologie des mathématiciens est restée différente de celle des logiciens. Pour exprimer que p im-
plique q, le mathématicien dira par exemple :
p entraîne q
p est une condition suffisante de q
pour que q soit vrai, il suffit que p soit vrai
q est une condition nécessaire de p
pour que p soit vrai, il faut que q soit vrai
Nous restreindrons notre étude à la logique classique (par opposition à la logique intuitionniste). La logique classique
est la logique à deux valeurs de vérité. De plus cette logique est celle des circuits combinatoires, ce qui explique sa grande
importance pratique.
Plan : Nous présentons dans la première partie la logique propositionnelle. Plus précisément dans un premier chapitre
nous donnons les définitions et résultats de base de la logique des prédicats. Dans le second chapitre nous parlons de la
résolution propositionnelle en introduisant la résolution binaire, la stratégie complète et l’algorithme DPLL. Enfin nous
illustrons une méthode de raisonnement logique en présentant la déduction naturelle. Dans le seconde partie du cours
nous revisitons l’ensemble des notions, résultats et techniques présentés dans la première partie pour la logique du premier
ordre.
Exercices : Nous proposons à la fin de chaque chapitre une série d’exercices portant sur le contenu du chapitre. Nous
indiquons par des étoiles la difficulté des exercices proposés, plus il y a d’étoiles plus l’exercice est difficile. Nous indi-
quons par les exercices qui complètent les preuves vues durant le cours. Les exercices proposés sont de trois catégories.
Nous avons des exercices :
— Basiques qui aident l’étudiant à se familiariser avec le vocabulaire et à manipuler les notions introduites en cours.
— Techniques qui sont des applications directes ou immédiates des résultats vus en cours.
— Réflexifs qui permettent à l’apprenant à raisonner, démontrer, prouver des résultats à partir des techniques et
notions apprises grâce aux deux autres types d’exercices.
Objectifs : Les compétences et connaissances que nous souhaitons transmettre sont les suivantes :
— Comprendre un raisonnement : être capable de déterminer si un raisonnement logique est correct ou non.
— Raisonner, c’est-à-dire, construire un raisonnement correct utilisant les outils de la logique propositionnelle et du
premier ordre.
— Modéliser et formaliser un problème.
— Écrire une preuve rigoureuse.
8/129 Table des matières
Première partie
Logique propositionnelle
Chapitre 1
Logique propositionnelle
Sommaire
1.1 Syntaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.1.1 Formules strictes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.1.2 Formules à priorité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.2 Sens des formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.2.1 Sens des connecteurs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.2.2 Valeur d’une formule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.2.3 Définitions et notions élémentaires de logique . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.2.5 Équivalences remarquables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
1.3 Substitution et remplacement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
1.3.1 Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
1.3.2 Remplacement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
1.4 Formes Normales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
1.4.1 Transformation en forme normale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
1.4.2 Transformation en forme normale disjonctive (somme de monômes) . . . . . . . . . . . . . . . . 23
1.4.3 Transformation en forme normale conjonctive (produit de clauses) . . . . . . . . . . . . . . . . . 24
1.5 Algèbre de Boole . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
1.5.1 Définition et notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
1.5.2 Propriétés . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
1.6 Fonctions booléennes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1.6.1 Fonctions booléennes et somme de monômes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1.6.2 Fonctions booléennes et produit de clauses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1.7 L’outil BDDC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1.8 Exercices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
A RISTOTE fut un des premiers à essayer de formaliser le raisonnement en utilisant la logique des syllogismes. La lo-
gique sert à préciser ce qu’est un raisonnement correct, indépendamment du domaine d’application. Un raisonnement
est un moyen d’obtenir une conclusion à partir d’hypothèses données. Un raisonnement correct ne dit rien sur la vérité des
hypothèses, il dit seulement qu’à partir de la vérité des hypothèses, nous pouvons déduire la vérité de la conclusion. Nous
commençons l’étude de la logique par les lois de la logique propositionnelle. La logique propositionnelle est la logique
sans quantificateurs qui s’intéresse uniquement aux lois gouvernant les opérations logiques suivantes : la négation (¬) , la
conjonction, autrement dit le « et » (∧), la disjonction, autrement dit le « ou » (∨), l’implication (⇒) et l’équivalence (⇔).
Ces opérations sont également appelées connecteurs. La logique propositionnelle permet de construire des raisonnements
à partir de ces connecteurs. Considérons l’exemple suivant qui comporte trois hypothèses :
1. si Pierre est grand, alors Jean n’est pas le fils de Pierre,
2. si Pierre n’est pas grand, alors Jean est le fils de Pierre,
3. si Jean est le fils de Pierre alors Marie est la sœur de Jean.
12/129 Chapitre 1. Logique propositionnelle
Nous concluons que Marie est la sœur de Jean ou Pierre est grand.
Afin de pouvoir raisonner nous extrayons la structure logique des hypothèses. Nous désignons les phrases « Pierre est
grand », « Jean est le fils de Pierre », « Marie est la sœur de Jean » respectivement par les lettres p, j, m. Les hypothèses
peuvent donc s’écrire :
1. p ⇒ ¬ j,
2. ¬p ⇒ j,
3. j ⇒ m,
et la conclusion se formalise en m ∨ p. Nous montrons alors que les hypothèses impliquent la conclusion indépendamment
de la nature des énoncés p, j, m. Pour cela nous prouvons que la formule suivante est vraie quelle que soit la vérité des
propositions p, j, m.
((p ⇒ ¬ j) ∧ (¬p ⇒ j) ∧ ( j ⇒ m)) ⇒ (m ∨ p).
Plan : Nous débutons ce chapitre par la syntaxe des formules logiques, c’est-à-dire, les règles permettant d’écrire des
formules. Une formule peut être vraie ou fausse, ainsi nous devons être capable d’évaluer le sens d’une formule. Pour cela
nous introduisons le sens de chaque connecteur ainsi que le calcul de la valeur d’une formule qui en dérive. Nous montrons
alors un résultat de compacité qui sera principalement utilisé dans la seconde partie de ce livre. Ensuite nous présentons des
équivalences remarquables utiles pour simplifier les raisonnements logiques. D’autres méthodes permettent de simplifier
les raisonnements logiques, par exemple le remplacement et la substitution de formule. Nous montrons ensuite comment
construire les formes normales conjonctives ou disjonctives d’une formule en utilisant les équivalences remarquables.
Ces formes normales permettent d’exhiber facilement les modèles ou les contre-modèles d’une formule. Nous montrons
ensuite que la logique propositionnelle est une instance d’une algèbre de Boole. Nous introduisons la notion de fonctions
booléennes. Enfin, nous présentons succinctement l’outil BDDC 1 développé par Pascal Raymond. Cet outil permet de
manipuler les formules propositionnelles.
1.1 Syntaxe
Avant de raisonner, nous définissons le langage que nous utilisons. Ce langage est celui des formules construites à
partir du vocabulaire suivant :
— Les constantes : > et ⊥ représentant respectivement le vrai et le faux.
— Les variables : une variable est un identificateur, avec ou sans indice, par exemple x, y1 .
— Les parenthèses : ouvrante ( et fermante ).
— Les connecteurs : ¬, ∨, ∧, ⇒, ⇔ respectivement appelés négation, disjonction (ou), conjonction (et), implication
et équivalence.
La syntaxe définit les règles de construction d’une formule de la logique propositionnelle. Nous introduisons deux modes
d’écriture d’une formule, l’un strict, l’autre plus souple dans le sens qu’il autorise plusieurs écritures d’une même formule.
Cette souplesse est obtenue grâce à l’introduction de priorités entre les connecteurs logiques.
Définition 1.1.1 (Formule stricte) Une formule stricte est définie de manière inductive comme suit :
— > et ⊥ sont des formules strictes.
— Une variable est une formule stricte.
— Si A est une formule stricte alors ¬A est une formule stricte.
— Si A et B sont des formules strictes et si ◦ est une des opérations ∨, ∧, ⇒, ⇔ alors (A ◦ B) est une formule stricte.
Dans la suite, nous désignons par ◦ tout connecteur binaire, et nous appellons simplement formule une formule stricte.
Les formules différentes de >, ⊥ et des variables sont des formules décomposables.
Exemple 1.1.2 L’expression (a ∨ (¬b ∧ c)) est une formule stricte construite suivant les règles précédentes. En revanche,
a ∨ (¬b ∧ c) et (a ∨ (¬(b) ∧ c)) ne sont pas des formules au sens de la définition 1.1.1.
1. [Link]
1.1. Syntaxe 13/129
L’intérêt de la définition de formules strictes est que les parenthèses permettent de trouver sans ambiguïté la structure
des formules. Nous représentons la structure des formules par un arbre, où les feuilles contiennent les constantes ou les
variables et les nœuds les connecteurs logiques. Le nœud racine est le connecteur à appliquer en dernier.
Exemple 1.1.3 La structure de la formule (a ∨ (¬b ∧ c)) est mise en évidence par l’arbre suivant :
Une formule peut être vue comme une liste de symboles (connecteurs, parenthèses, variables, et constantes). Un
facteur d’une telle liste est une suite de symboles consécutifs dans la liste.
Définition 1.1.4 (Sous-formule) Nous appelons sous-formule d’une formule (stricte) A tout facteur de A qui est une
formule (stricte).
Nous montrons que les formules sont décomposables d’une façon unique en leurs sous-formules. Ce résultat, précisé
par le théorème 1.1.13, est évident sur les exemples. L’unicité de la décomposition implique que nous pouvons identifier
une formule et son arbre de décomposition. Ainsi, une sous-formule de la formule A pourra être identifiée comme un
sous-arbre de l’arbre représentant la formule A.
Afin de raisonner par induction sur la structure d’une formule, nous définissons la taille d’une formule. Nous remar-
quons que la taille d’une formule correspond au nombre de connecteurs qu’elle contient.
Définition 1.1.10 (Taille d’une formule) La taille d’une formule A, notée |A|, est définie inductivement par :
— |>| = 0 et |⊥| = 0.
— Si A est une variable alors |A| = 0.
— |¬A| = 1 + |A|.
— |(A ◦ B)| = |A| + |B| + 1.
La taille des formules définie dans la définition 1.1.10 est une mesure utile pour prouver par récurrence des propriétés sur
les formules.
Avec la définition de formules (strictes) nous écrivons de nombreuses parenthèses inutiles comme les parenthèses qui
entourent chaque formule. Nous introduisons maintenant plus de souplesse dans notre syntaxe en définissant des priorités.
14/129 Chapitre 1. Logique propositionnelle
Définition 1.1.14 (Formule à priorité) Une formule à priorité est définie inductivement par :
— > et ⊥ sont des formules à priorité,
— une variable est une formule à priorité,
— si A est une formule à priorité alors ¬A est une formule à priorité,
— si A et B sont des formules à priorité alors A ◦ B est une formule à priorité,
— si A est une formule à priorité alors (A) est une formule à priorité.
Exemple 1.1.15 Considérons la formule a ∨ ¬b ∧ c qui est une formule à priorité mais pas une formule.
En général, une formule à priorité n’est pas une formule (stricte). Nous montrons dans l’exercice 2 page 31 que toute
formule est une formule à priorité. Afin de pouvoir supprimer des parenthèses sans aucune ambiguïté nous définissons un
ordre de priorité entre les différents connecteurs.
Définition 1.1.16 (Ordre de priorité des connecteurs) La négation est prioritaire, puis dans l’ordre des priorités dé-
croissantes, nous trouvons la conjonction (∧), la disjonction (∨), l’implication (⇒) et l’équivalence (⇔).
À priorité égale, le connecteur gauche est prioritaire, sauf pour l’implication qui est associative à droite. 2
Nous considérons qu’une formule à priorité est l’abréviation de la formule reconstituable en utilisant les priorités. Sauf
exception, nous identifions une formule et son abréviation. Autrement dit, ce qui nous intéresse dans une formule, ce n’est
pas son écriture superficielle, c’est sa structure, qui est mise en évidence par la syntaxe « stricte ». Ainsi la taille d’une
formule à priorité sera égale à la taille de la formule stricte dont elle est l’abréviation. De même, pour les sous-formules,
nous considérerons toujours la formule stricte dont la formule à priorité est l’abréviation.
Exemple 1.1.17 Nous donnons plusieurs exemples d’abréviation de formule par une formule à priorité :
— a ∧ b ∧ c est l’abréviation de
— a ∧ b ∨ c est l’abréviation de
— a ∨ b ∧ c est l’abréviation de
Maintenant que la syntaxe est définie, nous définissons le sens des formules.
Définition 1.2.1 (Assignation) Une assignation est une application de l’ensemble de toutes les variables d’une formule
dans l’ensemble B.
Définition 1.2.2 (Valeur d’une formule) Soient A une formule et v une assignation, [A]v dénote la valeur de la formule
A dans l’assignation v. La valeur de [A]v est définie par récurrence sur l’ensemble des formules. Soient A, B des formules,
x une variable et v une assignation.
— [x]v = v(x).
— [>]v = 1, [⊥]v = 0.
— [¬A]v = 1 − [A]v autrement dit pour calculer la valeur de ¬A, nous soustrayons à 1 la valeur de A.
— [(A ∨ B)]v = max{[A]v , [B]v }.
— [(A ∧ B)]v = min{[A]v , [B]v }.
— [(A ⇒ B)]v = si [A]v = 0 alors 1 sinon [B]v .
— [(A ⇔ B)]v = si [A]v = [B]v alors 1 sinon 0.
D’après le théorème 1.1.13 page 13, toute formule (stricte) se décompose de façon unique en l’un des cas ci-dessus.
Ainsi l’extension de v aux formules est une application des formules dans B. En effet, soient 4 formules A, A0 , B, B0 et deux
opérations ◦ et ◦0 telles que (A ◦ B) = (A0 ◦0 B0 ). Par unicité de la décomposition, A = A0 , B = B0 , ◦ = ◦0 , donc la valeur de
la formule (A ◦ B) est définie uniquement par une et une seule des lignes de la définition de la valeur. Il est clair que la
valeur d’une formule ne dépend que de ses variables et de sa structure, aussi l’évaluation d’une formule est présentée sous
la forme d’une table de vérité.
Définition 1.2.3 (Table de vérité d’une formule) Une table de vérité d’une formule A est un tableau qui représente la
valeur de A pour toutes les valeurs possibles des variables de A.
Chaque ligne de la table de vérité définit une assignation pour les variables des formules présentes dans les colonnes de
la table et chaque colonne donne la valeur d’une formule.
Exemple 1.2.4 Nous donnons la table de vérité des formules suivantes : x ⇒ y, ¬x, ¬x ∨ y, (x ⇒ y) ⇔ (¬x ∨ y) et x ∨ ¬y.
x y x⇒y ¬x ¬x ∨ y (x ⇒ y) ⇔ (¬x ∨ y) x ∨ ¬y
0 0
0 1
1 0
1 1
Définition 1.2.5 (Formules équivalentes) Deux formules A et B sont équivalentes si elles ont la même valeur pour toute
assignation.
16/129 Chapitre 1. Logique propositionnelle
Exemple 1.2.6 Les colonnes des deux formules x ⇒ y et ¬x ∨ y sont identiques dans l’exemple 1.2.4 page précédente.
Ces deux formules sont donc équivalentes. Par contre les formules x ⇒ y et x ∨ ¬y ne sont pas équivalentes car elles n’ont
pas les mêmes tables de vérité.
Remarque 1.2.7 Nous n’utilisons pas le symbole du connecteur logique ⇔ pour dire que A et B sont équivalentes. Nous
notons que les formules A et B sont équivalentes par A ≡ B ou simplement A = B si le contexte nous permet de comprendre
que le signe égal indique l’équivalence. Ainsi, x ⇒ y = ¬x ∨ y signifie que la formule x ⇒ y est équivalente à la formule
¬x ∨ y.
Définition 1.2.8 (Valide, tautologie) Une formule est valide si elle a la valeur 1 pour toute assignation. Une formule
valide est aussi appelée une tautologie.
Exemple 1.2.9 En regardant la table de vérité de l’exemple 1.2.4 page précédente nous obtenons que :
— la formule (x ⇒ y) ⇔ (¬x ∨ y) est valide ;
— la formule x ⇒ y n’est pas valide car
Notation : |= A dénote le fait que la formule A est valide. Nous pouvons écrire |= x ∨ ¬x, car x ∨ ¬x est une tautologie.
Propriété 1.2.10 Les formules A et B sont équivalentes si et seulement si la formule A ⇔ B est valide.
Preuve : La propriété est une conséquence de la table 1.1 page précédente et des définitions précédentes.
⇒ Si les formules A et B sont équivalentes cela signifie qu’elles ont la même table de vérité, ainsi d’après la définition
du connecteur ⇔ donnée dans la table 1.1 page précédente la table de vérité de A ⇔ B contient uniquement des 1
donc A ⇔ B est valide.
⇐ Si la formule A ⇔ B est valide, nous déduisons que la table de vérité de A ⇔ B contient uniquement des 1, ainsi
d’après la définition du connecteur ⇔ donnée dans la table 1.1 page précédente les tables de vérité de A et de B
coïncident donc les formules A et B sont équivalentes.
2
Définition 1.2.11 (Modèle d’une formule) Une assignation v qui donne la valeur 1 à une formule est un modèle de la
formule. Nous dirons aussi que v satisfait la formule ou que v rend vraie la formule.
Définition 1.2.13 (Modèle d’un ensemble de formules) Une assignation est un modèle d’un ensemble de formules si et
seulement si elle est un modèle de chaque formule de l’ensemble.
Exemple 1.2.14
Propriété 1.2.15 Une assignation est un modèle d’un ensemble de formules si et seulement si elle est un modèle de la
conjonction des formules de l’ensemble.
Définition 1.2.17 (Contre-Modèle) Une assignation v qui donne la valeur 0 à une formule est un contre-modèle de la
formule. Nous dirons que v ne satisfait pas la formule ou v rend la formule fausse.
Remarque 1.2.19 (Contre-modèle d’un ensemble de formules) La notion de contre-modèle s’étend aux ensembles de
formules de la même manière que la notion de modèle.
Définition 1.2.20 (Formule satisfaisable) Une formule (respectivement un ensemble de formules) est satisfaisable s’il
existe une assignation qui en est un modèle.
Définition 1.2.21 (Formule insatisfaisable) Une formule (respectivement un ensemble de formules) est insatisfaisable si
elle (respectivement s’il) n’est pas satisfaisable.
Une formule (respectivement un ensemble de formules) insatisfaisable ne possède pas de modèle. Sa table de vérité
ne comporte que des 0. La négation d’une tautologie est donc une formule insatisfaisable.
Exemple 1.2.22
Remarque 1.2.23 Les logiciens utilisent le mot consistant comme synonyme de satisfaisable et contradictoire comme
synonyme d’insatisfaisable.
Définition 1.2.24 (Conséquence) Soient Γ un ensemble de formules et A une formule : A est conséquence de l’ensemble
Γ d’hypothèses si tout modèle de Γ est modèle de A. Le fait que A soit conséquence de Γ est noté par Γ |= A.
Exemple 1.2.25 D’après la table de vérité suivante, la formule a ⇒ c est conséquence des hypothèses a ⇒ b et b ⇒ c.
Remarque 1.2.26 (Validité et conséquence) Nous notons A est valide par |= A, car A est valide si et seulement si A est
conséquence de l’ensemble vide.
Maintenant, nous établissons l’équivalence de la validité d’une formule composée d’hypothèses et d’une conclusion
avec la conséquence de la conclusion à partir des hypothèses mais aussi avec l’insatifaisabilité des hypothèses et de la
négation de la conclusion. Ces relations sont constamment utilisées dans les exercices et les démonstrations.
Propriété 1.2.27 Soient n + 1 formules A1 , . . . , An , B. Soit Hn la conjonction des formules A1 , . . . , An . Les trois formula-
tions suivantes sont équivalentes :
1. A1 , . . . , An |= B, c’est-à-dire B est conséquence des hypothèses A1 , . . . , An .
2. La formule Hn ⇒ B est valide.
18/129 Chapitre 1. Logique propositionnelle
3. Hn ∧ ¬B est insatisfaisable.
Preuve : La propriété est une conséquence de la table 1.1 page 15 et des définitions précédentes. Soient n + 1 formules
A1 , . . . An , B et Hn = A1 ∧ . . . ∧ An .
1 ⇒ 2 : Supposons que A1 , . . . , An |= B, c’est-à-dire tout modèle de A1 , . . . , An est aussi modèle de B.
Nous obtenons donc dans tous les cas que Hn ⇒ B est valide.
2 ⇒ 3 : Supposons que Hn ⇒ B est valide, cela signifie que pour toute assignation v, [Hn ⇒ B]v = 1. D’après la
table 1.1 page 15 nous avons deux possibilités soit [Hn ]v = 0, soit [Hn ]v = 1 et [B]v = 1. Or [Hn ∧ ¬B]v =
min([Hn ]v , [¬B]v ) = min([Hn ]v , 1 − [B]v ). Dans les deux cas, nous obtenons [Hn ∧ ¬B]v = 0. Nous concluons donc
que Hn ∧ ¬B est insatisfaisable.
3 ⇒ 1 : Supposons que Hn ∧ ¬B est insatisfaisable, c’est-à-dire que pour toute assignation la formule Hn ∧ ¬B est
contradictoire. Montrons que les modèles de A1 , . . . , An sont aussi des modèles de B.
Soit v une assignation modèle de A1 , . . . , An , il en découle que [Ai ]v = 1 pour i = 1, . . . , n donc [Hn ]v = [A1 ∧ . . . ∧
An ]v = 1. D’après notre hypothèse, nous en déduisons que [¬B]v = 0. D’où, 1−[B]v = 0. Nous avons donc [B]v = 1,
c’est-à-dire que v est aussi un modèle de B.
En utilisant le résultat de l’exercice 7 page 32 nous concluons. 2
Exemple 1.2.28 Nous considérons les deux formules a ⇒ b et b ⇒ c, nous illustrons le théorème précédent en prouvant
que a ⇒ b, b ⇒ c |= a ⇒ c, soit en montrant que (a ⇒ b) ∧ (b ⇒ c) ⇒ (a ⇒ c) est une tautologie, soit que (a ⇒ b) ∧ (b ⇒
c) ∧ ¬(a ⇒ c) est insatisfaisable. Pour cela nous donnons la table de vérité associée à ces formules.
— Commutative, c’est-à-dire, x ∧ y ≡ y ∧ x.
— 1 est l’élément neutre de la conjonction, c’est-à-dire, 1 ∧ x ≡ x.
3. La conjonction est distributive sur la disjonction : x ∧ (y ∨ z) ≡ (x ∧ y) ∨ (x ∧ z).
4. La disjonction est distributive sur la conjonction : x ∨ (y ∧ z) ≡ (x ∨ y) ∧ (x ∨ z).
5. Les lois de la négation :
— x ∧ ¬x ≡ 0.
— x ∨ ¬x ≡ 1 (Le tiers-exclus).
6. ¬¬x ≡ x.
7. ¬0 ≡ 1.
8. ¬1 ≡ 0.
9. Les lois de De Morgan :
— ¬(x ∧ y) ≡ ¬x ∨ ¬y.
— ¬(x ∨ y) ≡ ¬x ∧ ¬y.
10. 0 est l’élément absorbant de la conjonction : 0 ∧ x ≡ 0.
11. 1 est l’élément absorbant de la disjonction : 1 ∨ x ≡ 1.
12. idempotence de la disjonction : x ∨ x ≡ x.
13. idempotence de la conjonction : x ∧ x ≡ x.
Les équivalences 1 page ci-contre à 5 se démontrent à l’aide de tables de vérité 3 . Les équivalences 6 à 13 se déduisent
des équivalences 1 page ci-contre à 5, comme nous le montrons dans la section 1.5 page 24. Ci-dessous, nous donnons
quelques lois de simplification qui permettent d’alléger les raisonnements logiques.
Preuve : En utilisant les équivalences remarquables nous prouvons les trois lois de simplification. La preuve est demandée
dans l’exercice 12 page 33. 2
1.3.1 Substitution
Définition 1.3.1 (Substitution) Une substitution est une application de l’ensemble des variables dans l’ensemble des
formules. L’application d’une substitution σ à une formule consiste à remplacer dans la formule toute variable x par la
formule σ(x).
Notation : Soit A une formule, nous notons Aσ ou σ(A) l’application de la substitution σ à la formule A.
Définition 1.3.2 (Support d’une substitution, substitution à support fini) Le support d’une substitution σ est l’ensemble
des variables x telles que xσ 6= x. Une substitution σ à support fini est notée < x1 := A1 , . . . , xn := An >, où A1 , . . . , An sont
des formules, x1 , . . . , xn sont des variables distinctes et la substitution vérifie :
— pour i de 1 à n, xi σ = Ai
— pour toute variable y telle que y 6∈ {x1 , . . . , xn }, nous avons : yσ = y
3. Nous laissons le soin au lecteur de se convaincre de la véracité de ces équivalences en construisant les tables correspondantes.
20/129 Chapitre 1. Logique propositionnelle
Induction :
Supposons que la propriété soit vraie pour toute formule de taille inférieure ou égale à n, montrons qu’elle est
vraie pour une formule A de taille n + 1 :
Exemple 1.3.5 Soit A = x ∨ y ∨ d une formule. Soit σ =< x := a ∨ b, y := b ∧ c > une substitution. Soit v une assignation
telle que v(a) = 1, v(b) = 0, v(c) = 0, v(d) = 0. Nous avons :
Théorème 1.3.6 L’application d’une substitution à une formule valide donne une formule valide.
Preuve : Soient A une formule valide, σ une substitution et v une assignation quelconque. D’après la propriété 1.3.4 :
[Aσ]v = [A]w où pour toute variable x, w(x) = [σ(x)]v . Puisque A est valide, [A]w = 1. Par suite Aσ vaut 1 dans toute
assignation, c’est donc une formule valide. 2
Exemple 1.3.7 Soit A la formule ¬(p ∧ q) ⇔ (¬p ∨ ¬q). Cette formule est valide, c’est une équivalence remarquable.
Soit σ la substitution suivante : < p := (a ∨ b), q := (c ∧ d) >. La formule
1.3. Substitution et remplacement 21/129
La substitution est définie sur les formules, pour l’appliquer sans erreur aux formules à priorité, il suffit que l’image,
par la substitution, de toute variable soit une variable, une constante ou une formule entre parenthèses.
1.3.2 Remplacement
La notion de substitution ne nous permet pas de remplacer une formule par une formule, nous introduisons la notion
de remplacement à cette fin.
Définition 1.3.8 (Remplacement) Soient A, B,C, D des formules. La formule D est obtenue en remplaçant dans C cer-
taines occurrences de A par B, s’il existe une formule E et une variable x telles que, C = E < x := A > et D = E < x := B >.
Exemple 1.3.9 Considérons la formule C = ((a ⇒ b) ∨ ¬(a ⇒ b)).
— La formule obtenue en remplaçant toutes les occurrences de (a ⇒ b) par (a ∧ b) dans C est
elle est obtenue en considérant la formule E = (x ∨ ¬x) et les substitutions < x := (a ∧ b) > et < x := (a ⇒ b) >.
— La formule obtenue en remplaçant la première occurrence de (a ⇒ b) par (a ∧ b) dans C est
elle est obtenue en considérant la formule E = (x ∨ ¬(a ⇒ b)) et les substitutions < x := (a ∧ b) > et < x := (a ⇒
b) >.
La différence entre une substitution et un remplacement est qu’une substitution remplace un ensemble de variables par
des formules alors qu’un remplacement remplace les occurrences de certaines formules par une autre formule en utilisant
des substitutions.
Théorème 1.3.10 Soient C une formule et D la formule obtenue en remplaçant, dans C, des occurrences de la formule A
par la formule B, alors (A ⇔ B) |= (C ⇔ D).
Preuve : Par définition du remplacement, il existe une formule E et une variable x telles que, C = E < x := A > et
D = E < x := B >. Supposons que v est une assignation modèle de (A ⇔ B). Nous avons donc [A]v = [B]v . D’après la
propriété 1.3.4 page ci-contre :
— [C]v = [E]w où w est identique à v sauf que w(x) = [A]v
— [D]v = [E]w0 où w0 est identique à v sauf que w0 (x) = [B]v
Puisque [A]v = [B]v , les assignations w et w0 sont identiques, donc [C]v = [D]v . Par suite v est modèle de (C ⇔ D). 2
Corollaire 1.3.11 Soient C une formule et D la formule obtenue en remplaçant, dans C, une occurrence de la formule A
par la formule B, alors A ≡ B implique C ≡ D.
Preuve : Si A ≡ B, alors la formule (A ⇔ B) est valide (propriété 1.2.10), donc la formule (C ⇔ D) également puisqu’elle
est, d’après le théorème ci-dessus, la conséquence de (A ⇔ B), par suite C ≡ D. 2
Exemple 1.3.12 Le remplacement d’une occurrence d’une formule A par une occurrence de B est mis en évidence par
des boîtes marquant ces occurrences.
— D’après théorème 1.3.10 : p ⇔ q |= (p ∨ ( p ⇒ r)) ⇔ (p ∨ ( q ⇒ r)).
— D’après le corollaire 1.3.11 : (¬(p ∨ q) ⇒ ( ¬(p ∨ q) ∨ r)) ≡ (¬(p ∨ q) ⇒ ( (¬p ∧ ¬q) ∨ r)), puisque ¬(p ∨ q) ≡
(¬p ∧ ¬q).
Remarque 1.3.13 Le théorème précédent et son corollaire s’appliquent aux formules. Quand nous faisons un rempla-
cement directement sur une formule à priorité, nous devons nous assurer que ce remplacement reste correct sur les
formules (strictes) sous peine de commettre des erreurs. Par exemple, considérons les deux équivalences a ∧ b ≡ a ∧ b
et ¬c ⇒ d ≡ c ∨ d. Remplaçons b à gauche par ¬c ⇒ d et à droite par c ∨ d. Nous observons que bien que ¬c ⇒ d ≡ c ∨ d,
a ∧ ¬c ⇒ d 6≡ a ∧ c ∨ d, car pour a = c = d = 0, la formule de gauche vaut 1 et celle de droite vaut 0. Ici le corollaire
ne doit pas être appliqué à l’occurrence encadrée car a ∧ ¬c ⇒ d est une abréviation de ((a ∧ ¬c) ⇒ d), donc ¬c ⇒ d
n’apparaît pas comme une occurrence possible de a ∧ ¬c ⇒ d.
Nous avons défini les remplacements à partir des substitutions, nous allons maintenant appliquer les remplacements à
une formule afin de la transformer en une formule en forme normale équivalente.
22/129 Chapitre 1. Logique propositionnelle
En partant d’une forme normale et en distribuant toutes les conjonctions sur les disjonctions, nous obtenons une
disjonction de monômes. Pour cela il faut aussi savoir regrouper plusieurs applications de la distributivité.
Exemple 1.4.8 Dans une transformation en disjonction de monômes, nous pouvons appliquer de gauche à droite l’équi-
valence (a ∨ b) ∧ (c ∨ d ∨ e) ≡
La transformation par équivalence d’une formule en une disjonction de monômes peut être utilisée pour déterminer si
une formule est valide ou non. Soit A une formule dont nous souhaitons déterminer la validité : Nous transformons ¬A en
une disjonction de monômes équivalente à ¬A. Si ¬A = 0 alors A = 1 donc A est valide, sinon, toutes simplifications étant
faites, ¬A est égal à une disjonction de monômes non nuls, qui nous donnent des modèles de ¬A, donc des contre-modèles
de A.
Exemple 1.4.9 Soit A = (p ⇒ (q ⇒ r)) ⇒ (p ∧ q ⇒ r). Déterminons si A est valide par transformation de ¬A en disjonc-
tion de monômes.
Exemple 1.4.10 Soit A = ((a ⇒ b) ∧ c) ∨ (a ∧ d). Déterminer si A est valide par transformation de ¬A en disjonction de
monômes.
¬A
≡ ¬((a ⇒ b) ∧ c) ∧ ¬(a ∧ d) par déplacement des négations
≡ (¬(a ⇒ b) ∨ ¬c) ∧ (¬a ∨ ¬d) par déplacement des négations
≡ (a ∧ ¬b ∨ ¬c) ∧ (¬a ∨ ¬d) par combinaison du déplacement d’une négation
et élimination de l’implication
≡ (a ∧ ¬b ∧ ¬a) ∨ (a ∧ ¬b ∧ ¬d) ∨ (¬c ∧ ¬a) ∨ (¬c ∧ ¬d) par distributivité de la disjonction sur la conjonction
≡ (a ∧ ¬b ∧ ¬d) ∨ (¬c ∧ ¬a) ∨ (¬c ∧ ¬d) par simplification
Nous obtenons 3 modèles de ¬A (a = 1, b = 0, d = 0 ; a = 0, c = 0 ; c = 0, d = 0), c’est-à-dire, des contre-modèles de
A. Donc A n’est pas valide.
24/129 Chapitre 1. Logique propositionnelle
Définition 1.4.11 (Forme normale conjonctive) Une formule est une forme normale conjonctive (en bref fnc) si et seule-
ment si elle est une conjonction (produit) de clauses.
L’intérêt des formes normales conjonctives est de mettre en évidence des contre-modèles.
Par convention, nous considérons que 0 et 1 sont des disjonctions de monômes et des conjonctions de clauses. Nous
appliquons la distributivité (inhabituelle) de la disjonction sur la conjonction, autrement dit nous remplaçons toute sous-
formule A ∨ (B ∧C) par (A ∨ B) ∧ (A ∨C), et toute sous-formule (B ∧C) ∨ A par (B ∨ A) ∧ (C ∨ A).
La transformation par équivalence d’une formule en une conjonction de clauses de littéraux peut aussi être utilisée
pour déterminer si une formule est valide ou non. Soit A une formule dont nous souhaitons déterminer la validité : Nous
transformons A en une conjonction de clauses équivalente à A. Si A = 1 alors A est valide, sinon, toutes simplifications
étant faites, A est égale à une conjonction de clauses non égales à 1, et chacune de ces disjonctions nous donne un contre-
modèle de A.
Définition 1.5.1 Une algèbre de Boole est un ensemble d’au moins deux éléments, 0, 1, et trois opérations, complément
(le complément de x est noté x), somme (+) et produit (.), qui vérifient les axiomes suivants :
1. la somme est :
— associative : x + (y + z) = (x + y) + z,
— commutative : x + y = y + x,
— 0 est élément neutre de la somme : 0 + x = x,
2. le produit est :
— associatif : x.(y.z) = (x.y).z,
— commutatif : x.y = y.x,
— 1 est élément neutre du produit : 1.x = x,
3. le produit est distributif sur la somme : x.(y + z) = (x.y) + (x.z),
4. la somme est distributive sur le produit : x + (y.z) = (x + y).(x + z),
5. les lois de la négation :
— x + x = 1,
— x.x = 0.
1.5. Algèbre de Boole 25/129
Attention, le fait que la distributivité de la somme sur le produit n’est pas usuelle rend son application propice aux
erreurs.
Comme indiqué précédemment dans la sous-section 1.2.5 page 18, nous pouvons prouver en utilisant des tables
de vérité que la logique propositionnelle vérifie l’ensemble des axiomes d’une algèbre de Boole. Ainsi nous pouvons
considérer la logique propositionnelle comme la plus petite algèbre de Boole, car elle contient deux éléments. De ce fait,
nous pouvons utiliser les notations booléennes (plus condensées) en lieu et place des notations propositionnelles, comme
indiqué dans la table de correspondance donnée dans la figure 1.1. Nous conseillons de les utiliser pour effectuer de gros
calculs. Par ailleurs, observez que ces notations sont fréquemment utilisées dans le domaine du matériel.
Il est important de noter que la logique propositionnelle n’est pas l’unique algèbre de Boole. Par exemple, l’ensemble
P (X) des sous-ensembles d’un ensemble X est une algèbre de Boole, comme nous l’indique la mise en correspondance
des opérateurs ensemblistes avec leur désignation dans l’algèbre de Boole dans la figure 1.2.
Puisque les lois de simplification sont déduites des lois de l’algèbre de Boole, comme nous allons le montrer dans la
suite, elles sont vérifiées dans toute algèbre de Boole. En particulier dans l’algèbre de Boole P (X) nous avons A∪(A∩B) =
A. Une preuve dans l’algèbre de Boole est une suite d’égalités, permettant de passer d’une formule à une autre formule
équivalente en utilisant les axiomes ou simplifications de l’algèbre de Boole.
1.5.2 Propriétés
Nous présentons certaines des propriétés qui découlent de la définition de l’algèbre de Boole et qui sont couramment
utilisées dans les raisonnements. Pour raccourcir les preuves de ces propriétés, nous utilisons implicitement l’associativité
et la commutativité de la somme et du produit.
Propriété 1.5.3 Dans une algèbre de Boole, pour tout x, il y a un et un seul y tel que x + y = 1 et xy = 0, autrement dit la
négation est unique.
26/129 Chapitre 1. Logique propositionnelle
Preuve : Il y a un élément y vérifiant x + y = 1 et xy = 0, c’est x d’après les axiomes de l’algèbre de Boole. Montrons
qu’il est unique. Raisonnons par contradiction, supposons qu’il n’est pas unique, nous avons donc qu’il existe y et z deux
éléments distincts tels que x + y = 1, xy = 0, x + z = 1, et xz = 0. Nous considérons u = xy + z. Puisque xy = 0, nous
avons : u = z. Par distributivité de la somme sur le produit, nous avons : u = (x + z)(y + z). Puisque x + z = 1 et que 1
est l’élément neutre du produit, nous avons : u = y + z. Nous concluons donc que z = y + z. En considérant v = xz + y et
échangeant les rôles de y et z, nous obtenons de façon analogue y = y + z. Par suite y = z, ce qui prouve donc l’unicité de
la négation. 2
Propriété 1.5.4 Dans une algèbre de Boole, les équivalences suivantes sont vraies pour tout x et tout y :
1. 1 = 0.
2. 0 = 1.
3. x = x.
4. Idempotence du produit : x.x = x.
5. Idempotence de la somme : x + x = x.
6. 1 est élément absorbant de la somme : 1 + x = 1.
7. 0 est élément absorbant du produit : 0.x = 0.
8. Lois de De Morgan :
— xy = x + y.
— x + y = x.y.
Preuve :
1. 1 = 0.
2. 0 = 1.
3. x = x.
5. Idempotence de la somme : x + x = x.
8. Lois de De Morgan :
— x.y = x + y :
28/129 Chapitre 1. Logique propositionnelle
— x + y = x.y.
2
1.6. Fonctions booléennes 29/129
Définition 1.6.1 (Fonction booléenne) Une fonction booléenne f est une fonction dont les arguments et le résultat sont
dans le domaine B = {0, 1}.
f : Bn → B
Théorème 1.6.3 Soit f une fonction booléenne à n arguments. Cette fonction est représentée à l’aide de n variables
x1 , . . . , xn . Soit A la formule suivante :
A= ∑ x1a1 . . . xnan .
f (a1 ,...,an )=1
Les ai sont des valeurs booléennes et A est la somme des monômes x1a1 . . . xnan tels que f (a1 , . . . , an ) = 1. Par convention,
si la fonction f vaut toujours 0 alors A = 0.
Pour toute assignation v telle que v(x1 ) = a1 , . . . , v(xn ) = an , nous avons f (a1 , . . . , an ) = [A]v . En omettant la distinc-
tion entre une variable et sa valeur, ce résultat s’écrit plus brièvement : f (x1 , . . . xn ) = A.
Exemple 1.6.4 La fonction ma j à 3 arguments vaut 1 lorsqu’au moins 2 de ses arguments valent 1. Nous donnons la
table représentant cette fonction :
x1 x2 x3 ma j(x1 , x2 , x3 )
0 0 0 0 0 0 0 0 0
0 0 1 0 0 0 0 0 0
0 1 0 0 0 0 0 0 0
0 1 1 1 1 0 0 0 1
1 0 0 0 0 0 0 0 0
1 0 1 1 0 1 0 0 1
1 1 0 1 0 0 1 0 1
1 1 1 1 0 0 0 1 1
Nous notons sur la table de vérité, que chaque monôme ne vaut 1 que sur une ligne de la table et que la somme des
monômes est équivalente à ma j(x1 , x2 , x3 ). La fonction ma j peut donc s’exprimer par
Théorème 1.6.5 Soit f une fonction booléenne à n arguments. Cette fonction est représentée à l’aide de n variables
x1 , . . . , xn . Soit A la formule suivante :
A= ∏ x1a1 + . . . + xnan .
f (a1 ,...,an )=0
Les ai sont des valeurs booléennes et A est le produit des clauses x1a1 +. . .+xnan telles que f (a1 , . . . , an ) = 0. Par convention
si la fonction f vaut toujours 1 alors A = 1.
Pour toute assignation v telle que v(x1 ) = a1 , . . . , v(xn ) = an , nous avons f (a1 , . . . , an ) = [A]v . En omettant la distinc-
tion entre une variable et sa valeur, ce résultat s’écrit plus brièvement : f (x1 , . . . , xn ) = A.
Exemple 1.6.6 Nous représentons la fonction ma j définie dans l’exemple 1.6.4 page précédente par un produit de
clauses :
x1 x2 x3 ma j(x1 , x2 , x3 )
0 0 0 0 0 1 1 1 0
0 0 1 0 1 0 1 1 0
0 1 0 0 1 1 0 1 0
0 1 1 1 1 1 1 1 1
1 0 0 0 1 1 1 0 0
1 0 1 1 1 1 1 1 1
1 1 0 1 1 1 1 1 1
1 1 1 1 1 1 1 1 1
[Link]
Cet outil est une « calculette propositionnelle » basée sur les diagrammes de décision binaires. Ces diagrammes permettent
d’avoir une représentation interne des formules logiques sous la forme d’un graphe orienté acyclique ayant pour propriété
d’être canonique. Cette calculette offre notamment la possibilité :
— d’évaluer si une formule est une tautologie,
— d’évaluer si une formule a un modèle,
— de transformer une formule en forme normale conjonctive,
— de transformer une formule en forme normale disjonctive,
— ...
Ainsi, il est possible d’utiliser BDDC pour résoudre plusieurs des exercices proposés ci-après, parmi lesquels les exercices
8 page 32 à 16 page 33 et 23 page 34 à 24 page 34.
1.8. Exercices 31/129
1.8 Exercices
Exercice 1 (Formules strictes, formules à priorité) Parmi les expressions suivantes, indiquer celles qui sont et celles
qui ne sont pas des formules, au sens de la syntaxe stricte décrite dans la définition 1.1.1 page 12 :
1. x
2. (x
3. (x)
4. (x ⇒ (y ∧ z)
5. (x ⇒ (y ∧ z))
6. ¬(x ∨ y)
7. (¬(x ∨ y))
8. ¬(x ⇒ y) ∨ ¬(y ∧ z)
9. ¬(x)
10. (¬((x ∨ y) ∧ z) ⇔ (u ⇒ v)))
Exercice 2 (Formules et priorités) Montrer que toute formule stricte est une formule à priorité.
Exercice 3 (Formules et priorités) L’arbre suivant représente la structure de la formule ((p ∧ ¬(p ∨ q)) ∧ ¬r).
~
∧ ¬
p ¬ r
∨
p q
En utilisant les priorités, elle peut s’écrire avec le moins de parenthèses possibles sous l’une des formes : p∧¬(p∨q)∧¬r
avec les notations logiques, p.p + q.r avec les notations booléennes. Comme sur cet exemple, pour chacune des formules
suivantes, indiquer sa structure sous forme d’arbre, sa forme la moins parenthésée avec les opérations logiques, sa forme
la moins parenthésée avec les opérations booléennes :
1. (¬(a ∧ b) ⇔ (¬a ∨ ¬b)).
2. ((¬a ∨ b) ∧ (¬b ∨ a)).
3. (((a ∧ b) ∧ c) ∨ ((¬a ∧ ¬b) ∧ ¬c)).
4. (p ⇒ (q ⇒ r)).
5. ((p ⇒ q) ⇒ r).
Exercice 4 (Formules et priorités) Indiquer sous forme d’arbres, les structures des formules à priorité suivantes :
1. p ⇔ ¬q ∨ r.
2. p ∨ q ⇒ r ∧ s.
3. p ∨ q ⇒ r ⇔ s.
4. p ∨ q ∧ r ⇒ ¬s.
5. p ⇒ r ∧ s ⇒ t.
32/129 Chapitre 1. Logique propositionnelle
6. p ∨ q ∧ s ∨ t.
7. p ∧ q ⇔ ¬r ∨ s.
8. ¬p ∧ q ∨ r ⇒ s ⇔ t.
Exercice 7 (Raisonnement circulaire) Donner les tables de vérité des formules suivantes : a ⇒ b, b ⇒ c, c ⇒ a,
a ⇔ b, b ⇔ c et c ⇔ a. Conclure que (a ⇒ b) ∧ (b ⇒ c) ∧ (c ⇒ a) ≡ (a ⇔ b) ∧ (b ⇔ c) ∧ (c ⇔ a).
Exercice 10 (Équivalence) Parmi les formules suivantes, indiquer celles qui sont équivalentes à p ⇒ q ∨ r ?
1. q ∧ ¬r ⇒ p.
2. p ∧ ¬r ⇒ q.
3. ¬q ∧ ¬r ⇒ ¬p.
4. q ∨ ¬p ∨ r.
1.8. Exercices 33/129
Exercice 11 (Modèle d’un ensemble de formules,*) Montrer qu’une assignation est un modèle d’un ensemble de
formules, si et seulement si elle est un modèle de la conjonction des formules de l’ensemble.
Exercice 13 (Simplification de formule,*) Montrer par simplification que la formule suivante est une tautologie.
(a ∨ b) ∧ (¬b ∨ c) ⇒ (a ∨ c)
Exercice 15 (Récurrence,*) Montrer que toute formule construite avec une seule variable, uniquement les connec-
teurs binaires ∨ et ∧ et sans négation est équivalente à une formule de taille 0.
Exercice 16 (Algèbre de Boole) À l’aide de tables de vérité, indiquer pour les opérations suivantes ⇒, ⇔ si elles sont
commutatives, associatives, idempotentes, transitives.
Exercice 17 (Algèbre de Boole) Montrer qu’une formule avec une seule variable, notée p, est équivalente à l’une des
formules, 0, 1, p, ¬p.
Exercice 18 (Algèbre de Boole) Donner 16 formules telles que toute formule avec deux variables, notées p et q, soit
équivalente à l’une des 16 formules.
Exercice 20 (Conséquence) Au cours de l’enquête dont il est chargé, l’adjudant Tifrice effectue le raisonnement suivant :
— Si le meurtre a eu lieu le jour, le meurtrier est l’ami de la victime
— Or le meurtre a eu lieu la nuit
Donc le meurtrier n’est pas l’ami de la victime. Le raisonnement de l’adjudant Tifrice est-il correct ? Pour cela nous
procédons en trois étapes :
1. Formalisation des faits.
2. Formalisation du raisonnement permettant de déduire la conclusion à partir des hypothèses.
3. Démontrer que le raisonnement est correct ou non.
Exercice 21 (Conséquence) Pinocchio, Quasimodo et Roméo s’apprêtent à chanter en canon. Ils décident entre eux
que :
1. Si Pinocchio ne chante pas alors Quasimodo chantera.
2. Si Quasimodo chante alors Pinocchio et Roméo chanteront.
3. Si Roméo chante alors Quasimodo ou Pinocchio, l’un des deux au moins, ne chantera pas.
34/129 Chapitre 1. Logique propositionnelle
Peut-on en conclure que Pinocchio chantera ? Justifier votre réponse en formalisant le raisonnement.
Exercice 22 (Conséquence) Formaliser les énoncés suivants en dégageant les connecteurs logiques.
(a) Si Pierre est rentré chez lui, alors Jean est allé au cinéma.
(b) Marie est à la bibliothèque ou Pierre est rentré chez lui ou les deux.
(c) Si Jean est allé au cinéma, alors Marie est à la bibliothèque ou Pierre est rentré chez lui ou les deux.
(d) Marie n’est pas à la bibliothèque et Jean est allé au cinéma.
(e) Pierre est rentré chez lui.
Le dernier énoncé est-il conséquence des énoncés qui le précèdent ?
Exercice 23 (Formes normales) Pour chaque formule donnée ci-après, donner sa forme normale disjonctive et prouver
si elle est ou non satisfaisable (en donnant si besoin un modèle de la formule).
— ¬(a ⇔ b) ∨ (b ∧ c) ⇒ c.
— (a ⇒ b) ∧ (b ⇒ ¬a) ∧ (¬a ⇒ b) ∧ (b ⇒ a).
Exercice 24 (Formes normales) Soit A la formule p ∨ (q ∧ r) ⇔ (p ∨ q) ∧ (p ∨ r). Transformer A en une fnc. La formule
A est-elle valide ?
Exercice 25 (Formes normales,**) Nous revenons sur les preuves des transformations en forme normale.
1. Montrer que l’application de l’élimination des équivalences, des implications et de déplacement des négations sur
une formule donne une formule en forme normale.
2. Montrer aussi que quel que soit l’ordre d’application de l’élimination des équivalences, des implications et de
déplacement des négations sur une formule, l’algorithme de transformation en forme normale termine.
Exercice 26 (Conséquence et formes normales) L’adjudant Tifrice enquête une nouvelle fois. Ses hypothèses sont les
suivantes :
— Si Jean n’a pas rencontré Pierre l’autre nuit, c’est que Pierre est le meurtrier ou que Jean est un menteur
— Si Pierre n’est pas le meurtrier, alors Jean n’a pas rencontré Pierre l’autre nuit et le crime a eu lieu après minuit
— Si le crime a eu lieu après minuit, alors Pierre est le meurtrier ou Jean est un menteur.
Il en conclut que Pierre est le meurtrier. Son raisonnement est-il correct ? Donner la réponse en construisant la conjonc-
tion des hypothèses et de la négation de la conclusion et en mettant cette conjonction sous forme de somme de monômes.
Nous rappelons que le raisonnement est incorrect si et seulement si un des monômes de la somme ne comporte pas de
littéraux complémentaires : ce monôme donne un modèle des hypothèses, qui est un contre-modèle de la conclusion.
Exercice 27 (Formalisation, somme de monômes,*) Nous nous trouvons sur une île dont les indigènes sont répartis en
deux tribus, les Purs et les Pires. Les Purs disent toujours la vérité tandis que les Pires mentent toujours. Nous rencontrons
deux indigènes, Aha et Bébé 4 .
(a) Aha déclare : « L’un de nous au moins est un Pire ». Pouvons-nous en déduire ce que sont Aha et Bébé ?
(b) Aha déclare : « L’un de nous deux au plus est un Pire ». Pouvons-nous en déduire ce que sont Aha et Bébé ?
(c) Aha déclare :« Nous sommes tous les deux de la même tribu ». Pouvons-nous en déduire ce que sont Aha et Bébé ?
Exercice 28 (Ensemble complet et incomplet de connecteurs,**) Un ensemble de constantes et de connecteurs est dit
complet, si toute fonction booléenne est exprimable avec ces constantes et ces connecteurs. D’après le théorème 1.6.3
page 29, l’ensemble {0, 1, −, +, •} est complet.
1. Montrer que l’ensemble {−, +} est complet.
Indication : il suffit de montrer que {0, 1, •} sont définissables à l’aide de − et +.
4. Cette énigme provient du livre de Raymond M. Smullyan : « Quel est le titre de ce livre ? », qui contient bien d’autres problèmes amusants à
propos de ces indigènes.
1.8. Exercices 35/129
Exercice 29 (Dualité, récurrence,**) Considérons des formules dont les opérations sont limitées à 0, 1, ¬, ∧, ∨. Nous
rappelons que la formule duale d’une formule est obtenue en échangeant les conjonctions et les disjonctions ainsi que les
0 et les 1 et que nous notons A∗ la duale de la formule A.
1. Montrer que si 2 formules sont équivalentes, il en est de même de leurs duales. Nous donnons une indication qui
réduit la question à une récurrence simple. Soit v une assignation. Soit v l’assignation complémentaire de v : pour
toute variable x, v(x) = v(x). Par exemple l’assignation complémentaire de a = 1, b = 0 est a = 0, b = 1.
(a) Montrer que pour toute formule A : [A∗ ]v = [A]v .
(b) En déduire que si 2 formules sont équivalentes, il en est de même de leurs duales.
2. En déduire que si une formule est valide, sa duale est contradictoire.
Exercice 30 (Représentation canonique,***) Soit xi(0≤i≤n) une liste de n variables distinctes. Dans cet exercice, les
variables des formules sont toutes dans cette liste. À cette liste et à une formule A, nous associons la fonction booléenne
f à n arguments définie par f (x1 , . . . , xn ) = A. Cette notation signifie que pour a1 , . . . an ∈ B, la valeur de f (a1 , . . . , an ) est
la valeur de la formule A quand x1 = a1 , . . . , xn = an .
1. Combien y a-t-il de classes de formules ?
2. Notons par ⊕ le ou-exclusif. Nous avons x ⊕ y = 1 si et seulement soit x = 1, soit y = 1 mais pas x = y = 1
(d’où le nom de ou-exclusif). Nous pouvons aussi définir cette opération par x ⊕ y = ¬(x ⇔ y). Il est clair que
cette opération est commutative, associative, que l’opération ∧ est distributive sur ⊕ et que 0 est l’élément neutre
de ⊕. Exprimer la négation, la disjonction, l’implication et l’équivalence comme somme ou-exclusive de 1 et de
conjonctions de variables.
3. Montrer que toute formule booléenne est équivalente à une somme ou-exclusive de 1 et de produits de variables.
4. Par convention 1 est considéré comme le produit de zéro variable et 0 comme la somme ou-exclusive de zéro
produit de variables. Montrer que toute formule booléenne est équivalente à une somme ou-exclusive de produits
dont les ensembles de variables sont tous distincts.
5. Fixons un ordre arbitraire des n variables utilisées dans les formules (lorsque les variables sont des identificateurs,
cet ordre est souvent l’ordre lexicographique). Une somme ou-exclusive de produits de variables est canonique
(forme de Reed-Muller) si et seulement si :
— ses produits ne comportent pas de variables répétées et dans un produit les variables sont ordonnées de gauche
à droite dans l’ordre croissant,
— les produits sont ordonnés de gauche à droite dans l’ordre lexicographique décroissant déduit de l’ordre des
variables.
Montrer que toute formule booléenne est équivalente à une somme ou-exclusive canonique. En déduire l’unicité
de cette forme canonique.
36/129 Chapitre 1. Logique propositionnelle
Chapitre 2
Résolution propositionnelle
Sommaire
2.1 Résolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
2.1.1 Définitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
2.1.2 Cohérence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
2.1.3 Complétude pour la réfutation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
2.1.4 Réduction d’un ensemble de clauses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
2.2 Stratégie complète . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
2.2.1 Algorithme de la stratégie complète . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
2.2.2 Arrêt de l’algorithme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
2.2.3 Le résultat de l’algorithme est équivalent à l’ensemble initial de clauses . . . . . . . . . . . . . . 45
2.3 Algorithme de Davis-Putnam-Logemann-Loveland . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
2.3.1 Suppression des clauses contenant des littéraux isolés . . . . . . . . . . . . . . . . . . . . . . . . 46
2.3.2 Résolution unitaire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
2.3.3 Suppression des clauses valides . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
2.3.4 L’algorithme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
2.3.5 Solveurs SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
2.4 Exercices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
L ES tables de vérité et les transformations en sommes de monômes ou produits de clauses permettent de répondre
aux questions : une formule est-elle valide ? et un raisonnement est-il correct ? Cependant le temps de réponse de
ces méthodes augmente exponentiellement avec le nombre de variables. Pour illustrer cela, considérons la conséquence
suivante :
a ⇒ b, b ⇒ c, c ⇒ d, d ⇒ e, e ⇒ f , f ⇒ g, g ⇒ h, h ⇒ i, i ⇒ j |= a ⇒ j
En utilisant une table de vérité il faut tester 210 = 1024 lignes. Or par déduction, en utilisant la transitivité de l’im-
plication, nous savons immédiatement que le raisonnement ci-dessus est correct. Ainsi, en logique propositionnelle, les
déductions peuvent s’avérer très utiles, voire nécessaires lorsque la taille du problème à traiter est importante. Nous étu-
dions maintenant un système de déduction très simple. Dans ce système, les hypothèses et les formules déduites ne sont
pas des formules quelconques mais des clauses, c’est-à-dire des disjonctions de littéraux. De plus, le système comporte
une seule règle appelée la résolution.
Plan : Nous introduisons d’abord la méthode de résolution inventée en 1965 par J. Alan Robinson [23] dans le cadre
plus général de la recherche de preuve au premier ordre. Nous présentons ensuite une procédure pour calculer tous les ré-
solvants possibles, c’est-à-dire toutes les applications possibles de la règle de résolution : la stratégie complète. Puis, nous
étudions l’algorithme DPLL, proposé dans les années soixante par Martin Davis, Hilary Putnam, George W. Logemann et
Donald W. Loveland [10, 9]. En utilisant la notion de résolution, des méthodes de simplifications et le branchement/retour
arrière, cet algorithme prouve efficacement si une formule a un modèle ou non. Bien qu’inventé il y a plus de quarante
ans, il est toujours à la base de la plupart des solveurs SAT complets actuels. Notons que dans ce chapitre nous adoptons
la notation booléenne plus concise.
38/129 Chapitre 2. Résolution propositionnelle
2.1 Résolution
Nous souhaitons prouver que a + c est une conséquence de a + b et b + c, c’est-à-dire a + b, b + c |= a + c. En utilisant
la propriété 1.2.27 page 17, il suffit de démontrer que la formule (a + b).(b + c) ⇒ (a + c) est valide. Pour cela, nous
pouvons utiliser une table de vérité (8 lignes) ou alors une simplification de formules comme dans l’exercice 13 page 33.
Ces deux méthodes sont fastidieuses même pour des formules aussi simples (3 variables uniquement). En utilisant la règle
de résolution présentée dans ce chapitre, nous déduisons directement la clause a + c à partir des deux clauses a + b et
b + c.
Nous donnons maintenant la définition de la résolution et certaines propriétés utiles qui en dérivent. Nous prouvons
ensuite la cohérence et la complétude pour la réfutation de notre système basé sur la déduction. La cohérence nous permet
d’affirmer que si une clause C est obtenue par résolution à partir d’un ensemble Γ de clauses alors elle en est conséquence,
c’est-à-dire tout modèle de Γ est modèle de C. La complétude pour la réfutation nous permet d’affirmer que si ⊥ est
conséquence de Γ, autrement dit si Γ est insatisfaisable, alors ⊥ peut être retrouvé par résolution à partir de Γ.
2.1.1 Définitions
Dans un premier temps nous introduisons les notions nécessaires à la définition de la résolution. Nous rappelons
que les notions de clauses et littéraux sont définies dans la section 1.4 du chapitre précédent (page 22). Comme nous le
verrons dans la suite deux clauses qui ont le même ensemble de littéraux jouent le même rôle dans la résolution. Aussi,
nous définissons deux clauses égales comme étant deux clauses avec le même ensemble de littéraux.
Définition 2.1.1 (Éléments d’une clause, clauses égales et sous-clauses)
— Un littéral est élément d’une clause, s’il est élément de l’ensemble des littéraux de la clause.
— Une clause A est incluse dans une clause B, si tous les littéraux de la clause A sont éléments de la clause B. Dans
ce cas, A est une sous-clause de B.
— Deux clauses sont égales si elles ont le même ensemble de littéraux.
Exemple 2.1.2 Nous illustrons les notions introduites par des exemples simples :
— Le littéral p est élément de la clause q + p + r + p.
— La clause p + q est incluse dans la clause q + p + r + p.
— Enlever le littéral p de la clause q + p + r + p donne la clause q + r, enlever le littéral p de la clause p + p + p
donne la clause ⊥.
— Ajouter le littéral r à la clause p donne la clause p + r, ajouter le littéral p à la clause ⊥ donne la clause p.
— Les clauses p + q, q + p, et p + q + p sont égales.
Notation : Nous notons s(A) l’ensemble des littéraux de la clause A. Par convention ⊥ est la clause vide et s(⊥) = 0.
/
Propriété 2.1.8 Si l’un des parents d’un résolvant est valide, le résolvant est valide ou contient l’autre parent.
Définition 2.1.9 (C+̃D) Soient C et D deux clauses. Nous notons C+̃D la clause suivante :
— Si C = ⊥ alors C+̃D = D,
— sinon si D = ⊥ alors C+̃D = C sinon C+̃D = C + D.
Ajouter le littéral L à la clause C, c’est construire C+̃L. Munis de cette définition, nous pouvons reformuler plus
simplement la règle de résolution.
Définition 2.1.10 (Résolvant) Soient A et B deux clauses. La clause C est un résolvant de A et B si et seulement s’il y a
un littéral L tel que :
— L est élément de la clause A, Lc est élément de la clause B
— C est égale à la clause A0 +̃B0 où A0 = A − {L} est obtenue en enlevant L de A et B0 = B − {Lc } est obtenue en
enlevant Lc de B.
La combinaison de résolutions successives permet de générer de nouvelles clauses. Une clause issue de ces résolvants
sera une preuve par résolution de cette clause à partir d’un ensemble de clauses.
Définition 2.1.11 (Preuve) Soient Γ un ensemble de clauses et C une clause. Une preuve de C à partir de Γ est une liste
de clauses qui se termine par C. Toute clause de la preuve est égale à un élément de Γ ou est un résolvant de deux clauses
la précédant dans la preuve. La clause C est déduite de Γ, notée Γ ` C, s’il y a une preuve de C à partir de Γ.
Exemple 2.1.12 Soit Γ l’ensemble de clauses p + q, p + q, p + q, p + q. Nous montrons que Γ ` ⊥ par la preuve suivante :
40/129 Chapitre 2. Résolution propositionnelle
Nous pouvons aussi voir une preuve comme un arbre dont les feuilles sont les hypothèses et dont les sommets internes
sont obtenus par construction des résolvants.
Définition 2.1.13 (Taille de preuve) Une preuve P de C à partir d’un ensemble de clauses Γ est de taille n si elle contient
n lignes.
La taille de la preuve donnée dans l’example 2.1.12 page précédente est 8, ce qui n’est pas forcément intuitif sur la
représentation en arbre. Nous utiliserons les deux propriétés énoncées ci-dessous souvent de manière implicite dans les
preuves.
Propriété 2.1.14 (Monotonie et composition) Soient Γ, ∆ deux ensembles de clauses et A, B deux clauses.
1. Monotonie de la déduction : Si Γ ` A et si Γ est inclus dans ∆ alors ∆ ` A
2. Composition des déductions : Si Γ ` A, Γ ` B et si C est un résolvant de A et B alors Γ ` C.
2.1.2 Cohérence
La cohérence de la résolution signifie que si une clause C est obtenue après une à plusieurs applications de la règle de
résolution à un ensemble de clauses Γ alors tout modèle de Γ est aussi modèle de C (autrement dit, C est une conséquence
de Γ). La première partie de la preuve consiste à démontrer la cohérence d’une application de la règle de résolution
(théorème 2.1.15). Nous généralisons ensuite par induction dans le théorème 2.1.16 page suivante.
Preuve : Supposons que C soit un résolvant de A et B. Par définition il y a un littéral L tel que L ∈ s(A), Lc ∈ s(B), s(C) =
(s(A) − {L}) ∪ (s(B) − {Lc }). Soit v une assignation modèle de A et B, c’est-à-dire, [A]v = 1 et [B]v = 1. Montrons que v
est modèle de C. Nous distinguons deux cas possibles :
2
2.1. Résolution 41/129
Théorème 2.1.16 (Cohérence de la déduction) Soient Γ un ensemble de clauses et C une clause. Si Γ ` C alors Γ |= C.
Preuve : Supposons que Γ ` C. Par définition, il existe une preuve P de C à partir de Γ. Supposons que pour toute preuve
de D à partir de Γ, plus courte que P, nous avons Γ |= D. Montrons que Γ |= C. Nous avons deux cas possibles :
Corollaire 2.1.17 D’après le théorème 2.1.16, si Γ ` ⊥ alors Γ |= ⊥, autrement dit Γ est insatisfaisable.
Définition 2.1.18 (Γ[L := 1]) Soient Γ un ensemble de clauses et L un littéral. Γ[L := 1] est l’ensemble de clauses obtenu
en supprimant les clauses dont L est élément et en enlevant Lc des autres clauses. Nous posons Γ[L := 0] = Γ[Lc := 1].
Γ[L := x] est égal à l’ensemble de clauses obtenu en donnant à L la valeur x (x = 0 ou x = 1) et en simplifiant le résultat
obtenu.
— Γ[p := 0] =
Afin de donner une intuition de comment calculer Γ[p := 1] et Γ[p := 0], nous considérons le produit de clauses suivant
(p + q)(q + r)(p + q)(p + r) et observons :
— (1 + q)(q + r)(1 + q)(1 + r) =
Nous notons v[L := 1] l’assignation qui donne à L la valeur 1, à Lc la valeur 0 et ne change pas la valeur des autres
littéraux.
Définition 2.1.20 (v[L := 1]) Soit une assignation v, l’assignation v[L := 1] est l’assignation identique à v sauf éventuel-
lement pour x la variable de L. Si L = x alors v[L := 1](x) = 1, si L = x alors v[L := 1](x) = 0.
Nous posons v[L := 0] = v[Lc := 1]. La propriété suivante se déduit du fait que si Γ a un modèle v, alors v donne soit la
valeur 1 soit la valeur 0 au littéral L.
Propriété 2.1.21 Soient Γ un ensemble de clauses et L un littéral. Γ a un modèle si et seulement si Γ[L := 1] ou Γ[L := 0]
a un modèle.
Lemme 2.1.22 Soient Γ un ensemble de clauses, C une clause et L un littéral. Si Γ[L := 1] ` C alors Γ ` C ou Γ ` C+̃Lc .
Rappel : L’opération +̃ est introduite dans la définition 2.1.9 page 39.
Lemme 2.1.23 Soient Γ un ensemble de clauses, C une clause et L un littéral. Si Γ[L := 0] ` C alors Γ ` C ou Γ ` C+̃L.
Preuve : Supposons Γ[L := 0] ` C. Puisque Γ[L := 0] = Γ[Lc := 1] et que Lcc = L, d’après le lemme 2.1.22 nous avons
Γ ` C ou Γ ` C+̃L. 2
Propriété 2.1.28 Un ensemble de clauses E est équivalent à l’ensemble de clauses réduit obtenu à partir de E.
Preuve :
2
2.2. Stratégie complète 43/129
1 a+b
2 a+b
3 a+b
4 a+b
L’ensemble Θ0 est vide. L’algorithme calcule les résolvants non valides suivants :
5 a résolvant de 1 et 2
6 b résolvant de 1 et 3
7 b résolvant de 2 et 4
8 a résolvant de 3 et 4
9 ⊥ de 5 et 8
1 a+b
2 a+b
5 a résolvant de 1 et 2
3 a+b
4 a+b
8 a résolvant de 3 et 4
9 ⊥ résolvant de 5 et 8
Nous pouvons utiliser la représentation ci-dessous sous forme de tableau représentant la construction de ces en-
sembles.
k ∆k Θk ∆k ∪ Θk Résolvants de ∆k et ∆k ∪ Θk
0
1
2
3
Comme le montre cet exemple, les clauses de ∆i ont des preuves de hauteur i, et celles de Θi des preuves de hauteur
inférieure à i.
Exemple 2.2.2 L’application de la stratégie complète sur l’ensemble {a, c, a+b, c+e} nous donne l’ensemble {a, c, e, b}.
k ∆k Θk ∆k ∪ Θk Résolvants de ∆k et ∆k ∪ Θk
0
1
2
Nous montrons que l’algorithme se termine et qu’il est correct, c’est-à-dire que l’ensemble Θk est l’ensemble des
clauses minimales déduites de Γ. Γ est insatisfaisable si et seulement si la clause vide est élément de Θk .
clauses. D’après l’algorithme, les ensembles ∆i sont non vides pour i < k. Nous montrons ci-dessous que ces ensembles
sont disjoints. Par conséquent k ≤ 2n + 1, autrement dit l’algorithme s’arrête.
que C contient une clause de ∆i+1 ∪ Θi+1 . Nous examinons tous les cas possibles pour C.
1. C ∈ ∆i+1 . Donc C contient une clause de ∆i+1 ∪ Θi+1 .
2. C ∈ j≤i ∆ j . Par hypothèse de récurrence, C contient une clause D ∈ ∆i ∪ Θi . Nous distinguons deux situations
S
pour D.
(a) D ∈ Θi+1 . Donc C contient une clause de ∆i+1 ∪ Θi+1 .
(b) D 6∈ Θi+1 . Par construction de Θi+1 , puisque D ∈ ∆i ∪ Θi et que D 6∈ Θi+1 , c’est que D contient une clause
de ∆i+1 . Or C contient D, donc C contient aussi une clause de ∆i+1 ∪ Θi+1 .
2
Propriété 2.2.4 Pour tout i ≤ k, les ensembles ∆i sont disjoints entre eux.
2.3. Algorithme de Davis-Putnam-Logemann-Loveland 45/129
Propriété 2.2.5 Pour tout i < k, les ensembles ∆i ∪ Θi et ∆i+1 ∪ Θi+1 sont équivalents.
Preuve :
1. Toute clause de ∆i+1 ∪ Θi+1 est conséquence de ∆i ∪ Θi . En effet toute clause de ∆i+1 ∪ Θi+1 est élément de ∆i ∪ Θi
ou résolvant de deux éléments de cet ensemble, donc est conséquence de cet ensemble.
2. Toute clause de ∆i ∪ Θi est conséquence de ∆i+1 ∪ Θi+1 . Soit C ∈ ∆i ∪ Θi . Nous distinguons deux cas possibles :
(a) C ∈ Θi+1 , ainsi C est conséquence de ∆i+1 ∪ Θi+1 .
(b) C 6∈ Θi+1 , ainsi C contient une clause de ∆i+1 donc est conséquence de ∆i+1 ∪ Θi+1 .
2
Preuve : Par définition ∆0 est l’ensemble obtenu par réduction de Γ, d’après la propriété 2.1.28 page 42, ces deux
ensembles sont équivalents. Puisque Θ0 est vide, Γ est équivalent à ∆0 ∪ Θ0 . D’après la propriété 2.2.5 et par récurrence,
∆0 ∪ Θ0 est équivalent à l’ensemble de clauses ∆k ∪ Θk . Puisque l’algorithme termine quand ∆k est l’ensemble vide, les
ensembles Γ et Θk sont équivalents. 2
Définition 2.3.1 (Littéral isolé) Soient Γ un ensemble de clauses et L un littéral élément d’une clause de Γ, L est un
littéral isolé (relativement à Γ), si aucune clause de Γ ne comporte de littéral complémentaire de L.
Lemme 2.3.2 La suppression des clauses qui comportent un littéral isolé, préserve la satisfaisabilité.
Les clauses unitaires sont aussi des clauses particulières qui sont :
— soit isolées et donc seront traitées par la simplification précédente,
— soit de potentiels résolvants, dans ce cas il faut effectuer la résolution dite « unitaire » de ces clauses.
Lemme 2.3.5 Soit Γ un ensemble de clauses. Soit L l’ensemble des littéraux des clauses unitaires de Γ. Soit Θ l’ensemble
de clauses ainsi obtenu à partir de Γ :
— Si L comporte deux littéraux complémentaires, alors Θ = {⊥}.
— Sinon Θ est obtenu ainsi :
• Nous enlevons les clauses qui comportent un élément de L.
• À l’intérieur des clauses restantes nous enlevons les littéraux complémentaires des éléments de L.
Γ a un modèle si et seulement si Θ en a un.
Exemple 2.3.6
— Soit Γ l’ensemble de clauses : p + q, p, q.
Enfin la dernière transformation utilisée dans l’algorithme DPLL est de simplement enlever les clauses valides d’un
ensemble de clauses. Ceci peut paraître une évidence mais cette transformation est une des idées centrales de cet algo-
rithme, une fois une variable affectée à une valeur, elle est implicitement utilisée dans la suppression de clauses contenant
des littéraux isolés.
Lemme 2.3.7 Soit Γ un ensemble de clauses. Soit Θ l’ensemble de clauses obtenu en supprimant les clauses valides de
Γ. Γ a un modèle si et seulement si Θ en a un.
Preuve :
— Supposons que Γ a un modèle v, comme Θ est un sous-ensemble des clauses de Γ, v est aussi modèle de Θ. Donc,
Θ a un modèle.
— Supposons que Θ a un modèle v. Soit v0 une assignation de Γ telle que v0 (x) = v(x) pour toute variable x présente
à la fois dans Γ et Θ. Soit C une clause de Γ. Si C est aussi une clause de Θ, alors v0 est un modèle de C car v et v0
donnent la même valeur à C. Si C n’est pas une clause de Θ, alors C est valide, en conséquence toute assignation,
v0 en particulier, est modèle de C. D’où, Γ a un modèle : v0 .
2
2.3.4 L’algorithme
Nous donnons une version de l’algorithme DPLL dans la figure 2.1 page suivante dans la fonction Algo_DPLL. Nous
pouvons constater dans l’algorithme que nous supprimons une seule fois les clauses valides avant de réellement commen-
cer les simplifications. Cela se justifie par le fait que l’algorithme ne pourra pas produire de nouvelles clauses valides.
En effet, il ne fait qu’enlever des littéraux des clauses initialement données. Par suite, il est inutile d’enlever des clauses
valides lors de l’étape de réduction, puisqu’il n’y aura plus de telles clauses. La fonction DPLL teste d’abord si la clause
vide a été générée, puis effectue les simplifications possibles avant de choisir une variable pour appliquer récursivement
la même fonction dans le cas où cette variable est affectée à vraie et dans le cas où elle est affectée à faux.
Pour obtenir une trace de l’algorithme, nous supprimons les clauses valides, en abrégé VAL, puis nous dessinons
l’arbre des appels avec l’argument de la fonction ainsi que les ensembles obtenus par les étapes 2 (réduction, en abrégé
RE), 3 (enlèvement des clauses ayant des littéraux isolés, en abrégé ELI) et 4 (résolution unitaire, abrégé en RU). À cause
du « ou alors », il est inutile de poursuivre la construction de cet arbre dès que la réponse vrai (attachée à un ensemble vide)
a été obtenue. Dans ce cas, un modèle peut être exhibé en remontant la récursion, en tenant compte des simplifications :
le modèle doit rendre vrai chaque littéral isolé ou clause unitaire trouvé.
Exemple 2.3.8 Nous illustrons l’application de cet algorithme sur deux ensembles de clauses.
— Soit Γ l’ensemble de clauses : a + b, a + b, a + c, a + c, b + c, b + c. Nous donnons la trace de l’algorithme.
48/129 Chapitre 2. Résolution propositionnelle
p + q, p + s, p + q, p + s
u s=0 s=1 )
p + q, p, p + q p + q, p + q, p
RE
p, p + q
ELI : q=1
p
ELI : p = 0
0/
Puisqu’une feuille porte l’ensemble vide, l’ensemble Γ est satisfaisable. Il est inutile de poursuivre la construction
2.3. Algorithme de Davis-Putnam-Logemann-Loveland 49/129
de la branche droite.
Preuve : La réduction et les transformations 2.3.1 page 46, 2.3.2 page 46 et 2.3.3 page 47 préservent l’existence d’un
modèle, donc au pas 0 et 1, l’algorithme vérifie l’invariant suivant : la valeur courante de l’ensemble de clauses de Γ a un
modèle si et seulement si Γ a un modèle. Nous en déduisons immédiatement que les réponses de l’algorithme, fournies
au pas 0 ou 1, sont correctes. Au pas 5, pour les mêmes raisons, la valeur courante de l’ensemble de clauses de Γ, lors de
l’appel de DPLL, a un modèle si et seulement si Γ a un modèle. Supposons les appels récursifs corrects :
— Si DPLL(Γ[x := 0]) est vrai, par récurrence Γ[x := 0] est satisfaisable donc Γ est satisfaisable (nous utilisons le
résultat 2.1.21 page 42 : Γ est satisfaisable ssi Γ[x := 0] est satisfaisable ou Γ[x := 1] est satisfaisable), ce qui
correspond à la valeur vrai de DPLL(Γ).
— Si DPLL(Γ[x := 0]) est faux, par récurrence Γ[x := 0] est insatisfaisable. Dans ce cas, DPLL(Γ) vaut DPLL(Γ[x := 1]) :
— Supposons que DPLL(Γ[x := 1]) soit vrai alors par récurrence Γ[x := 1] est satisfaisable donc Γ est satisfaisable,
ce qui correspond à la valeur vrai de DPLL(Γ).
— Supposons que DPLL(Γ[x := 1]) soit faux, alors par récurrence Γ[x := 1] est insatisfaisable. Donc Γ est insatis-
faisable, ce qui correspond à la valeur faux de DPLL(Γ).
2
Preuve : Au pas 0, la fonction Algo_DPLL consiste en un test, puis soit le renvoi de la valeur vrai soit l’appel de la
fonction DPLL(Γ). Le pas 0 consiste en la suppression de clauses de l’ensemble de départ, cet ensemble étant fini, le pas 0
termine. Donc, la fonction Algo_DPLL termine si la fonction DPLL(Γ) termine.
Considérons un appel de la fonction DPLL(Γ). Le pas 1 est constitué d’un test et d’instructions élémentaires, donc
il termine. Le pas 2 consiste à réduire Γ qui est un ensemble fini. La réduction consistant à supprimer des clauses, elle
termine. Le pas 3 consiste à supprimer des clauses, puis éventuellement retourner au pas 1. Le nombre de clauses étant
fini, soit l’algorithme termine en 1, soit le pas 4 débute. De la même manière, le pas 4 consiste à supprimer des clauses
et des variables, qui sont en nombres finis, puis éventuellement retourner au pas 1. Le nombre de clauses et de variables
étant fini, soit l’algorithme termine en 1, soit le pas 5 débute. Le pas 5 consiste en un ou deux appels récursifs sur un
ensemble de clauses où une variable a disparu (la valeur d’une variable est fixée). Ainsi, la récurrence en 5 se termine car
à chaque appel récursif le nombre de variables diminue strictement. D’où, l’algorithme Algo_DPLL termine. 2
Remarque 2.3.11 (Oubli de simplifications) L’algorithme Algo_DPLL a été donné avec les étapes de « simplification » :
suppression des clauses valides (0), réduction (2), enlèvement des littéraux isolés (3) et réduction unitaire (4). L’algo-
rithme reste correct si nous omettons ces étapes, ou si nous ne faisons qu’une partie des simplifications, ce qui est souvent
le cas lorsque nous faisons une trace de l’exécution sans machine. Car sans machine il est fréquent d’oublier des simpli-
fications, ce qui ne nuit pas car l’algorithme reste correct.
Remarque 2.3.12 (Choix de la variable) Un bon choix pour la variable x de l’étape (5), consiste à choisir la variable
qui apparaît le plus souvent. Un meilleur choix consiste à choisir la variable qui va entraîner par la suite le plus de
simplifications : il faut faire des compromis entre le temps passé à choisir la « bonne » variable et l’importance des
simplifications induites par ce choix. Plusieurs heuristiques classiques de choix de variable sont présentées dans le para-
graphe [Link] page suivante.
— Les solveurs SAT « complets » sont généralement des versions améliorées de l’algorithme DPLL. Parmi les solveurs
SAT complets les plus utilisés à l’heure actuelle, nous pouvons citer par exemple zchaff, satz, march ou encore
GRASP.
— Les solveurs SAT « incomplets » sont des algorithmes de semi-décision qui finissent par trouver un modèle à la
formule, s’il existe et qui ne terminent pas dans le cas contraire. Ces algorithmes sont fondés sur des marches
aléatoires dans l’espace d’état. Dans cette catégorie, nous pouvons citer les algorithmes par exemple WalkSAT et
GSAT.
Nous décrivons maintenant, de manière non-exhaustive, les principales améliorations de l’algorithme DPLL utilisées dans
les solveurs SAT complets.
[Link] Apprentissage
L’apprentissage consiste à analyser et apprendre les raisons qui ont amené à une contradiction : lorsqu’une assignation
partielle amène à une contraction, il est possible d’isoler un sous-ensemble d’assignations et un sous-ensemble de clauses,
qui sont responsables du conflit. À partir de ces assignations, il est possible de construire (d’apprendre) une clause qui est
impliquée par ces clauses. Cette nouvelle clause est ajoutée à l’ensemble de clauses du problème. Les assignations perti-
nentes sont déterminées par un graphe de dépendance entre les clauses et les assignations, appelé graphe d’implication.
Les clauses apprises permettent de ne pas refaire plusieurs fois les mêmes « erreurs » dans l’arbre de recherche.
[Link] Redémarrage
La plupart des solveurs SAT actuels utilisent une stratégie de redémarrage, qui consiste à redémarrer la recherche en
prenant en compte de nouvelles clauses apprises durant la recherche précédente. La plupart des solveurs effectuent un
redémarrage après qu’un seuil de clauses apprises soit atteint. Ainsi, à chaque redémarrage, le parcours de l’espace de
2.3. Algorithme de Davis-Putnam-Logemann-Loveland 51/129
recherche change car l’ensemble de clauses est modifié. Il faut noter que la plupart des solveurs effacent régulièrement les
clauses apprises. Ainsi, le mixage des redémarrages et des oublis peut dans certains cas mettre en cause la complétude des
solveurs. Un paramétrage des redémarrages est donc nécessaire pour garder cette dernière propriété. Le solveur Chaff, par
exemple, augmente à chaque redémarrage le seuil au-delà duquel une clause est oubliée. Ainsi, de plus en plus de clauses
sont gardées, ce qui assure la complétude.
2.4 Exercices
Exercice 31 (Résolvant) Par résolution, nous avons :
a+b a+b
b+b
Exercice 32 (Résolvant) Nous rappelons que deux clauses sont égales si et seulement si elles ont les mêmes ensembles
de littéraux.
— Les clauses p + q + r + q + p + s + q + r et s + q + r + p sont-elles égales ?
— Les clauses p + q + r + p et q + r + q + r + q + r sont-elles égales ? L’une est-elle incluse dans l’autre ? L’une
est-elle la conséquence de l’autre ? Sont-elles équivalentes ?
— Indiquer tous les résolvants des clauses a + b + c et a + b + c. Ces résolvants sont-ils valides ?
Exercice 34 (Formalisation et résolution,*) Remarquons que : « x à moins que y » se formalise en ¬(x ⇔ y). Dans
une maison hantée, les esprits se manifestent sous deux formes différentes, un chant obscène et un rire sardonique,
cependant nous pouvons influencer le comportement en jouant de l’orgue ou en brûlant de l’encens. Compte-tenu des
données suivantes :
(i) Le chant ne se fait pas entendre, à moins que nous jouions de l’orgue sans que le rire ne se fasse entendre.
(ii) Si nous brûlons de l’encens, le rire se fait entendre si et seulement si le chant se fait entendre.
(iii) (En ce moment) Le chant se fait entendre et le rire est silencieux.
Et de la conclusion :
(iv) (En ce moment) Nous jouons de l’orgue et ne brûlons pas d’encens.
Nous posons :
— c : le chant se fait entendre.
— o : nous jouons de l’orgue.
— r : le rire se fait entendre.
— e : nous brûlons de l’encens.
1. Simplifier en produit de clauses ¬(x ⇔ y).
2. Formaliser sous forme de produit de clauses les hypothèses et la négation de la conclusion.
3. Prouver par résolution que le raisonnement est correct.
Autrement dit transformer le produit des hypothèses et de la négation de la conclusion en un produit de clauses, et en
déduire la clause vide.
Exercice 35 (Preuve,*) Montrer, à l’aide d’une preuve par résolution, la correction du raisonnement suivant :
r + q ⇒ t,t.q ⇒ r, q |= t ⇔ r.
Exercice 36 (Formalisation et preuve,*) Montrer par résolution que le raisonnement suivant est contradictoire :
— Il fait beau à moins qu’il neige.
— Il pleut à moins qu’il neige.
— Il fait beau à moins qu’il pleuve.
2.4. Exercices 53/129
Exercice 37 (Définir une clause) Une clause est la clause vide ou une disjonction (non vide) de littéraux. Donner une
définition formelle de ce qu’est une clause et définir par récurrence la fonction s telle que s(C) est l’ensemble des littéraux
de la clause C.
Exercice 40 (La résolution n’ajoute aucun littéral,*) Soit Γ un ensemble de clauses. Un littéral de Γ est un littéral
d’une clause de Γ. Montrer que toute clause déduite de Γ ne comporte que des littéraux de Γ.
{p + q, p + r + q + p, p + r, q + p + q, q + r + p, r + q + p + r, r + q}.
54/129 Chapitre 2. Résolution propositionnelle
1. Réduire cet ensemble (la réduction est définie en 2.1.4 page 42)
2. Indiquer si l’ensemble réduit est ou non satisfaisable.
{a + b + f , a + b + f , e + a, a + b, a + c, d + a + d, a + b, a + c + d, d}.
Exercice 45 (DPLL) Utiliser l’algorithme Algo_DPLL pour déterminer si les ensembles suivants de clauses sont satis-
faisables ou insatisfaisables :
— {a + b + c + d + e + f , a + b, b + a, c + d, d + c, b + c, b + c, b + c, e, f }.
— {a + b + c + d + f , a + b, b + a, c + d, d + c}.
— {b + j + a, a + j + b, b + a + j, a + j, j + b, b + j, j + b, j + s, s + b}.
— {a + c + d, b + c + f , b + e + f , c + e + f , e + f , c + d, a, e + f }.
Donner une trace de l’algorithme.
Déterminer par la stratégie complète de résolution si Γ est insatisfaisable ou possède un modèle. Donner la trace de
l’algorithme. Indiquer la ou les preuves obtenues. Si Γ a un modèle indiquez-le.
{p + q, p + s, s + t,t, q + r, r, r + p + t, q + z + z, q + r + s}.
Appliquer l’algorithme de la stratégie complète sur cet ensemble de clauses et conclure si cet ensemble est satisfaisable
ou non.
Exercice 48 (Stratégie complète) Considérons la fonction f telle que f (x, y, z) = 0 si et seulement si le nombre d’ar-
guments valant 1 est pair. Exprimer f comme un produit de clauses suivant la méthode décrite dans la sous-section 1.6
page 29 puis simplifier f en utilisant la stratégie complète.
Exercice 51 (De SAT à 3-SAT,***) SAT est un problème de décision qui peut être énoncé comme suit : « étant donné un
ensemble de clauses Γ, existe-t-il une assignation qui soit modèle de Γ ? » 3-SAT est une restriction de ce problème où
toutes les clauses de Γ ont exactement trois littéraux.
SAT est un problème NP-complet [5]. Dans cet exercice, nous proposons d’étudier une réduction polynomiale de SAT
vers 3-SAT, prouvant ainsi que 3-SAT est aussi NP-complet 2 .
Une réduction polynomiale de SAT vers 3-SAT consiste à transformer en temps polynomial un ensemble de clauses Γ
en un ensemble de clauses Γ0 vérifiant les deux propriétés suivantes :
2. Il faut noter qu’en général, un problème k-SAT n’est pas nécessairement NP-complet. Par exemple, 2-SAT a été prouvé polynomial.
2.4. Exercices 55/129
Par construction, la réduction proposée vérifie la propriété (a). Les réponses aux questions suivantes permettent de
prouver les propriétés (b) et (c) :
1. Montrer (sans table de vérité) que toute assignation donne la même valeur à ci et Ci0 lorsque ci est constituée d’un
seul littéral.
2. Montrer (sans table de vérité) que toute assignation donne la même valeur à ci et Ci0 lorsque ci est constituée de
deux littéraux.
3. Soit ci une clause de plus de 3 littéraux. Montrer que si ci a un modèle, alors Ci0 a aussi un modèle.
4. Soit ci une clause de plus de 3 littéraux. Montrer que tout modèle de Ci0 est modèle de ci .
5. La réduction proposée maintient uniquement la satisfaisabilité. Montrer qu’elle ne maintient pas le sens.
56/129 Chapitre 2. Résolution propositionnelle
Chapitre 3
Déduction Naturelle
Sommaire
3.1 Système formel de la déduction naturelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
3.1.1 Règles de conjonction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
3.1.2 Règles de disjonction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
3.1.3 Règles de l’implication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
3.1.4 Deux règles spéciales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
3.1.5 Preuves en déduction naturelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
3.2 Tactiques de preuve . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
3.3 Cohérence de la déduction naturelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
3.4 Complétude de la déduction naturelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.5 Outils . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.5.1 Logiciel de construction automatique de preuves . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.5.2 Dessiner des arbres de preuves . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.6 Exercices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
U NE preuve dans les cours de Mathématiques est une décomposition du raisonnement en pas élémentaires évidents,
nous pratiquons alors sans le savoir la déduction naturelle. Dans ce chapitre, nous présentons un système formel qui
est une modélisation particulière de la déduction naturelle. La déduction naturelle et le calcul de séquent furent introduits
en 1934 par Gerhard Gentzen (1909-1945) [12, 13]. Les preuves dans notre système ne sont pas des arbres comme dans
le système original de Gehard Gentzen mais ressemblent plus aux preuves des mathématiciens. Nous expliquons aussi
comment faire le lien entre ces deux formalismes en construisant des arbres proches de ceux introduits originellement.
Nous choisissons de ne parler que de la logique classique, par opposition à la logique intuitionniste qui est obtenue en
omettant la règle de réduction à l’absurde (la dernière règle de la table 3.1 page 59).
Remarque préliminaire : Pour simplifier l’étude de la déduction naturelle, nous considérons que le vrai, la négation et
l’équivalence sont des abréviations ainsi définies :
— > abrège ⊥ ⇒ ⊥.
— ¬A abrège A ⇒ ⊥.
— A ⇔ B abrège (A ⇒ B) ∧ (B ⇒ A).
Deux formules seront considérées comme égales, si les formules obtenues en éliminant les abréviations sont identiques.
Par exemple, les formules ¬¬a, ¬a ⇒ ⊥ et (a ⇒ ⊥) ⇒ ⊥ sont égales. Il est clair que deux formules égales, au sens ci-
dessus, sont équivalentes (voir exercice 55 page 67) et nous utilisons implicitement cette propriété quand nous remplaçons
une formule par une autre formule égale aux abréviations près.
Plan : Nous décrivons tout d’abord notre système de règles de déduction naturelle et introduisons la notion de preuve
dans ce contexte. Ensuite, nous présentons des tactiques pour aider le lecteur à la rédaction de preuve. Nous montrons
la cohérence et la complétude de notre système. Enfin nous présentons un outil permettant à partir d’une formule de
construire automatiquement une preuve ou bien d’exhiber un contre-exemple.
58/129 Chapitre 3. Déduction Naturelle
Définition 3.1.1 (Règle) Une règle est constituée de formules dites hypothèses H1 , . . . , Hn et d’une conclusion. Les hypo-
thèses sont écrites au-dessus d’un trait et l’unique formule en dessous de ce trait est la conclusion de la règle. Le nom
d’une règle est écrit au même niveau que le trait séparant hypothèses et conclusion.
H1 . . . Hn
R
C
La déduction naturelle que nous présentons comporte une dizaine de règles de déduction qui sont regroupées dans la
table 3.1 page suivante. La règle fondamentale est la suivante : si nous pouvons déduire une formule B d’une hypothèse A,
alors nous pouvons déduire A ⇒ B en nous passant de cette hypothèse. Nous décrivons chacune des dix règles du système
de déduction que nous considérons. L’application de ces règles et seulement de ces règles va nous permettre de prouver la
correction des raisonnements. Il est donc important de bien comprendre le fonctionnement de chacune d’entre elles. Nous
avons deux familles de règles pour chaque connecteur : les règles d’introduction et les règles d’élimination. L’intuition du
rôle des règles d’introduction est de générer un symbole de la logique afin de bâtir progressivement la formule à prouver.
Les règles d’élimination servent à simplifier un raisonnement ou à obtenir une nouvelle formule grâce aux raisonnements
déjà réalisés et ainsi faire disparaître un connecteur logique. En plus nous avons deux règles spéciales, que nous décrirons
en dernier, une pour éliminer deux occurrences successives de la négation et une autre pour déduire d’importe quoi à partir
du faux.
A B
∧I
A∧B
Les règles d’élimination de la conjonction, notées ∧E1 et ∧E2, permettent de déduire à partir de la conjonction de
deux formules A ∧ B soit la formule A soit la formule B. Ainsi nous avons éliminé le connecteur de la conjonction.
A∧B A∧B
∧E1 ∧E2
A B
A A
∨I1 ∨I2
A∨B B∨A
La règle d’élimination de la disjonction, notée ∨E, est plus complexe. Afin de déduire la formule C à partir de la
disjonction A ∨ B il faut aussi prouver les prémisses suivantes : A implique C et B implique C. Cette règle formalise
la notion de preuve par cas utilisée en mathématiques : supposons que dans un environnement donné, nous souhaitons
prouver C alors que deux cas, A ou B, sont possibles ; nous nous plaçons alors dans le cas où A est vérifiée et nous prouvons
C, puis nous nous plaçons dans le cas où B est vérifiée et nous prouvons C.
A A⇒B
⇒E
B
La règle fondamentale de notre système est la règle d’introduction de l’implication ⇒ I : si nous pouvons déduire
une formule B d’une hypothèse A, alors nous pouvons déduire A ⇒ B en nous passant de cette hypothèse. Cette règle est
résumée par le schéma ci-dessous, où la notation [A] indique que si A est une hypothèse de la preuve de B, cette hypothèse
est enlevée de la preuve de A ⇒ B, autrement dit ne sert plus pour prouver A ⇒ B.
[A]
..
..
B
⇒I
A⇒B
⊥ E fq
A
— La seconde est la règle de réduction à l’absurde, notée RAA pour « reductio ad absurdum ». Elle élimine deux
occurrences successives de la négation.
¬¬A
RAA
A
Nous regroupons l’ensemble des règles de la déduction naturelle dans la table 3.1.
Introduction Élimination
Règle du faux
Définition 3.1.2 (Ligne de preuve) Une ligne de preuve est de l’une des trois formes suivantes :
— Supposons formule,
— formule,
— Donc formule.
Un brouillon de preuve est une preuve en construction, intuitivement elle a au moins autant de Supposons que de
Donc.
Définition 3.1.3 (Brouillon de preuve) Un brouillon de preuve est une suite de lignes telle que, dans tout préfixe de la
suite, le nombre de lignes commençant par le mot Supposons est au moins égal à celui des lignes commençant par le
mot Donc.
Exemple 3.1.4 Dans l’exemple ci-dessous, la suite des lignes de 1 à 3 est un brouillon de preuve. Par contre la suite des
lignes de 1 à 5, n’est pas un brouillon de preuve car dans la suite des lignes 1 à 4, le nombre de lignes commençant par
le mot Donc dépasse celui des lignes commençant par le mot Supposons.
numéro ligne
1 Supposons a
2 a∨b
3 Donc a ⇒ a ∨ b
4 Donc ¬a
5 Supposons b
Définition 3.1.5 (Contexte) Nous numérotons les lignes d’un brouillon de preuve de 1 à n. Pour i de 1 à n, la liste de
formules Γi est le contexte de la ligne i. La liste Γ0 est vide et les listes de formules Γi sont ainsi définies :
— Si la ligne i est « Supposons A », alors Γi = Γi−1 , i.
— Si la ligne i est « A » alors Γi = Γi−1
— Si la ligne i est « Donc A » alors Γi est obtenue en enlevant la dernière formule de Γi−1
3.1. Système formel de la déduction naturelle 61/129
Nous présentons nos preuves sous forme de tableaux, ce qui nous permet de numéroter les lignes d’une preuve, les
contextes utilisables, et les règles utilisées pour générer une nouvelle ligne.
Exemple 3.1.6 Nous illustrons ici la gestion des contextes sur un brouillon de preuve simple.
[Link] Preuves
Nous précisons la notion de conclusion et de formule utilisable afin de définir et manipuler des preuves en déduction
naturelle.
Définition 3.1.7 (Conclusion, formule utilisable) Nous définissons la notion de conclusion et de formule utilisable :
— La formule figurant sur une ligne d’un brouillon de preuve est la conclusion de la ligne.
— La conclusion d’une ligne est utilisable tant que son contexte (c’est-à-dire les hypothèses qui ont permis de la
déduire) est présent.
Autrement dit la conclusion de la ligne i est utilisable sur la ligne i et sur toutes les lignes suivantes dont le contexte a
pour préfixe le contexte de la ligne i.
Exemple 3.1.8 Dans l’exemple ci-dessous, la conclusion de la ligne 2 est utilisable sur la ligne 2, et pas au delà, car à
la ligne 3, l’hypothèse qui a permis de la déduire est enlevée.
Nous donnons la définition de preuve dans un environnement. Un environnement est un ensemble de formules suppo-
sées « vraies ». Intuitivement, réaliser une preuve dans un environnement consiste à pouvoir utiliser sans les prouver les
formules de l’environnement.
Définition 3.1.9 (Preuve) Soit Γ un ensemble de formules, une preuve dans l’environnement Γ est un brouillon de preuve
ayant les propriétés suivantes :
1. Pour toute ligne « Donc A », la formule A est égale à B ⇒ C, où B est la dernière formule du contexte de la ligne
précédente et où C est une formule utilisable sur la ligne précédente ou égale à un élément de l’environnement Γ.
2. Pour toute ligne « A », la formule A est la conclusion d’une règle (autre que la règle d’introduction de l’implica-
tion) dont les prémisses sont utilisables sur la ligne précédente ou sont éléments de l’environnement Γ.
La ligne « Donc A » est une application de la règle d’introduction de l’implication. En effet, C est déduite de Γ ou
d’hypothèses qui figurent dans la ligne précédente. La liste des hypothèses de la ligne précédente se terminant par B, nous
pouvons en déduire B ⇒ C, en nous passant de l’hypothèse B.
Définition 3.1.10 (Preuve d’une formule) Une preuve de la formule A dans l’environnement Γ est soit la preuve vide
lorsque A est élément de Γ, soit une preuve dont la dernière ligne est de conclusion A et de contexte vide.
62/129 Chapitre 3. Déduction Naturelle
Nous notons Γ ` A le fait qu’il y a une preuve de A dans l’environnement Γ et Γ ` P : A le fait que P est une preuve de
A dans l’environnement Γ. Lorsque l’environnement est vide, nous l’omettons, autrement dit nous abrégeons 0/ ` A en ` A.
Lorsque nous demandons une preuve d’une formule sans indiquer d’environnement, nous supposons que l’environnement
est vide.
La preuve elle-même est ce qui figure dans la colonne preuve. Nous y avons ajouté la numérotation des lignes de
preuves, les justifications qui indiquent les règles utilisées et les contextes de chaque ligne de la preuve.
Nous présentons la même preuve sous forme d’arbre, ce qui correspond à l’approche originelle de Gerhard Gentzen.
Nous remarquons que pour lever une hypothèse il est d’usage de barrer cette hypothèse.
Exemple 3.1.12 Nous donnons la preuve de ¬A ∨ B dans l’environnement A ⇒ B. Nous suggérons de numéroter par i, ii,
iii, etc... les formules de l’environnement pour distinguer ces numéros et les numéros des lignes de la preuve.
environnement
référence formule
i A⇒B
contexte numéro preuve règle
1
2
3
4
5
6
7
8
9
10
3.2. Tactiques de preuve 63/129
Comme il a été rappelé dans les remarques préliminaires, nous considérons comme égales deux formules qui sont iden-
tiques quand nous éliminons leurs abréviations. Ainsi dans l’exemple précédent, nous avons identifié A ⇒ ⊥ et ¬A ainsi
que (¬A ∨ B) ⇒ ⊥ et ¬(¬A ∨ B).
10. Si A = B ∨C, alors prouver C sous l’hypothèse ¬B : soit P la preuve obtenue. « Supposons ¬B, P, Donc ¬B ⇒ C »
est une preuve de la formule ¬B ⇒ C qui est équivalente à A. Pour obtenir la preuve de A, il suffit d’ajouter la
preuve P1, demandé à l’exercice 59 page 68, de A dans l’environnement ¬B ⇒ C. La preuve obtenue de A est donc
« Supposons ¬B, P, Donc ¬B ⇒ C, P1 ».
11. Si ¬(B ∧C) est dans l’environnement, alors nous en déduisons ¬B ∨ ¬C par la preuve P3 demandée à l’exercice 59
page 68 puis nous raisonnons par cas comme ci-dessous :
— prouver A dans l’environnement où ¬B remplace ¬(B ∧C) : Soit P la preuve obtenue,
— prouver A dans l’environnement où ¬C remplace ¬(B ∧C) : Soit Q la preuve obtenue.
La preuve de A est « P3, Supposons ¬B, P, Donc ¬B ⇒ A, Supposons ¬C, Q, Donc ¬C ⇒ A, A ».
12. Si ¬(B ⇒ C) est dans l’environnement, alors nous déduisons B par la preuve P6, ¬C par la preuve P7 (preuves
demandées à l’exercice 59 page 68). Soit P la preuve de A dans l’environnement où B, ¬C remplacent la formule
¬(B ⇒ C). La preuve de A est « P6, P7, P ».
13. Si B ⇒ C est dans l’environnement et si C 6= ⊥, autrement dit si B ⇒ C n’est pas égale à ¬B, alors, nous déduisons
¬B ∨C dans l’environnement B ⇒ C par la preuve P2 demandée à l’exercice 59 page 68 puis nous raisonnons par
cas :
— prouver A dans l’environnement où ¬B remplace B ⇒ C : Soit P la preuve obtenue,
— prouver A dans l’environnement où C remplace B ⇒ C : Soit Q la preuve obtenue.
La preuve de A est « P2, Supposons ¬B, P, Donc ¬B ⇒ A, Supposons C, Q, Donc C ⇒ A, A ».
Exemple 3.2.1 Nous appliquons ces tactiques à la preuve de la loi de Peirce 1 : ((p ⇒ q) ⇒ p) ⇒ p. Cette formule n’est
pas prouvable en logique intuitionniste, qui est, ainsi qu’il est dit au début du chapitre, la logique classique privée de la
règle de réduction à l’absurde. Nous pouvons montrer, qu’en logique intuitionniste, cette formule est équivalente à la loi
du tiers-exclu.
Vu la forme de la formule, nous devons appliquer la tactique 5. La preuve de la formule de Peirce est donc de la forme
suivante :
Preuve Q :
Supposons (p ⇒ q) ⇒ p
Q1 preuve de p dans l’environnement (p ⇒ q) ⇒ p
Donc ((p ⇒ q) ⇒ p) ⇒ p
La preuve Q1 utilise nécessairement la tactique 13. Donc cette preuve s’écrit : Dans l’environnement B ⇒ C où B = p ⇒
q, C = p.
Preuve Q1 :
Q11 = P2 où P2 est la preuve de ¬B ∨C dans l’environnement B ⇒ C, voir exercice 59 page 68
Supposons ¬B
Q12 preuve de A = p dans l’environnement ¬B
Donc ¬B ⇒ A
Supposons C
Q13 preuve de A = p dans l’environnement C
Donc C ⇒ A
A
Pour obtenir une contradiction, donc une preuve de ⊥, il faut déduire p ⇒ q. Donc la preuve Q121 est :
Supposons p
⊥
q
Donc p ⇒ q
⊥
Théorème 3.3.1 (Cohérence de la déduction) Si une formule A est déduite d’un environnement de formules Γ (Γ ` A),
alors A est une conséquence de Γ (Γ |= A).
Preuve : Soit Γ un ensemble de formules. Soit P une preuve de A dans cet environnement. Soient Ci la conclusion et Hi le
contexte de la ième ligne de la preuve P. Nous posons H0 = 0,/ la liste vide. Si la preuve P est vide, nous posons C0 = A.
Notons par Γ, Hi l’ensemble des formules de l’ensemble Γ et de la liste Hi . Nous montrons par induction que pour tout k
nous avons Γ, Hk |= Ck , ce qui implique que pour la dernière ligne n de cette preuve, comme par définition Hn est la liste
vide et Cn = A, nous obtenons Γ |= A.
Cas de base : Supposons que A est déduite de Γ par la preuve vide. Alors A est élément de Γ, donc Γ |= A. Puisque
/ nous pouvons conclure : Γ, H0 |= A, donc Γ, H0 |= C0 .
H0 = 0,
Induction : Supposons que pour toute ligne i < k de la preuve nous avons Γ, Hi |= Ci . Montrons que Γ, Hk |= Ck .
Supposons que la ligne k est :
1. « Supposons Ck ». La formule Ck est la dernière formule de Hk , donc Γ, Hk |= Ck .
2. « Donc Ck ». La formule Ck est égale à la formule B ⇒ D, et B est la dernière formule de Hk−1 . Nous distinguons
deux cas, soit D est élément de Γ, soit D est utilisable sur la ligne précédente.
(a) Dans le premier cas, puisque D est égale à une formule de Γ, D est conséquence de Γ donc de Γ, Hk .
Puisque B ⇒ D est conséquence de D, il en résulte que Γ, Hk |= Ck
(b) Dans le deuxième cas, D est utilisable sur la ligne précédente. Donc il existe i < k tel que D = Ci et Hi
est préfixe de Hk−1 . Par hypothèse de récurrence, Γ, Hi |= D. Puisque Hi est préfixe de Hk−1 , nous avons
Γ, Hk−1 |= D. Puisque B est la dernière formule de Hk−1 , nous avons Hk−1 = Hk , B et donc Γ, Hk , B |= D,
ce qui implique Γ, Hk |= B ⇒ D. Enfin puisque Ck est égale à B ⇒ D et que deux formules égales sont
équivalentes, nous avons Γ, Hk |= Ck .
3. « Ck ». Cette formule est la conclusion d’une règle de la table 3.1 page 59, appliquée à ses prémisses utilisables
à la ligne précédente ou aux éléments de Γ. Considérons le seul cas de la règle ∧I, les autres cas étant analogues.
La formule Ck est égale à (D ∧ E) et les prémisses de la règle sont D et E. Puisque D et E sont éléments de Γ
ou utilisables à la ligne précédente, comme dans le cas précédent, en utilisant l’hypothèse de récurrence, nous
avons : Γ, Hk−1 |= D et Γ, Hk−1 |= E. Puisque la ligne k ne change pas les hypothèses, nous avons Hk−1 = Hk ,
donc Γ, Hk |= D et Γ, Hk |= E. Puisque Ck est égale à (D ∧ E), nous avons : D, E |= Ck . Par suite Γ, Hk |= Ck .
2
66/129 Chapitre 3. Déduction Naturelle
Remarque 3.4.2 Nous admettons ce thèorème dans ce polycopié. On peut en donner une preuve constructive, c’est-à-
dire qu’elle donne un ensemble complet de tactiques pour construire des preuves d’une formule dans un environnement.
Cependant ces tactiques peuvent donner des preuves longues. En particulier si nous devons prouver une formule (B ∨C),
il vaut mieux en général suivre les tactiques données au paragraphe 3.2 page 63, c’est-à-dire essayer de prouver B, puis
essayer de prouver C et seulement en cas d’échec, utiliser la tactique donnée dans la preuve de complétude, qui « réduit »
cette preuve à une preuve de C en ajoutant l’hypothèse ¬B.
3.5 Outils
Nous indiquons deux logiciels pour se familiariser avec la déduction naturelle. Le premier construit automatiquement
des preuves comme nous les avons présentées, le deuxième illustre sur quelques exemples de manière interactive comment
dessiner des preuves sous forme d’arbres.
[Link]
Ce logiciel se présente comme un jeu, il propose des formules à prouver et permet d’appliquer les règles de la déduction
naturelle, de manière interactive, pour en construire les arbres de preuve. Quand vous réussissez à construire la preuve
d’une formule, vous voyez la photo de Dag Prawitz, un des principaux logiciens qui a étudié les propriétés de la déduction
naturelle.
3.6. Exercices 67/129
3.6 Exercices
Exercice 52 (Brouillon de preuve) La suite de lignes suivante n’est pas un brouillon de preuve. Indiquer le numéro i de
la première ligne telle que les lignes 1 à i − 1 soient un brouillon de preuve et que les lignes 1 à i ne soient pas un brouillon
de preuve. Préciser le contexte des lignes 1 à i − 1.
Exercice 53 (Preuves de formules avec les règles spéciales) Donner une preuve pour les formules suivantes :
1. a ⇒ ¬¬a,
2. ¬¬a ⇒ a,
3. a ⇔ ¬¬a,
4. a ∨ ¬a.
Exercice 54 (Preuves simples de formules) Donner une preuve pour les formules suivantes :
1. a ⇒ c dans l’environnement a ⇒ b, b ⇒ c.
2. (a ⇒ b) ∧ (b ⇒ c) ⇒ (a ⇒ c).
3. (a ⇒ b) ⇒ ((b ⇒ c) ⇒ (a ⇒ c)).
Exercice 55 (Abréviations) Soient A une formule et d pl(A) la formule obtenue en remplaçant dans A, le vrai, les
négations et les équivalences (en forme abréviées) par leur définition. d pl(A) est la formule obtenue en « dépliant » A,
d’où le nom d pl choisi pour cette fonction de dépliage.
— Définir par récurrence la fonction d pl.
— Montrer que les formules A et d pl(A) sont équivalentes.
— En déduire que deux formules, égales aux abréviations près, sont équivalentes.
Exercice 56 (Preuves de formules) Donner une preuve pour les formules suivantes :
1. a ⇒ (b ⇒ a).
2. a ∧ b ⇒ a.
3. ¬a ⇒ (a ⇒ b).
4. (a ⇒ (b ⇒ c)) ⇒ ((a ⇒ b) ⇒ (a ⇒ c)).
5. a ∧ b ⇒ b ∧ a.
6. a ∨ b ⇒ b ∨ a.
7. (a ⇒ (b ⇒ c)) ⇒ (a ∧ b ⇒ c).
8. (a ∧ b ⇒ c) ⇒ (a ⇒ (b ⇒ c)).
68/129 Chapitre 3. Déduction Naturelle
9. (a ⇒ b) ∧ (c ⇒ d) ⇒ (a ∧ c ⇒ b ∧ d).
Exercice 57 (À propos de l’implication) Donner une preuve pour les formules suivantes :
1. (**) a ⇒ b dans l’environnement ¬a ∨ b.
2. (¬b ⇒ ¬a) ⇒ (a ⇒ b).
Exercice 58 (Algèbre de Boole) Donner une preuve pour les formules suivantes :
1. ¬(a ∧ ¬a).
2. a ∨ a ⇒ a.
3. a ∧ a ⇒ a.
4. a ∧ (b ∨ c) ⇒ a ∧ b ∨ a ∧ c.
5. a ∧ b ∨ a ∧ c ⇒ a ∧ (b ∨ c).
6. a ∨ b ∧ c ⇒ (a ∨ b) ∧ (a ∨ c).
7. (a ∨ b) ∧ (a ∨ c) ⇒ a ∨ b ∧ c.
Exercice 59 (Preuves de formules avec environnement) Donner une preuve des formules suivantes :
1. P1 : B ∨C dans l’environnement ¬B ⇒ C.
2. P2 : ¬B ∨C dans l’environnement B ⇒ C.
3. P3 : ¬B ∨ ¬C dans l’environnement ¬(B ∧C).
4. P4 : ¬B dans l’environnement ¬(B ∨C).
5. P5 : ¬C dans le même environnement ¬(B ∨C).
6. P6 : B dans l’environnement ¬(B ⇒ C).
7. P7 : ¬C dans le même environnement ¬(B ⇒ C).
Exercice 60 (Preuves de formules) Donner une preuve en déduction naturelle des formules suivantes :
1. ¬(a ∨ b) ⇒ (¬a ∧ ¬b).
2. (¬a ∧ ¬b) ⇒ ¬(a ∨ b).
3. (*) (¬a ∨ ¬b) ⇒ ¬(a ∧ b).
4. (**) (a ∨ b) ∧ (¬a ∨ b) ⇒ b.
5. (***) ¬(a ∧ b) ⇒ (¬a ∨ ¬b).
6. (***) (a ∨ b) ∧ (¬b ∨ c) ⇒ a ∨ c.
Exercice 61 (Partiel 2011) Prouver les formules suivantes en utilisant la déduction naturelle sous forme de tableau :
1. ¬p ∧ ¬(¬p ∧ q) ⇒ ¬q.
2. ((p ∨ q) ∨ (p ∨ r)) ∧ ¬p ⇒ q ∨ r.
3. (*) ¬p ∨ ¬(p ∧ q) ⇒ ¬q ∨ ¬p.
Exercice 62 (Partiel 2013) Donner une preuve des formules suivantes en utilisant la déduction naturelle sous forme de
tableau :
1. (p ∨ q) ⇒ (¬p ∧ ¬q) ⇒ r.
2. ((p ⇒ q) ∧ (q ⇒ r)) ∧ ¬r ⇒ ¬p.
3. (p ⇒ q) ⇒ ((p ∧ q) ∨ ¬p).
3.6. Exercices 69/129
Sommaire
4.1 Syntaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
4.1.1 Formules strictes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
4.1.2 Formules à priorité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
4.2 Être libre ou lié . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
4.2.1 Occurrences libres et liées . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
4.2.2 Variables libres et liées . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
4.3 Sens des formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
4.3.1 Déclaration de symbole . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
4.3.2 Signature . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
4.3.3 Interprétation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
4.3.4 Sens des formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
4.3.5 Modèle, validité, conséquence, équivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
4.3.6 Instanciation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
4.3.7 Interprétation finie . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
4.3.8 Substitution et remplacement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
4.4 Équivalences remarquables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
4.4.1 Relation entre ∀ et ∃ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
4.4.2 Déplacement des quantificateurs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
4.4.3 Changement de variables liées . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
4.5 Exercices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
que nous détaillerons dans cette seconde partie. Ce même raisonnement s’applique également pour prouver le syllogisme
suivant :
Malgré la conclusion qui semble contradictoire, le raisonnement est correct. Afin d’obtenir une contradiction il faut
ajouter l’hypothèse suivante : ∀x( bonmarché (x) ⇔ ¬ cher (x)). Ceci traduit la relation communément admise entre la
notion de bon marché et de cher, i.e., tout ce qui est cher n’est pas bon marché et réciproquement. Avec cette hypothèse
supplémentaire nous pouvons montrer que ce raisonnement est contradictoire, sans cette hypothèse le raisonnement est
correct. Ceci élucide le paradoxe de ce syllogisme.
Notre objectif dans ce chapitre est d’introduire les concepts et notions élémentaires de la logique du premier ordre afin
de pouvoir proposer des méthodes de raisonnement dans les chapitres suivants.
Plan : Nous commençons par décrire la syntaxe de la logique du premier ordre. Puis, nous définissons les notions
de libre et liée qui sont essentielles pour pouvoir interpréter le sens des formules. Ensuite nous définissons le sens des
formules que nous pouvons construire à partir de la syntaxe introduite précédemment. Enfin, nous énonçons des propriétés
remarquables de la logique du premier ordre, qui pourront être utilisées dans les raisonnements.
4.1 Syntaxe
Nous ajoutons à la logique propositionnelle deux symboles : le symbole existentiel (∃) et le symbole universel (∀). Le
symbole existentiel signifie qu’il existe un élément ayant une certaine propriété alors que le symbole universel permet de
parler de tous les éléments ayant une propriété. Ces changements impliquent qu’un élément de ce langage peut désormais
dépendre de plusieurs variables. Il faut donc rajouter dans la syntaxe un délimiteur de variables. Nous avons choisi clas-
siquement la virgule. Ces changements introduisent de nouveaux symboles en plus des variables, ces symboles peuvent
par exemple être des nombres sur lesquels nous pouvons créer des fonctions (comme l’addition) ou encore définir des
relations (comme l’égalité). Toutes ces modifications rendent la présentation de la syntaxe légèrement plus subtile que
celle de la logique propositionnelle.
Nous définissons en toute généralité la notion de terme qui est essentielle en logique du premier ordre. Nous étendrons
dans la suite cette notion en définissant ce qu’est un terme associé à un ensemble de symboles.
4.1. Syntaxe 75/129
n’est pas un terme. Notons que 42(1, y, 3) est aussi un terme, mais l’usage veut que les noms des fonctions et relations
soient des symboles ordinaires commençant par des lettres.
Définition 4.1.4 (Formule atomique) Nous définissons une formule atomique de manière inductive par :
— > et ⊥ sont des formules atomiques
— un symbole ordinaire est une formule atomique
— si t1 , . . . ,tn sont des termes et si s est un symbole (ordinaire ou spécial) alors s(t1 , . . . ,tn ) est une formule atomique.
Exemple 4.1.5
Exemple 4.1.9 Nous abrégeons le terme +(x, ∗(y, z)) en x + y ∗ z et ≤ (∗(3, x), +(y, 5)) en 3 ∗ x ≤ y + 5. La transformation
inverse est définie en donnant aux symboles =, 6=, <, ≤, >, ≥ des priorités inférieures à celle des symboles +, −, ∗, /.
O PÉRATIONS
−+ unaire
∗, / associatif gauche
+, − binaire associatif gauche
R ELATIONS
=, 6=, <, ≤, >, ≥
N ÉGATION , QUANTIFICATEURS
¬, ∀, ∃
C ONNECTEURS BINAIRES
∧ associatif gauche
∨ associatif gauche
⇒ associatif droit
⇔ associatif gauche
Exemple 4.1.11 La formule (à priorité) ∀xP(x) ∧ ∀xQ(x) ⇔ ∀x(P(x) ∧ Q(x)) peut être vue comme une abréviation de la
formule ((∀xP(x) ∧ ∀xQ(x)) ⇔ ∀x(P(x) ∧ Q(x))).
La formule (à priorité) ∀x∀y∀z(x ≤ y ∧ y ≤ z ⇒ x ≤ z) peut être vue comme une abréviation de la formule ∀x∀y∀z((≤
(x, y)∧ ≤ (y, z)) ⇒≤ (x, z)).
Exemple 4.1.12 La priorité du ∀ est plus forte que celle de ⇒, dans la formule ∀xP(x) ⇒ Q(y). Donc, l’opérande gauche
de l’implication est ∀xP(x). La structure de la formule sera ainsi représentée par l’arbre suivant :
~
∀x Q
P y
x
4.2. Être libre ou lié 77/129
De manière analogue à la logique propositionnelle, la taille d’une formule à priorité sera égale à la taille de la formule
stricte dont elle est l’abréviation. De même, pour les sous-formules, nous considérerons toujours la formule stricte dont la
formule à priorité est l’abréviation.
Définition 4.2.1 (Portée de liaison, occurrence libre, liée) Soient x une variable et A une formule. Dans une formule
∀x A ou ∃x A, la portée de la liaison pour x est A. Une occurrence de x dans une formule est libre si elle n’est pas dans la
portée d’une liaison pour x, sinon elle est dite liée.
Exemple 4.2.2 Pour voir les occurrences des variables, nous dessinons la structure de la formule ∀xP(x, y) ∧ ∃zR(x, z),
puisque la priorité de ∀ est supérieure à celle du ∧, nous obtenons :
L’occurrence de x présente dans P(x, y) est liée, l’occurrence de x présente dans R(x, z) est libre. L’occurrence de z
est liée.
Remarque 4.2.4 Une variable peut-être à la fois libre et liée. Par exemple, dans la formule ∀xP(x) ∨ Q(x), x est à la fois
libre et liée.
Remarque 4.2.5 Par définition, une variable qui n’apparaît pas dans une formule (0 occurrence) est une variable NON
libre de la formule.
Définition 4.3.1 (Déclaration de symbole) Une déclaration de symbole est un triplet noté sgn où s est un symbole, g est
soit f (pour fonction) ou r (pour relation), et n est un entier naturel dénotant le nombre d’arguments de ce symbole, n est
aussi appelé l’arité de s.
Exemple 4.3.2 Les fonctions d’arité 0 constituent les constantes, par exemple 1 et 2 sont des constantes d’arité nulle,
mais parent r2 est une notation signifiant que parent est employé comme relation d’arité 2. De même ∗ f 2 est une déclara-
tion annonçant que ∗ est une fonction 2-aire. Le symbole Ar0 est d’arité 0 et signifie que A est une variable proposition-
nelle. Le symbole hommer1 est d’arité 1 ou unaire et le symbole g f 2 est d’arité 2 ou 2-aire.
Remarque 4.3.3 Lorsque le contexte ou les conventions usuelles comportent une déclaration implicite d’un symbole,
nous omettons l’exposant. Par exemple, le symbole égal étant toujours employé comme relation à deux arguments, nous
abrégeons la déclaration de symbole =r2 en =.
4.3.2 Signature
En logique du premier ordre nous pouvons choisir le nom des variables utilisées mais nous avons aussi la possibilité
de construire nos propres constantes (fonctions sans arguments), fonctions, variables propositionnelles (relations d’arité
nulle) et relations. Une signature est donc l’ensemble des déclarations de symboles autorisés pour construire des formules.
Elle permet de définir les symboles dont le sens n’est pas fixé a priori, contrairement par exemple aux constantes > et ⊥
dont le sens est toujours fixé respectivement à 1 et 0.
Définition 4.3.4 (Signature, constante, symbole de fonction, variable propositionnelle, et relation) Une signature Σ est
un ensemble de déclarations de symboles de la forme sgn . Soient n un entier strictement positif et Σ une signature, le sym-
bole s est :
1. une constante de la signature si et seulement si s f 0 ∈ Σ
2. un symbole de fonction à n arguments de la signature, si et seulement si s f n ∈ Σ
3. une variable propositionnelle de la signature si et seulement si sr0 ∈ Σ
4. un symbole de relation à n arguments de la signature, si et seulement si srn ∈ Σ
Au lieu de dire 0 f 0 , 1 f 0 , + f 2 , ∗ f 2 , =r2 est une signature pour l’arithmétique, nous disons plus simplement qu’une
signature possible pour l’arithmétique comporte 0, 1, + (à deux arguments), ∗ et =. Sur cet exemple, nous devons préciser
que le symbole plus est utilisé avec deux arguments (car nous pouvons aussi rencontrer le symbole plus avec un seul
argument).
Exemple 4.3.5 Une signature possible pour la théorie des ensembles est ∈, =. Notons que toutes les autres opérations
sur les ensembles peuvent être définies à partir de ces deux symboles.
Nous définissons maintenant les termes associés à une signature. Nous considérons un ensemble dénombrable de
variables disjoint de l’ensemble de symboles de la signature.
Définition 4.3.8 (Terme sur une signature) Soit Σ une signature, un terme sur Σ est :
— soit une variable,
— soit une constante s où s f 0 ∈ Σ,
4.3. Sens des formules 79/129
— soit un terme de la forme s(t1 , . . . ,tn ), où n ≥ 1, s f n ∈ Σ et t1 , . . . ,tn sont des termes sur Σ.
Définition 4.3.9 (Formule atomique sur une signature) Soit Σ une signature, une formule atomique sur Σ est :
— soit une des constantes >, ⊥,
— soit une variable propositionnelle s où sr0 ∈ Σ,
— soit de la forme s(t1 , . . . ,tn ) où n ≥ 1, srn ∈ Σ et où t1 , . . . ,tn sont des termes sur Σ.
Définition 4.3.10 (Formule sur une signature) Une formule sur une signature Σ est une formule, dont les sous-formules
atomiques sont des formules atomiques sur Σ (au sens de la définition 4.3.9).
Exemple 4.3.11 ∀x (p(x) ⇒ ∃y q(x, y)) est une formule sur la signature Σ = {pr1 , qr2 , h f 1 , c f 0 }. Mais c’est aussi une
formule sur la signature Σ0 = {pr1 , qr2 }, puisque les symboles h et c ne figurent pas dans la formule.
Définition 4.3.12 (Signature associée à une formule) La signature associée à une formule est la plus petite signature Σ
telle que la formule est élément de FΣ , c’est la plus petite signature permettant d’écrire la formule.
Exemple 4.3.13 La signature Σ associée à la formule ∀x (p(x) ⇒ ∃y q(x, y)) est Σ = {pr1 , qr2 }.
Définition 4.3.14 (Signature associée à un ensemble de formules) La signature associée à un ensemble de formules est
l’union des signatures associées à chaque formule de l’ensemble.
Exemple 4.3.15 La signature Σ associée à l’ensemble constitué des deux formules ∀x(p(x) ⇒ ∃y q(x, y)), ∀u ∀v (u +
s(v) = s(u) + v) est Σ = {pr1 , qr2 , + f 2 , s f 1 , =r2 }.
4.3.3 Interprétation
En logique propositionnelle, le sens des formules est uniquement fixé par les valeurs des variables, en logique du
premier ordre le sens des formules dépend aussi du sens des fonctions et des relations. Le sens des fonctions et des
relations est fixé par une interprétation.
Définition 4.3.16 (Interprétation) Une interprétation I sur une signature Σ est définie par un domaine D non vide et une
gn
application qui à chaque déclaration de symbole sgn ∈ Σ associe sa valeur sI comme suit :
f0
1. sI est un élément de D.
fn
2. sI où n ≥ 1 est une fonction de Dn dans D, autrement dit une fonction à n arguments.
3. sr0
I vaut 0 ou 1.
4. srn n
I où n ≥ 1 est un sous-ensemble de D , autrement dit une relation à n arguments.
Exemple 4.3.17 Soit l’interprétation I de domaine D = {1, 2, 3} où la relation binaire ami est vraie pour les couples
(1, 2), (1, 3) et (2, 3), c’est-à-dire, amir2
I = {(1, 2), (1, 3), (2, 3)}. ami(2, 3) est vraie dans l’interprétation I. En revanche,
ami(2, 1) est fausse dans l’interprétation I.
Remarque 4.3.18 Dans toute interprétation I, la valeur du symbole = est l’ensemble {(d, d) | d ∈ D}, autrement dit dans
toute interprétation le sens de l’égalité est l’identité sur le domaine de l’interprétation.
f1 f1 f1 f1
— cI (0) = 1, cI (1) = 0, cI (2) = 2. Notons que la fonction cI a comme domaine D, ce qui oblige à définir artifi-
f1
ciellement cI (2) : Claude, dénoté par 2, n’a ni copain, ni copine.
Définition 4.3.20 (Interprétation d’un ensemble de formules) L’interprétation d’un ensemble de formules est une in-
terprétation qui définit seulement le sens de la signature associée à l’ensemble des formules.
Définition 4.3.21 (État) Un état e d’une interprétation est une application de l’ensemble des variables dans le domaine
de l’interprétation.
Définition 4.3.22 (Assignation) Une assignation est un couple (I, e) composé d’une interprétation I et d’un état e.
Exemple 4.3.23 Soient le domaine D = {1, 2, 3} et l’interprétation I où la relation binaire ami est vraie uniquement
pour les couples (1, 2), (1, 3) et (2, 3), c’est-à-dire, amir2
I = {(1, 2), (1, 3), (2, 3)}. Soit e l’état qui associe 2 à x et 1 à y.
L’assignation (I, e) rend la relation ami(x, y) fausse.
Remarque 4.3.24 La valeur d’une formule ne dépend que de ses variables libres et de ses symboles, aussi pour évaluer
une formule sans variable libre, l’état des variables est inutile. Nous avons alors deux possibilités :
— Pour une formule sans variables libres, il suffit de donner une interprétation I des symboles de la formule. Dans
ce cas, les assignations (I, e) et (I, e0 ) donnerons la même valeur à la formule pour tous états e et e0 . Ainsi pour
tout état e, nous identifierons (I, e) et I. Selon le contexte, I sera considéré comme soit une interprétation soit une
assignation dont l’état est quelconque.
— Pour une formule avec des variables libres, nous avons donc besoin d’une assignation.
Soient Σ une signature, I une interprétation sur Σ de domaine D et e un état de cette interprétation. Nous souhaitons
connaître la valeur (0 ou 1) de toute formule A sur Σ dans l’assignation (I, e). Cette valeur sera notée [A](I,e) . Pour cela,
nous avons tout d’abord besoin de définir le sens de chaque terme t sur Σ dans l’assignation (I, e), noté JtK(I,e) . Ensuite
nous devons fixer le sens de chaque formule atomique B sur Σ dans la même assignation, noté [B](I,e) .
Définition 4.3.25 ( Évaluation) Nous donnons la définition inductive de l’évaluation d’un terme t :
1. si t est une variable, alors JtK(I,e) = e(t),
f0
2. si t est une constante alors JtK(I,e) = tI ,
fn
3. si t = s(t1 , . . . ,tn ) où s est un symbole et t1 , . . . ,tn sont des termes, alors JtK(I,e) = sI (Jt1 K(I,e) , . . . , Jtn K(I,e) ).
Dans les exemples, nous remplaçons les variables par leurs valeurs, nous confondons les symboles et leur sens.
Remarque 4.3.28 Nous devons distinguer entre évaluer un terme J K et évaluer une formule atomique [ ], car dans notre
présentation, ces deux catégories syntaxiques ne sont pas disjointes, car s(t1 , . . . ,tn ) peut être l’application d’une fonction
(JK) ou d’une relation ([ ]). Mais quand le contexte est sans ambiguïté, nous pouvons omettre cette distinction.
— [a(Anne,Claude)]I =
— [a(y, c(y))](I,e) =
Attention à distinguer (suivant le contexte), les éléments du domaine 0, 1 et les valeurs de vérité 0, 1. Les exemples suivants
mettent en évidence l’interprétation de l’égalité comme une identité. Dans l’interprétation I, nous avons :
— [(Anne = Bernard)]I =
— [(c(Anne) = Anne)]I =
— [(c(c(Anne)) = Anne)]I =
Définition 4.3.30 (Sens des formules) Le sens des formules est donné par :
1. Les connecteurs propositionnels ont le même sens qu’en logique propositionnelle. Soient B et C des formules,
rappelons uniquement le sens de l’implication : si [B](I,e) = 0 alors [(B ⇒ C)](I,e) = 1 sinon [(B ⇒ C)](I,e) = [C](I,e) .
82/129 Chapitre 4. Logique du premier ordre
2. Soient x une variable et B une formule. [∀xB](I,e) = 1 si et seulement si [B](I, f ) = 1 pour tout état f identique à e,
sauf pour x. Soit d ∈ D. Notons e[x = d] l’état identique à l’état e, sauf pour la variable x, auquel l’état e[x = d]
associe la valeur d. La définition ci-dessus peut être mise sous la forme suivante :
Exemple 4.3.31 Soit l’interprétation I de domaine D = {1, 2, 3} où la relation binaire ami est vraie pour les couples
(1, 2), (1, 3) et (2, 3), c’est-à-dire, amir2
I = {(1, 2), (1, 3), (2, 3)}. La formule ami(1, 2) ∧ ami(2, 3) ⇒ ami(1, 3) est vraie
dans l’interprétation I, i.e., [ami(1, 2) ∧ ami(2, 3) ⇒ ami(1, 3)]I = 1.
Exemple 4.3.32 Utilisons l’interprétation I donnée dans l’exemple 4.3.19 page 79. D’après le sens du quantificateur
existentiel, nous devons évaluer a(x, x) pour x = 0, x = 1, et x = 2. Nous simplifions ce calcul et les calculs suivants en
remplaçant immédiatement les variables par leurs valeurs : cela nous évite d’utiliser les états.
— [∃x a(x, x)]I =
— [∀x∃y a(x, y)]I = min{max{[a(0, 0)]I , [a(0, 1)]I , [a(0, 2)]I }, max{[a(1, 0)]I , [a(1, 1)]I , [a(1, 2)]I }, max{[a(2, 0)]I ,
[a(2, 1)]I , [a(2, 2)]I }} = min{max{0, 1, 0}, max{1, 0, 0}, max{1, 0, 0}} = min{1, 1, 1} = 1.
D’après la définition, nous avons : [∀x∃y a(x, y)]I = ([a(0, 0)]I + [a(0, 1)]I + [a(0, 2)]I ). ([a(1, 0)]I + [a(1, 1)]I +
[a(1, 2)]I ). ([a(2, 0)]I + [a(2, 1)]I + [a(2, 2)]I ) = (0 + 1 + 0).(1 + 0 + 0).(1 + 0 + 0) = 1.1.1 = 1.
— [∃y∀x a(x, y)]I =
Remarque 4.3.33 Dans l’interprétation ci-dessus, les formules ∀x∃y a(x, y) et ∃y∀x a(x, y) n’ont pas la même valeur.
Donc en intervertissant un quantificateur existentiel et un quantificateur universel, nous ne préservons pas le sens des
formules.
4.3.6 Instanciation
Définition 4.3.34 (Instanciation) Soit x une variable, t un terme et A une formule.
1. A<x := t> est la formule obtenue en remplaçant dans la formule A toute occurrence libre de x par le terme t.
4.3. Sens des formules 83/129
2. Le terme t est libre pour x dans A si les variables de t ne sont pas liées dans les occurrences libres de x dans A.
Exemple 4.3.35 Le terme z est libre pour x dans la formule ∃yp(x, y). Par contre le terme y, comme tout terme comportant
la variable y, n’est pas libre pour x dans cette formule. Soit A la formule (∀xP(x) ∨ Q(x)), la formule A<x := b> vaut
Théorème 4.3.36 Soient A une formule et t un terme libre pour la variable x dans A. Soient I une interprétation et e un
état de l’interprétation. Nous avons [A<x := t>](I,e) = [A](I,e[x=d]) , où d = JtK(I,e) .
Autrement dit, la valeur de A<x := t> dans une assignation est la même que celle de A dans une assignation identique,
sauf qu’elle donne à x la valeur du terme t. Ce théorème, dont le résultat est évident, peut être prouvé par une récurrence
(que nous ne ferons pas) sur la taille des formules. Nous montrons seulement que la condition sur t est indispensable en
observant un exemple où cette condition n’est pas respectée.
Exemple 4.3.37 Soient I l’interprétation de domaine {0, 1} avec pI = {(0, 1)} et e, un état où y = 0. Soient A la formule
∃yp(x, y) et t le terme y. Ce terme n’est pas libre pour x dans A. Nous avons :
— A<x := y>=
et [A<x := y>](I,e) =
— Soit d = JtK(I,e) = JyK(I,e) = 0. Dans l’assignation (I, e[x = d]), nous avons x = 0. Donc, nous obtenons :
[A](I,e[x=d]) =
Théorème 4.3.41 Soient n un entier et A une formule ne comportant que des représentations d’entiers de valeur inférieure
à n. Soit A0 la n-expansion de A. Toute interprétation de domaine {0, . . . , n − 1} attribue la même valeur à A et à A0 .
La condition sur A est nécessaire car si A comporte une représentation d’un entier au moins égal à n, la valeur de cette
représentation ne sera pas dans le domaine de l’interprétation. La preuve du théorème est une récurrence sur la taille des
formules, que nous ne ferons pas. Nous nous contentons de montrer que l’élimination d’un quantificateur universel de la
formule ∀xB conserve la valeur de cette formule.
Soient (I, e) une interprétation et un état de domaine {0, . . . , n − 1} donnant à la représentation d’un entier, la valeur
de l’entier représenté. Par définition du sens du quantificateur universel : [∀xB](I,e) = ∏i<n [B](I,e[x=i]) . D’après le théo-
rème 4.3.36 page précédente et le fait que la valeur de la représentation de l’entier i est i, nous avons : [B](I,e[x=i]) = [B<
x := i>](I,e) . Par suite : [∀xB](I,e) = ∏i<n [B<x := i>](I,e) = [∏i<n B<x := i>](I,e) .
De l’assignation à l’interprétation.
Théorème 4.3.42 Soit v une assignation propositionnelle de P dans {0, 1} alors il existe une interprétation I de A telle
que [A]I = [A]v .
Preuve : Soit v une assignation propositionnelle de P dans {0, 1}. Soit I l’interprétation suivante de A :
1. Domaine : {0, . . . , n − 1}
2. sr0
I = v(s) si et seulement si s ∈ P
rp
3. Soit p ≥ 1 et srp un symbole de relation de A . Alors sI = {(k1 , . . . , k p )|s(k1 , . . . , k p ) ∈ P et v(s(k1 , . . . , k p )) = 1}
Par définition de I, l’assignation v et l’interprétation I donnent la même valeur aux sous-formules atomiques de A, donc
(par récurrence sur les formules) la même valeur à la formule A. 2
Exemple 4.3.43 L’assignation v, définie par p(0) = 1 et p(1) = 0, donne la valeur 0 à la formule suivante :
(p(0) + p(1)) ⇒ (p(0).p(1)).
Donc I définie par pI = {0} donne aussi la valeur 0 à cette même formule. Cet exemple montre que v et I sont deux façons
analogues de présenter une interprétation, la deuxième étant souvent plus concise.
De l’interprétation à l’assignation.
Théorème 4.3.44 Soit I une interprétation de A alors il existe une assignation v de P telle que
[A]I = [A]v .
Preuve : Soient I une interprétation de A et v l’assignation propositionnelle suivante de P dans {0, 1} : pour tout B ∈ P,
v(B) = [B]I . Par définition de v, l’assignation v et l’interprétation I donnent la même valeur aux sous-formules atomiques
de A, donc la même valeur à la formule A. 2
4.3. Sens des formules 85/129
Formule fermée sans symbole de fonction : Soit A une formule fermée sans symbole de fonction ni constantes, sauf des
représentations d’entiers de valeur inférieure à n. Pour trouver une interprétation I modèle de A de domaine {0, . . . , n − 1}
donnant à la représentation d’un entier, la valeur de l’entier représenté, nous procédons ainsi :
1. Supposons qu’il n’y ait pas d’assignation propositionnelle modèle de C, mais que A ait un modèle I. D’après le
théorème 4.3.41 page ci-contre, I est modèle de B, donc de C, et d’après le théorème 4.3.44 page précédente, il y
a une assignation propositionnelle modèle de C. De cette contradiction, nous déduisons que A n’a pas de modèle
à n éléments.
2. Supposons que l’assignation propositionnelle v soit modèle de C. Donc, l’interprétation I construite comme il est
indiqué dans le théorème 4.3.42 page ci-contre est modèle de C, donc elle est modèle de B, donc aussi d’après le
théorème 4.3.41 page précédente, elle est modèle de A.
Exemple 4.3.45 Soit A la formule ∃xP(x) ∧ ∃x¬P(x) ∧ ∀x∀y(P(x) ∧ P(y) ⇒ x = y). Il est clair que cette formule n’a pas
de modèle à un élément car cet élément devrait vérifier à la fois la propriété P et sa négation. La 2-expansion de A est :
Formule fermée avec symbole de fonction : Soit A une formule fermée pouvant comporter des représentations d’en-
tiers de valeur inférieure à n. Comme dans le cas précédent, nous remplaçons A par son expansion, nous supprimons les
égalités. Puis, nous énumérons les choix des valeurs des symboles comme dans l’algorithme DPLL, en propageant le plus
possible chacun des choix effectués.
Exemple 4.3.46 Soit A la formule ∃y P(y) ⇒ P(a), dont nous cherchons un contre-modèle à 2 éléments (cela revient au
même que de trouver un modèle de la négation de A).
86/129 Chapitre 4. Logique du premier ordre
Exemple 4.3.47 Nous cherchons un modèle à 2 éléments des formules P(a), ∀x(P(x) ⇒ P( f (x))), ¬P( f (b)).
2. ∀xA ≡ ¬∃x¬A.
3. ¬∃xA ≡ ∀x¬A.
4. ∃xA ≡ ¬∀x¬A.
Prouvons les deux premières identités, les deux autres sont données en exercice 78 page 92 :
1. Soient I une interprétation de domaine D et e un état.
[¬∀xA](I,e) ≡ 1 − [∀xA](I,e)
≡ 1 − ∏d∈D [A](I,e[x=d]) d’après le sens de ∀
≡ ∑d∈D 1 − [A](I,e[x=d]) par les lois de De Morgan généralisées
≡ ∑d∈D [¬A](I,e[x=d]) par définition du sens de ¬
≡ [∃x¬A](I,e) par définition du sens de ∃
En examinant de façon critique cette preuve, nous voyons qu’elle utilise la loi de De Morgan généralisée, qui
est l’expression dans un autre formalisme d’une loi analogue. Il faut donc formaliser l’usage des quantificateurs
pour échapper à ces preuves qui ne sont en fait que des changements de notations. Nous le ferons en ajoutant à la
déduction naturelle des règles qui gouvernent les quantificateurs.
2. Les autres équivalences sont prouvables à partir de la première par le principe de remplacement. Nous ne prouvons
que la deuxième identité :
∀xA ≡ ¬¬∀xA identité de la double négation
≡ ¬∃x¬A par l’identité 1 page précédente
Exemple 4.4.2 Nous éliminons de ces deux formules les quantificateurs inutiles :
— ∀x∃xP(x) ≡
— ∀x(∃xP(x) ∨ Q(x)) ≡
Exemple 4.4.4 La formule ∀x p(x, z) est équivalente à la formule ∀y p(y, z) (d’après le théorème ci-dessus) mais elle
n’est pas équivalente à la formule ∀z p(z, z), où le changement de variable ne respecte pas les conditions du théorème.
88/129 Chapitre 4. Logique du premier ordre
Définition 4.4.5 (Formules égales à un changement près de variables liées) Deux formules sont égales à un change-
ment près de variables liées si nous pouvons obtenir l’une à partir de l’autre par des remplacements de sous-formules
de la forme QxA par QyA<x := y> où Q est un quantificateur et y est une variable qui ne figure pas dans QxA. Deux
formules égales à un changement près de variables liées, sont dites aussi copies l’une de l’autre ou encore α-équivalentes.
Théorème 4.4.6 Si deux formules sont égales à un changement près de variables liées alors elles sont équivalentes.
Ce résultat est clairement une conséquence du théorème 4.4.3 page précédente. Nous n’en ferons pas la preuve, qui est
longue et fastidieuse. Nous nous contentons de suggérer cette preuve à l’aide d’un exemple.
Exemple 4.4.7 Nous montrons que les formules ∀x∃yP(x, y) et ∀y∃xP(y, x) sont égales par changement des variables
liées, au sens de la définition 4.4.3 page précédente donc sont équivalentes, en effet :
Notre définition de l’égalité entre deux formules à un changement près de variables liées n’est pas pratique, car la
définition ne donne pas un test. Or il est simple de voir si deux formules sont égales à un changement près de variables
liées : nous traçons des traits entre chaque quantificateur et les variables qu’il lie et nous effaçons les noms des variables
liées. Si après cette transformation, les deux formules deviennent identiques, c’est qu’elles sont égales à un changement
près des variables liées.
Exemple 4.4.8 Les deux formules ∀x∃yP(y, x) et ∀y∃xP(x, y) sont transformées en ∀|∃|P(|, |).
4.5. Exercices 89/129
4.5 Exercices
Exercice 64 (Structure et variables libres)
Pour chaque formule ci-dessous, indiquer sa structure et ses variables libres.
1. ∀x(P(x) ⇒ ∃yQ(x, y)).
2. ∀a∀b(b 6= 0 ⇒ ∃q∃r(a = b ∗ q + r ∧ r < b)) 4 .
3. Pair(x) ⇔ ∃y(x = 2 ∗ y).
4. x Divise y ⇔ ∃z(y = z ∗ x).
5. Premier(x) ⇔ ∀y(y Divise x ⇒ y = 1 ∨ y = x).
Exercice 65 (Formalisation, symbole de fonction et de relation) Nous considérons Σ = { f r2 , or2 , cr2 , jr2 , r f 0 , p f 1 } la
signature ayant la sémantique donnée ci-dessous.
— f (x, y) : x est frère de y.
— o(x, y) : x est l’oncle de y.
— c(x, y) : x est le cousin de y.
— j(x, y) : x est plus jeune que y.
— r est le diminutif de Robert.
— p(x) est le père de x.
Exprimer en logique du premier ordre et en utilisant la signature Σ les phrases suivantes :
1. Tout frère du père de Robert est un oncle de Robert.
2. Si les pères de deux enfants sont des frères alors ces deux enfants sont des cousins.
3. Robert a un cousin plus jeune qu’un des frères de Robert.
Exprimer en français les propositions logiques suivantes :
1. 6 ∃x j(p(x), x)
2. ∀x∀y(p(p(x)) = p(p(y)) ⇒ c(x, y))
3. ∀x∃y( f (x, y) ∧ j(x, y))
4. ∃x∃y( f (x, y) ∧ ¬(p(x) = p(y)))
Exercice 66 (Formalisation) Considérons la signature Σ = {a f 0 , f f 0 , J r2 , Gr2 }, où les symboles ont le sens donné ci-
dessous.
— a : l’équipe d’Allemagne.
— f : l’équipe de France.
— J(x, y) : x a joué un match contre y.
— G(x, y) : x a gagné contre y.
Exprimer en logique du premier ordre en utilisant la signature Σ les assertions suivantes :
1. L’équipe de France a gagné un match et en a perdu un.
2. L’équipe de France et l’équipe d’Allemagne ont fait match nul.
3. Une équipe a gagné tous ses matchs.
4. Aucune équipe n’a perdu tous ses matchs.
5. Considérons l’assertion suivante : « Tous ceux qui ont joué contre une équipe qui a gagné tous ses matchs, ont
gagné au moins un match ». Parmi les formules suivantes, lesquelles expriment la phrase ci-dessus, et lesquelles
sont équivalentes ?
(a) ∀x∃y (J(x, y) ∧ ∀z(J(y, z) ⇒ G(y, z)) ⇒ ∃vG(x, v)).
(b) ∀x(∃y (J(x, y) ∧ ∀z(J(y, z) ⇒ G(y, z))) ⇒ ∃vG(x, v)).
(c) ∃x(∀y (J(x, y) ⇒ G(x, y)) ⇒ ∀z(J(x, z) ⇒ ∃vG(x, v))).
(d) ∀x∀y (J(x, y) ∧ ∀z(J(y, z) ⇒ G(y, z)) ⇒ ∃vG(x, v)).
(e) ∀x(∀y (J(x, y) ∧ ∀z(J(y, z) ⇒ G(y, z))) ⇒ ∃vG(x, v)).
4. Afin de respecter la notation usuelle pour la division euclidienne nous prenons exceptionnellement a, b, q et r comme nom de variable.
90/129 Chapitre 4. Logique du premier ordre
Exercice 67 (Formaliser,**) Soient les constantes s pour Serge, t pour Tobby et les symboles de relation A(x, y), x aime
y, C(x), x est un chien, D(x), x est un animal domestique, E(x), x est un enfant, O(x), x est un oiseau et P(x, y), x a peur
de y, donner la signature Σ associée à ces symboles. Formaliser en logique du premier ordre en utilisant Σ les énoncés
suivants :
1. Les chiens et les oiseaux sont des animaux domestiques.
2. Tobby est un chien qui aime les enfants.
3. Les oiseaux n’aiment pas les chiens.
4. Serge aime tous les animaux domestiques sauf les chiens.
5. Tous les enfants n’ont pas peur des chiens.
6. Certains chiens aiment les enfants.
7. Certains chiens aiment les enfants et réciproquement.
8. Les enfants aiment certains chiens.
Exercice 68 (Évaluer des prédicats unaires) Soit I l’interprétation de domaine D = {0, 1} telle que PI = {0}, QI = {1}.
1. Évaluer dans cette interprétation les formules ∀xP(x) et ∀x(P(x) ∨ Q(x)).
2. Les formules ∀xP(x) ∨ ∀xQ(x) et ∀x(P(x) ∨ Q(x)) sont-elles équivalentes ?
3. Évaluer dans cette interprétation les formules ∃xP(x) et ∃x(P(x) ∧ Q(x)).
4. Les formules ∃xP(x) ∧ ∃xQ(x) et ∃x(P(x) ∧ Q(x)) sont-elles équivalentes ?
5. Évaluer dans cette interprétation les formules ∀x(P(x) ⇒ Q(x)) et ∀xP(x) ⇒ ∀xQ(x).
6. Les deux formules ∀x(P(x) ⇒ Q(x)) et ∀xP(x) ⇒ ∀xQ(x) sont-elles équivalentes ?
Exercice 70 (Prédicat unaire et égalité) Soit I l’interprétation de domaine D = {0, 1, 2} telle que : PI = {0, 1}, QI =
{1, 2}, RI = {}. Évaluer dans cette interprétation les formules suivantes :
1. ∃xR(x).
2. ∀x(P(x) ∨ Q(x)).
3. ∀x(P(x) ⇒ Q(x)).
4. ∀x(R(x) ⇒ Q(x)).
5. ∃x(P(x) ∧ ∀y(P(y) ⇒ x = y)) 5 .
5. Cette formule signifie qu’il y a un et un seul élément vérifiant P.
4.5. Exercices 91/129
Exercice 71 (Évaluation, égalité) Nous utilisons le symbole de fonction unaire f et la constante a. Nous abrégeons
¬(x = y) en x 6= y. Soient I1 , I2 les interprétations suivantes de domaine {0, 1, 2} : aI1 = aI2 = 0.
Exercice 73 (Expansion et contre-modèle) Trouver, par la méthode des expansions, des contre-modèles des formules
suivantes :
1. ∃xP(x) ⇒ ∃x(P(x) ∧ Q(x)).
2. ∀x(P(x) ⇒ Q(x)) ⇒ ∃xQ(x).
3. ∀x(P(x) ⇒ Q(x)) ⇒ (∃xP(x) ⇒ ∀xQ(x)).
4. (∃xF(x) ⇒ ∃xG(x)) ⇒ ∀x(F(x) ⇒ G(x)).
5. ∀x∃yR(x, y) ⇒ ∃xR(x, x).
6. ∀x∀y(R(x, y) ⇒ R(y, x)) ⇒ ∀xR(x, x).
Indication : il suffit de construire des 1 ou 2 expansions.
1. ∃xP(x).
2. ∃xQ(x).
3. ∀x(P(x) ∧ Q(x) ⇒ R(x)).
Montrer, en utilisant la méthode des expansions, qu’il est incorrect de déduire à partir de ces trois hypothèses la conclu-
sion suivante : ∃xR(x).
Exercice 75 (Contre-modèles avec relation) Construire des contre-modèles des formules suivantes, où F est une rela-
tion :
1. ∀x∃y(x = y) ⇒ ∃y∀x(y = x).
2. F(a) ∧ (a 6= b) ⇒ ¬F(b).
3. ∃x∃y(F(x) ∧ F(y) ∧ x 6= y) ⇒ ∀xF(x).
4. ∀x∀y(F(x, y) ⇒ x = y) ⇒ ∃xF(x, x).
Exercice 76 (Contre-modèles avec fonction) Construire, en utilisant la méthode des expansions, des contre-modèles
des formules suivantes, où f est une fonction et P une relation :
1. ∀y∃x( f (x) = y).
2. ∀x∀y( f (x) = f (y) ⇒ x = y).
3. ∃x∀y( f (y) = x).
4. ∀x(P(x) ⇒ P( f (x)).
Exercice 78 (, Preuve,*) Prouver les deux équivalences suivantes du lemme 4.4.1 page 86 :
— ¬∃xA ≡ ∀x¬A.
— ∃xA ≡ ¬∀x¬A.
Conseil : utiliser les propriétés 1 page 86 et 2 page 87 du lemme 4.4.1 page 86.
Exercice 79 (Preuve) Nous savons que (∀x(A ∧ B)) ≡ (A ∧ (∀xB)) à la condition que x ne soit pas une variable libre de
A comme il est dit au paragraphe 4.4.2 page 87. Montrer que cette condition est nécessaire en donnant une assignation
qui donne des valeurs différentes aux deux formules ∀x(P(x) ∧ Q(x)) et P(x) ∧ (∀xQ(x)).
Chapitre 5
Sommaire
5.1 Méthode de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
5.1.1 Domaine et base de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
5.1.2 Interprétation de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
5.1.3 Théorème de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
5.2 Skolémisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
5.2.1 Algorithme de skolémisation d’une formule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
5.2.2 Propriétés de la forme de Skolem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
5.2.3 Forme clausale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
5.3 Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
5.3.1 Unificateur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
5.3.2 Algorithme d’unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
5.4 Résolution au premier ordre . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
5.4.1 Trois règles pour la résolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
5.4.2 Cohérence de la résolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
5.4.3 Complétude de la résolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
5.5 Outil logiciel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110
5.6 Exercices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
I L est important de préciser que la logique du premier ordre est indécidable, cela signifie qu’il n’existe pas d’algorithme
pour déterminer si une formule est valide ou non valide. Ce résultat fut établi par Alonzo Church et Alan Türing en
1936 et 1937 [4, 24]. Ils ont aussi montré que cette logique est semi-décidable, c’est-à-dire que nous pouvons écrire un
programme, qui prend en entrée une formule et qui a le comportement suivant :
1. S’il termine alors il décide correctement si la formule est valide ou non. Lorsque la formule est valide, la décision
est généralement accompagnée d’une preuve.
2. Si la formule est valide, alors il termine. Cependant, l’exécution peut être longue !
Notons que si la formule n’est pas valide, la terminaison de ce programme n’est pas garantie. En effet si le programme
terminait pour toute formule, alors, d’après le premier point, ce serait un algorithme pour déterminer si une formule est
valide ou non. Or, ainsi qu’il est dit ci-dessus, Church et Türing ont prouvé qu’un tel algorithme n’existait pas.
Plan : Dans ce chapitre nous commençons par présenter la méthode, introduite par Jacques Herbrand, permettant d’énu-
mérer un ensemble fini de formules afin de trouver un modèle à une formule. Ensuite nous présentons la transformation
due à Thoralf Albert Skolem qui transforme (skolémise) une formule en une « forme de Skolem » où l’existence d’un
modèle est préservée. En transformant ensuite cette forme de Skolem en une « forme clausale » équivalente, nous pou-
vons appliquer la résolution. Nous reprenons alors le concept de résolution introduit dans le chapitre 2 page 37 et nous
l’étudions en logique du premier ordre. En 1929, Kurt Gödel (1906 - 1978) prouva que la logique du premier ordre est
complète et cohérente. Nous présentons ce résultat pour la résolution, c’est-à-dire qu’il existe une preuve par résolution
en logique du premier ordre d’une formule F à partir d’un ensemble de formules Γ si et seulement si F est conséquence
de Γ.
94/129 Chapitre 5. Base de la démonstration automatique
Définition 5.1.1 (Fermeture universelle) Soit C une formule ayant pour variables libres x1 , . . . , xn . La fermeture univer-
selle de C, notée ∀(C), est la formule ∀x1 . . . ∀xnC. Cette notion est définie à l’ordre près des variables libres de C. Soit Γ
un ensemble de formules, ∀(Γ) = {∀(A) | A ∈ Γ}.
Nous généralisons la définition 1.3.1 page 19 aux termes de la logique du premier ordre.
Définition 5.1.3 (Substitution) Une substitution est une application des variables dans les termes. Soient A une formule
et σ une substitution. Aσ est la formule obtenue en remplaçant toute occurrence libre d’une variable par son image dans
l’application. La formule Aσ est une instance de A.
Dans la suite de ce chapitre, nous ne considérons que des formules qui ne contiennent ni le symbole égal, ni les
constantes propositionnelles > et ⊥, car leur sens est fixé dans toute interprétation : > vaut 1, ⊥ vaut 0, et le symbole
= est l’identité sur le domaine de l’interprétation (voir Remarque 4.3.18 page 79). De plus nous considérons que toute
signature comporte au moins une constante. Ainsi la signature d’un ensemble de formules ne comportant pas de constante,
sera arbitrairement complétée par la constante a.
Notons que le domaine de Herbrand d’une signature sans constante est vide. Puisque toutes les signatures considérées
dans ce chapitre doivent comporter au moins une constante, ce domaine n’est pas vide.
2. Soit Σ la signature comportant uniquement la constante a, le symbole de fonction unaire f et le symbole de relation
unaire P. Nous avons DΣ = { f n (a) | n ∈ N} et BΣ =
Définition 5.1.6 (Interprétation de Herbrand) Soient Σ une signature et E ⊆ BΣ . L’interprétation de Herbrand HΣ,E a
pour domaine DΣ et donne aux symboles le sens suivant :
5.1. Méthode de Herbrand 95/129
1. Si le symbole s est une constante de la signature, il vaut lui-même dans cette interprétation.
fn
2. Si s est un symbole de fonction à n ≥ 1 arguments de la signature et si t1 , . . . ,tn ∈ DΣ alors sHΣ,E (t1 , . . . ,tn ) =
s(t1 , . . . ,tn ).
3. Si le symbole s est une variable propositionnelle, il vaut 1, autrement dit il est vrai, si et seulement si s ∈ E.
4. Si s est un symbole de relation de la signature à n ≥ 1 arguments et si t1 , . . . ,tn ∈ DΣ alors srn
HΣ,E = {(t1 , . . . ,tn ) |
t1 , . . . ,tn ∈ DΣ ∧ s(t1 , . . . ,tn ) ∈ E}.
Le résultat suivant montre qu’une interprétation de Herbrand peut être identifiée à l’ensemble des formules atomiques
fermées dont elle est modèle.
Propriété 5.1.7 (Propriété d’une interprétation de Herbrand) Soient Σ une signature et E ⊆ BΣ . Dans l’interprétation
de Herbrand HΣ,E :
1. La valeur d’un terme sans variable est lui-même.
2. L’interprétation est modèle d’une formule atomique fermée si et seulement si elle est élément de E.
Exemple 5.1.8 Soit Σ la signature comportant les 2 constantes a, b et les 2 symboles de relations unaires P, Q. L’ensemble
E = {P(b), Q(a)} définit l’interprétation de Herbrand HΣ,E de domaine DΣ = {a, b}
Théorème 5.1.16 (Fermeture universelle et modèle de Herbrand) Soit Γ un ensemble de formules sans quantificateur
sur la signature Σ. La fermeture universelle ∀(Γ) a un modèle si et seulement si ∀(Γ) a un modèle qui est une interprétation
de Herbrand de Σ.
Théorème 5.1.17 (Théorème de Herbrand) Soit Γ un ensemble de formules sans quantificateur de signature Σ. ∀(Γ)
a un modèle si et seulement si tout ensemble fini d’instances fermées sur la signature Σ des formules de Γ a un modèle
propositionnel application de la base de Herbrand BΣ dans l’ensemble {0, 1}.
Corollaire 5.1.18 Soit Γ un ensemble de formules sans quantificateur de signature Σ. La fermeture universelle ∀(Γ)
est insatisfaisable si et seulement s’il existe un ensemble fini insatisfaisable d’instances fermées sur la signature Σ des
formules de Γ.
Preuve : Le corollaire est obtenu en remplaçant chaque côté de l’équivalence du théorème de Herbrand par sa négation.
2
Dans le cas où Γ est un ensemble fini de formules, ce corollaire fonde une procédure de semi-décision pour savoir si
∀(Γ) est ou n’est pas insatisfaisable : nous énumérons l’ensemble des instances fermées des formules de Γ sur la signature
Σ et nous arrêtons cette énumération dès que nous obtenons un ensemble insatisfaisable, ou dès que cette énumération est
terminée sans contradiction ou dès que nous sommes « fatigués » :
1. Dans le premier cas, la procédure répond (en appliquant le corollaire) que ∀(Γ) est insatisfaisable.
2. Le deuxième cas ne peut se produire que si le domaine de Herbrand ne comprend que des constantes, la procédure
répond (en appliquant le corollaire) que ∀(Γ) est satisfaisable et en donne un modèle.
3. Dans le troisième cas, nous ne pouvons évidemment pas conclure : le corollaire nous dit que si ∀(Γ) est insatisfai-
sable, et si nous avions été plus courageux, nous aurions obtenu une contradiction.
96/129 Chapitre 5. Base de la démonstration automatique
Exemple 5.1.19
1. Soit Γ = {P(x), Q(x), ¬P(a) ∨ ¬Q(b)}. La signature Σ comporte 2 constantes a, b et 2 symboles de relation unaire
P, Q.
2. Soit Γ = {P(x) ∨ Q(x), ¬P(a), ¬Q(b)}. Nous avons la même signature que précédemment.
3. Soit Γ = {P(x), ¬P( f (x))}. La signature Σ comporte une constante a, un symbole de fonction unaire f et un
symbole de relation unaire P. La constante a est ajoutée à la signature de Γ pour que le domaine de Herbrand ne
soit pas vide.
4. Soit Γ = {P(x) ∨ ¬P( f (x)), ¬P(a), P( f ( f (a)))}. Nous avons la même signature que précédemment.
5. Soit Γ = {R(x, s(x)), R(x, y) ∧ R(y, z) ⇒ R(x, z), ¬R(x, x)}. La signature Σ comporte une constante a, un symbole
de fonction unaire s et un symbole de relation binaire R.
5.2. Skolémisation 97/129
5.2 Skolémisation
Le théorème de Herbrand est applicable à la fermeture universelle d’un ensemble de formules sans quantificateur. Nous
étudions une transformation, la skolémisation, qui change un ensemble de formules fermées en la fermeture universelle
d’un ensemble de formules sans quantificateur et qui préserve l’existence d’un modèle. Cette transformation est due à
Thoralf Albert Skolem (1887 - 1963), mathématicien et logicien norvégien. Elle est nécessaire pour pouvoir appliquer la
résolution sur un ensemble de formules de la logique du premier ordre. Nous commençons par donner l’intuition de la
skolémisation avant de regarder le résultat de cette transformation sur des exemples simples afin d’observer les propriétés
de la skolémisation. La skolémisation sert à éliminer les quantificateurs existentiels et change une formule fermée A en
une formule B telle que :
— B a pour conséquence A.
— tout modèle de A donne un modèle de B.
Par suite A a un modèle si et seulement si B a un modèle : la skolémisation préserve l’existence d’un modèle, nous
disons aussi qu’elle préserve la satisfaisabilité. Regardons ce qu’il en est sur deux exemples simples.
Exemple 5.2.1 La formule ∃xP(x) est skolémisée en P(a). Nous observons les relations entre ces deux formules :
1. P(a) a pour conséquence ∃xP(x).
2. ∃xP(x) n’a pas pour conséquence P(a) mais un modèle de ∃x P(x) « donne » un modèle de P(a). En effet soit I un
modèle de ∃xP(x). Donc il existe d ∈ PI . Soit J l’interprétation telle que PJ = PI et aJ = d. J est modèle de P(a).
Exemple 5.2.2 La formule ∀x∃yQ(x, y) est skolémisée en ∀xQ(x, f (x)). Nous observons les relations entre ces deux for-
mules :
1. ∀xQ(x, f (x)) a pour conséquence ∀x∃yQ(x, y).
2. ∀x∃yQ(x, y) n’a pas pour conséquence ∀xQ(x, f (x)) mais un modèle de ∀x∃yQ(x, y) « donne » un modèle de
∀xQ(x, f (x)). En effet soient I un modèle de ∀x∃yQ(x, y) et D le domaine de I. Pour tout d ∈ D, l’ensemble
{e ∈ D | (d, e) ∈ QI } n’est pas vide, donc il existe g : D → D une fonction 1 telle que pour tout d ∈ D, g(d) ∈ {e ∈
D | (d, e) ∈ QI }. Soit J l’interprétation telle que QJ = QI et fJ = g : J est modèle de ∀xQ(x, f (x)).
Exemple 5.2.7 La formule ∀y(∀xP(x, y) ⇔ Q(y)) est transformée par élimination de l’équivalence et de l’implication
en :
Théorème 5.2.9 Soit A0 la formule obtenue en appliquant l’élimination d’un quantificateur existentiel sur la formule A.
La formule A0 est une formule fermée en forme normale et propre vérifiant :
1. A0 a pour conséquence A (A0 |= A).
2. Si A a un modèle alors A0 a un modèle identique à celui de A sauf pour le sens de f .
2. Si n = 0, f est une constante.
5.2. Skolémisation 99/129
Remarque 5.2.10 Dans le théorème 5.2.9 page précédente, il faut constater que la formule A0 obtenue à partir de la
formule A par élimination d’un quantificateur reste fermée, en forme normale et propre. Donc, en « appliquant » plusieurs
fois le théorème, ce qui implique de choisir un nouveau symbole à chaque quantificateur éliminé, nous transformons une
formule A fermée, en forme normale et propre en une formule B fermée, en forme normale, propre et sans quantificateur
existentiel telle que :
— la formule A est conséquence de la formule B,
— si A a un modèle, alors B a un modèle identique sauf pour le sens des nouveaux symboles.
Exemple 5.2.11 En éliminant les quantificateurs existentiels de la formule ∃x∀yP(x, y) ∧ ∃z∀u¬P(z, u) nous obtenons
Donc, il faut impérativement utiliser un nouveau symbole lors de chaque élimination d’un quantificateur existentiel.
Exemple 5.2.12 En éliminant les quantificateurs existentiels de la formule ∃x∀y∃zP(x, y, z) nous obtenons deux solutions
possibles :
— ∀yP(a, y, f (a, y))
— ∀yP(a, y, f (y))
Ceci dépend de l’ordre dans lequel nous appliquons l’elimination des quantificateurs existentiels. Or le théorème 5.2.9
montre que une des ces transformations a un modèle si et seulement si l’autre a également un modèle.
Théorème 5.2.13 Soit A une formule fermée, en forme normale, propre et sans quantificateur existentiel. Soit B la formule
obtenue en enlevant de A tous les quantificateurs universels. La formule A est équivalente à la fermeture universelle de B.
Preuve : Avec les conditions posées sur A, la transformation de A en ∀(B) revient à effectuer tous les remplacements
possibles des sous-formules de la forme suivante :
— (∀xC) ∧ D par ∀x(C ∧ D), où x non libre dans D,
— (∀xC) ∨ D par ∀x(C ∨ D), où x non libre dans D,
— D ∧ (∀xC) par ∀x(D ∧C), où x non libre dans D,
— D ∨ (∀xC) par ∀x(D ∨C), où x non libre dans D.
Puisque chacun de ces remplacements change une formule en une autre équivalente, les formules A et ∀(B) sont équiva-
lentes. 2
Preuve : Soit C la formule fermée en forme normale et propre, obtenue au terme des deux premières étapes de la skolémi-
sation de A. Soit D le résultat de l’élimination des quantificateurs existentiels appliquée à C. D’après la remarque 5.2.10
nous avons :
— la formule D a pour conséquence la formule C,
— si C a un modèle alors D a un modèle.
Puisque les deux premières étapes changent des formules en des formules équivalentes, A et C sont équivalentes. D’après
le théorème 5.2.13, D est équivalent à ∀(B). Donc nous pouvons remplacer ci-dessus D par ∀(B) et C par A, ce qui prouve
le théorème. 2
Exemple 5.2.15 Soit A = ∀x(P(x) ⇒ Q(x)) ⇒ (∀xP(x) ⇒ ∀xQ(x)). Nous skolémisons ¬A.
100/129 Chapitre 5. Base de la démonstration automatique
Cette formule est la forme de Skolem de ¬A suivant la définition 5.2.5 page 97.
Instancions la forme de Skolem de ¬A en remplaçant x et y par a. Nous obtenons la formule (¬P(a)∨Q(a))∧P(a)∧¬Q(a)
qui est insatisfaisable. Donc ∀((¬P(x) ∨ Q(x)) ∧ P(y) ∧ ¬Q(a)) est insatisfaisable. Puisque, d’après la propriété 5.2.14
page précédente, la skolémisation préserve l’existence d’un modèle, ¬A est insatisfaisable, donc A est valide.
Pour skolémiser un ensemble de formules, nous skolémisons chaque formule de l’ensemble comme il a été indiqué
ci-dessus en choisissant impérativement un nouveau symbole pour chaque quantificateur existentiel éliminé durant la
troisième étape de la skolémisation. Les raisons pour le choix d’un symbole nouveau apparaissent clairement dans la
preuve du théorème 5.2.9 page 98 et dans l’exemple 5.2.11 page précédente.
Corollaire 5.2.16 En skolémisant un ensemble de clauses fermées Γ, nous obtenons un ensemble ∆ de formules sans
quantificateurs tel que :
— Tout modèle de ∀(∆) est modèle de Γ.
— Si Γ a un modèle alors ∀(∆) en a un modèle qui ne diffère de celui de Γ que par le sens des nouveaux symboles.
La skolémisation a des conséquences pratiques : elle facilite la preuve d’insatisfiabilité d’une formule. Elle a aussi des
conséquences théoriques, que nous examinons.
Théorème 5.2.17 Soit Γ un ensemble dénombrable de formules fermées. Si Γ a un modèle alors Γ a un modèle dénom-
brable.
Preuve : Nous skolémisons Γ en un ensemble ∆ de formules sans quantificateurs. Supposons que Γ a un modèle. Alors
∀(∆) a un modèle d’après le corollaire 5.2.16. D’après le théorème 5.1.16 page 95, ∀(∆) a un modèle de Herbrand sur
la signature de ∆. Puisque l’ensemble Γ est dénombrable, sa signature l’est aussi, donc aussi celle de ∆ et par suite le
domaine de ce modèle de Herbrand est dénombrable. 2
Remarque 5.2.18 Appelons théorie, un ensemble de formules. D’après le théorème, toute théorie dénombrable qui a un
modèle, a un modèle dénombrable. Autrement dit avec une théorie du premier ordre, nous pouvons parler des propriétés
des nombres réels ou des ensembles, mais nous ne pouvons pas obliger notre théorie à n’avoir que des modèles non
dénombrables, bien que l’ensemble des réels ou la classe de tous les ensembles ne soient pas dénombrables.
5.2. Skolémisation 101/129
Définition 5.2.22 (Forme clausale d’un ensemble de formules) Soit Γ un ensemble de formules fermées. Nous définis-
sons la forme clausale de Γ comme l’union des formes clausales de chacune des formules de Γ, en prenant soin au cours
de la skolémisation d’éliminer chaque occurrence d’un quantificateur existentiel à l’aide d’un nouveau symbole.
Corollaire 5.2.23 Soient Γ un ensemble de formules fermées et ∆ la forme clausale de Γ. Nous avons :
— ∀(∆) a pour conséquence Γ, et
— si Γ a un modèle alors ∀(∆) a un modèle.
Théorème 5.2.24 (Adaptation du théorème de Herbrand aux formes clausales) Soient Γ un ensemble de formules fer-
mées et ∆ la forme clausale de Γ. L’ensemble Γ est insatisfaisable si et seulement s’il existe un sous-ensemble fini insatis-
faisable d’instances des clauses de ∆ sur la signature de ∆.
Preuve : D’après l5.2.23, la skolémisation préserve la satisfaisablité, donc : Γ est insatisfaisable si et seulement si ∀(∆)
est insatisfaisable. D’après le corollaire du théorème de Herbrand 5.1.18 page 95, ∀(∆) est insatisfaisable si et seulement
s’il existe un sous-ensemble fini insatisfaisable d’instances des clauses de ∆ sur la signature de ∆. 2
Exemple 5.2.25 Soit A = ∃y∀z(P(z, y) ⇔ ¬∃x(P(z, x) ∧ P(x, z))). Calculons la forme clausale de A.
1. Mettre A sous forme en forme normale :
5. Transformer en produit de sommes de littéraux, nous obtenons la forme clausale de A, qui est l’ensemble suivant
de clauses :
D’après la propriété ci-dessus, A n’a pas de modèle si et seulement s’il y a un ensemble fini insatisfaisable d’instances de
C1 ,C2 ,C3 sur la signature de ces clauses. Nous recherchons ces instances :
5.3 Unification
Après la mise en forme clausale d’un ensemble de formules en logique du premier ordre et avant de généraliser la
résolution pour ces clauses, nous avons besoin d’un algorithme résolvant l’égalité entre deux termes. Étant donné deux
termes, trouver une substitution qui appliquée à ces deux termes les rendent égaux est appelé problème d’unification de ces
deux termes. Ce problème a intéressé de grands noms de l’informatique comme Alan Robinson [23], Gérard Huet [15, 16],
Alberto Martelli et Ugo Montanari [21], ou encore plus récemment Franz Baader et Ayne Snyder [3].
5.3.1 Unificateur
Définition 5.3.1 (Expression, solution) Appelons expression, un terme ou un littéral. Une substitution σ (voir défini-
tion 5.1.3 page 94) est solution de l’équation e1 = e2 entre deux expressions, si les deux expressions e1 σ et e2 σ sont
identiques. Une substitution est solution d’un ensemble d’équations si elle est solution de chaque équation de l’ensemble.
Définition 5.3.2 (Unificateur) Soient σ une substitution et E un ensemble d’expressions. Eσ = {tσ | t ∈ E}. La substi-
tution σ est un unificateur de E si et seulement si l’ensemble Eσ n’a qu’un élément. Soit {ei |1 ≤ i ≤ n} un ensemble
fini d’expressions. La substitution σ est un unificateur de cet ensemble si et seulement si elle est solution du système
d’équations {ei = ei+1 |1 ≤ i < n}.
Définition 5.3.3 (Support d’une substitution) Le support d’une substitution σ est l’ensemble des variables x telles que
xσ 6= x. Dans la suite, nous nous intéressons seulement aux substitutions à support fini, c’est à dire qui ne changent
qu’un nombre fini de variables. Une substitution σ à support fini est notée < x1 := t1 , . . . , xn := tn > ou plus simplement
x1 := t1 , . . . , xn := tn quand il n’y a pas de risque d’ambiguïté. Les variables x1 , . . . , xn sont distinctes et la substitution
vérifie :
5.3. Unification 103/129
— Pour i de 1 à n, xi σ = ti .
— Pour toute variable y telle que y 6∈ {x1 , . . . , xn }, nous avons : yσ = y.
Exemple 5.3.4 L’équation P(x, f (y)) = P(g(z), z) a pour solution :
Définition 5.3.5 (Composition de substitutions) Soient σ et τ deux substitutions, nous notons στ la substitution telle
que pour toute variable x, xστ = (xσ)τ. La substitution στ est une instance de σ. Deux substitutions sont équivalentes si
chacune d’elles est une instance de l’autre.
Exemple 5.3.6 Considérons les substitutions suivantes :
— σ1 =< x := g(z), y := z >.
— σ2 =< x := g(y), z := y >.
— σ3 =< x := g(a), y := a, z := a >.
Nous avons les relations suivantes entre ces substitutions :
Définition 5.3.7 (Solution la plus générale) Une solution d’un système d’équations est appelée la plus générale (en fran-
çais nous disons aussi principale) si toute autre solution en est une instance. Notons que deux solutions « les plus géné-
rales » sont équivalentes.
Exemple 5.3.8 L’équation f (x, g(z)) = f (g(y), x) a pour solutions (entre autres) :
Définition 5.3.9 (Unificateur le plus général) Soit E un ensemble d’expressions. Nous rappelons qu’une expression est
un terme ou un littéral. Un unificateur de E (voir définition 5.3.2 page précédente) est appelé le plus général (ou encore
principal), si tout autre unificateur en est une instance.
Remarque 5.3.10 (Unificateur le plus général et solution la plus générale) Soit E = {ei | 1 ≤ i ≤ n} un ensemble d’ex-
pressions. Dans la définition d’un unificateur, nous avons indiqué que σ est un unificateur de E si et seulement si σ est
solution du système S = {ei = ei+1 | 1 ≤ i < n}.
Donc l’unificateur le plus général de E est la solution la plus générale de S.
Exemple 5.3.11 Nous appliquons cet algorithme afin de résoudre les équations suivantes :
1. f (x, g(z)) = f (g(y), x).
3. Nous pouvons nous limiter à la suppression des équations de la forme x = x où x est une variable.
4. Un algorithme efficace évite ce remplacement systématique.
5.4. Résolution au premier ordre 105/129
Nous montrons d’abord que notre algorithme est correct, c’est-à-dire qu’il calcule bien un unificateur. Ensuite nous
démontrons qu’il termine toujours.
1. La factorisation qui de la prémisse P(x, f (y)) ∨ P(g(z), z) ∨ Q(z, x) déduit P(g( f (y)), f (y)) ∨ Q( f (y), g( f (y))).
La clause déduite est obtenue en calculant la solution la plus générale x := g( f (y)), z := f (y) de P(x, f (y)) =
P(g(z), z).
2. La règle de copie qui permet de renommer les variables d’une clause.
3. La résolution binaire (RB) qui des deux prémisses sans variable commune P(x, a) ∨ Q(x) et ¬P(b, y) ∨ R( f (y))
déduit le résolvant Q(b) ∨ R( f (a)), en calculant la solution plus générale x := b, y := a de P(x, a) = P(b, y).
Pour simplifier la présentation des règles, nous identifierons une clause, qui est une somme de littéraux, avec l’ensemble
de ses littéraux. Nous formalisons ces trois règles.
[Link] Factorisation
Propriété 5.4.1 Soient A une formule sans quantificateur et B une instance de A. Nous avons : ∀(A) |= ∀(B).
Définition 5.4.2 La clause C0 est un facteur de la clause C si C0 = C ou s’il existe un sous-ensemble E de C tel que E a
au moins deux éléments, E est unifiable et C0 = Cσ où σ est l’unificateur le plus général de E.
Propriété 5.4.4 (Cohérence de la règle de factorisation) Soit C0 un facteur de la clause C. Nous avons : ∀(C) |= ∀(C0 ).
Preuve : Puisque C0 est une instance de C, la propriété est une conséquence immédiate de la propriété 5.4.1. 2
Définition 5.4.6 Soient C une clause et σ un renommage de C. Soit f la restriction de σ aux variables de C et f −1
l’application réciproque de f . Soit σC−1 la substitution ainsi définie pour toute variable x :
— Si x est une variable de Cσ alors xσC−1 = x f −1 (par soucis de clarté, nous avons préféré utiliser la notation
postfixée x f −1 plutôt que la notation préfixée f −1 (x), plus usuelle).
— Sinon xσC−1 = x.
Cette substitution est appelée l’inverse du renommage σ de C.
Exemple 5.4.7 Soit σ =<x := u, y := v>. σ est un renommage du littéral P(x, y). Le littéral P(u, v), où P(u, v) = P(x, y)σ,
est une copie de P(x, y). Soit τ =<u := x, v := y>. τ est l’inverse du renommage σ de P(x, y). Notons que P(u, v)τ = P(x, y) :
le littéral P(x, y) est une copie de P(u, v) par le renommage τ.
Preuve : Soit f la restriction de σ aux variables de C. Par définition du renommage, f est une bijection entre les variables
de C et celles de Cσ.
1. Par définition de σC−1 , cette substitution ne change que les variables de Cσ et sa restriction aux variables de Cσ est
la bijection f −1 . Donc, σC−1 est un renommage de Cσ.
5.4. Résolution au premier ordre 107/129
2. Soit x une variable de C. Par définition de f , xσσC−1 = x f f −1 = x. Donc, par une récurrence omise et sans intérêt
sur les termes, littéraux et clauses, pour toute expression ou clause E, dont les variables sont celles de C, nous
avons EσσC−1 = E.
2
Propriété 5.4.9 Soient deux clauses copies l’une de l’autre, leurs fermetures universelles sont équivalentes.
Preuve : Soit C0 une copie de C. Par définition, C0 est une instance de C et par la propriété précédente, C est une copie de
C0 , donc une instance de C0 . Donc par la propriété 5.4.1 page ci-contre, la fermeture universelle de C est conséquence de
celle de C0 et inversement. Par suite, ces deux fermetures universelles sont équivalentes. 2
Propriété 5.4.12 (Cohérence de la règle de résolution binaire) Soit E un résolvant binaire des clauses C et D, nous
avons : ∀(C), ∀(D) |= ∀(E).
Preuve : Soit I une interprétation. Puisque les trois formules ∀(C), ∀(D), ∀(E) sont sans variable libre, il suffit de montrer
que si I est modèle de ∀(C) et de ∀(D) alors I est modèle de ∀(E). Supposons que I est modèle de ∀(C), ∀(D) et montrons
que c’est un modèle de ∀(E). Soit e un état quelconque de cette interprétation. (I, e) est modèle de Cσ et Dσ, pour toute
substitution σ. Par définition du résolvant binaire, il y a un littéral L ∈ C et un littéral M ∈ D tels que L et M c (le littéral
opposé à M) sont unifiables. Ainsi, Lσ et Mσ sont deux littéraux opposés, donc (I, e) est modèle soit de l’un, soit de
l’autre de ces deux littéraux.
1. Supposons (I, e) modèle de Lσ. Puisque (I, e) est contre-modèle de Mσ et modèle de Dσ, c’est un modèle de
(D − {M})σ donc de E car (D − {M})σ ⊂ E.
2. Supposons (I, e) contre-modèle de Lσ. Puisque c’est un modèle de Cσ, c’est un modèle de (C − {L})σ donc de E
car (C − {L})σ ⊂ E.
Donc (I, e) est modèle de E. Puisque l’état e est quelconque, I est modèle de ∀(E). 2
C est déduite de Γ au premier ordre par les 3 règles de factorisation, copie et résolution binaire est dénoté par Γ `1 f cb C.
Cela signifie qu’il y a une preuve de C à partir de Γ. Quand il n’y a pas d’ambiguïté sur le système formel utilisé, nous
remplaçons `1 f cb par `.
Preuve : Cette propriété est une conséquence immédiate de la cohérence de la factorisation, de la copie et de la résolution
binaire. Cette preuve est demandée dans l’exercice 97 page 114. 2
108/129 Chapitre 5. Base de la démonstration automatique
Cet exemple montre, a contrario, que la résolution binaire seule est incomplète, sans la factorisation, nous ne pouvons
pas déduire la clause vide.
Définition 5.4.17 La clause E est un résolvant au 1o ordre des clauses C et D si E est un résolvant binaire de C0 et D0 où
C0 est un facteur de C et D0 est une copie sans variable commune avec C0 d’un facteur de D. La règle qui de C et D déduit
E est appelée la résolution de 1o ordre.
Exemple 5.4.18 Soient C = ¬P(z, a) ∨ ¬P(z, x) ∨ ¬P(x, z) et D = P(z, f (z)) ∨ P(z, a).
C0 = ¬P(a, a) est un facteur de C. La clause P(a, f (a)) est un résolvant binaire de C0 et de D (qui est facteur de
lui-même) donc
Soient Γ un ensemble de clauses et C une clause, nous avons défini jusqu’à présent trois notions de preuve par
résolution que nous distinguons en notant par :
1. Γ ` p C le fait qu’il y existe une preuve de C à partir de Γ obtenue par résolution propositionnelle, autrement dit
sans substitution.
2. Γ `1 f cb C le fait qu’il y existe une preuve de C à partir de Γ par factorisation, copie et résolution binaire.
3. Γ `1r C le fait qu’il y existe une preuve de C à partir de Γ obtenue par résolution de 1o ordre.
Puisque la résolution du premier ordre est une combinaison des règles factorisation, copie et résolution binaire, nous
avons immédiatement Γ `1r C implique Γ `1 f cb C.
Théorème 5.4.19 (Théorème du relèvement) Soient C et D deux clauses. Soient C0 une instance de C et D0 une instance
de D. Soit E 0 un résolvant propositionnel de C0 et D0 , il existe E un résolvant au premier ordre de C et D qui a pour
instance E 0 .
Exemple 5.4.20 Soient C = P(x) ∨ P(y) ∨ R(y) et D = ¬Q(x) ∨ P(x) ∨ ¬R(x) ∨ P(y).
— Les clauses C0 = P(a) ∨ R(a) et D0 = ¬Q(a) ∨ P(a) ∨ ¬R(a) sont des instances respectivement de C et D.
— La clause E 0 = P(a) ∨ ¬Q(a) est un résolvant propositionnel de C0 et D0 .
— La clause E = P(x) ∨ ¬Q(x) est un résolvant au 1o ordre de C et D qui a pour instance E 0 .
Théorème 5.4.21 Soient Γ un ensemble de clauses et ∆ un ensemble d’instances des clauses de Γ, et C1 , . . . ,Cn une
preuve par résolution propositionnelle à partir de ∆, il existe une preuve D1 , . . . , Dn par résolution au 1o ordre à partir de
Γ telle que pour i de 1 à n, la clause Ci est une instance de Di .
Preuve : Nous effectuons une récurrence sur n. Soit C1 , . . . ,Cn ,Cn+1 une preuve par résolution propositionnelle à partir
de ∆. Par récurrence, il existe une preuve D1 , . . . , Dn par résolution 1o ordre à partir Γ telle que pour i de 1 à n, la clause
Ci est une instance de Di . Nous distinguons deux cas :
1. Supposons Cn+1 ∈ ∆. Il existe E ∈ Γ dont Cn+1 est une instance donc nous prenons Dn+1 = E.
2. Supposons que Cn+1 soit un résolvant propositionnel de C j et Ck où j, k ≤ n. D’après le résultat précédent, il existe
E résolvant au 1o ordre de D j et Dk : nous prenons Dn+1 = E.
2
Nous en déduisons immédiatement le corollaire suivant.
Corollaire 5.4.22 Soient Γ un ensemble de clauses et ∆ un ensemble d’instances des clauses de Γ. Supposons que ∆ ` p C.
Il existe D telle que Γ `1r D et C est une instance de D.
Exemple 5.4.23 Soit l’ensemble de clauses P( f (x)) ∨ P(u), ¬P(x) ∨ Q(z), ¬Q(x) ∨ ¬Q(y). La fermeture universelle de
cet ensemble de clauses est insatisfaisable et nous le montrons de trois manières.
1. Par instanciation sur le domaine de Herbrand { f n (a), n ∈ N} :
— P( f (x)) ∨ P(u) est instanciée par x := a, u := f (a) en P( f (a))
— ¬P(x) ∨ Q(z) est instanciée par x := f (a), z := a en ¬P( f (a)) ∨ Q(a)
— ¬Q(x) ∨ ¬Q(y) est instanciée par x := a, y := a en ¬Q(a)
L’ensemble de ces 3 instanciations est insatisfaisable, comme le montre la preuve par résolution propositionnelle
ci-dessous :
P( f (a)) ¬P( f (a)) ∨ Q(a)
Q(a) ¬Q(a)
⊥
110/129 Chapitre 5. Base de la démonstration automatique
2. Cette preuve par résolution propositionnelle est relevée en une preuve par la règle de résolution au premier ordre :
3. Chaque règle de résolution au premier ordre est décomposée en factorisation, copie et résolution binaire :
Théorème 5.4.24 (Complétude réfutationnelle de la résolution au 1o ordre) Soit Γ un ensemble de clauses. Les pro-
positions suivantes sont équivalentes :
1. Γ `1r ⊥.
2. Γ `1 f cb ⊥.
3. ∀(Γ) |= ⊥.
Preuve :
— Nous savons que (1) implique (2), car la résolution au 1o ordre est une combinaison de factorisation, copie et
résolution binaire.
— Nous savons que (2) implique (3), car la factorisation, la copie et la résolution binaire sont cohérentes.
— Il nous reste à montrer que (3) implique (1). Supposons que ∀(Γ) |= ⊥, autrement dit ∀(Γ) est insatisfaisable.
D’après le théorème de Herbrand, il y a ∆ un ensemble fini d’instances sans variable de clauses de Γ qui n’a
pas de modèle propositionnel. Par complétude de la résolution propositionnelle, nous avons : ∆ ` p ⊥. D’après le
corollaire au relèvement 5.4.22 page précédente, il existe D telle que Γ `1r D et ⊥ est instance de D. Dans ce cas,
nous avons D = ⊥.
2
[Link]
Cet outil, de façon similaire à celui proposé pour la déduction naturelle propositionnelle au paragraphe 3.5 page 66,
permet de saisir une liste de clauses du premier ordre. Il tente alors automatiquement d’en déduire la clause vide :
— si cette liste de clauses est insatisfaisable et qu’aucune limite de temps ni de taille n’a été fixée, alors la clause vide
sera déduite ;
— il est possible de restreindre l’espace de recherche, en imposant une limite de temps ou de taille sur les clauses
produites (mais alors on perd la complétude du prouveur).
Si la liste de clauses est insatisfaisable, on obtient une preuve utilisant les règles de copie, factorisation et résolution
binaire, annotée par les unificateurs utilisés.
5.6. Exercices 111/129
5.6 Exercices
Exercice 80 (Domaine de Herbrand) Soient Σ la signature composée de la constante a et des symboles de fonctions f
et g respectivement à un et deux arguments.
— Donner 5 éléments différents du domaine de Herbrand de cette signature.
— Définir inductivement ce domaine.
Exercice 81 (Signature, domaine et base de Herbrand) Pour chacun de ces ensembles de formules :
— Γ1 = {P(x) ∨ Q(x) ∨ R(x), ¬P(a), ¬Q(b), ¬R(c)}.
— Γ2 = {P(x), ¬Q(x), ¬P( f (x)) ∨ Q( f (x))}.
— Γ3 = {P(x), Q( f (x)), ¬R( f ( f (x))), ¬P( f ( f (x))) ∨ ¬Q(x) ∨ R( f (x))}.
1. Donner la signature, le domaine de Herbrand ainsi que la base de Herbrand.
2. Prouver si leur fermeture universelle a un modèle ou pas.
Exercice 82 (Méthode de Herbrand) Utiliser la méthode de Herbrand pour démontrer que l’ensemble de formules sui-
vant est insatisfaisable :
1. ∀xR(x, f (x))
2. ∀x∀y(¬S(x, y) ∨ R(x, y) ∨ R(y, x))
3. ∀x∀y(S(x, y) ∨ ¬R(x, y))
4. ∀x∀y(S(x, y) ∨ ¬R(y, x))
5. ∀y¬S(y, a)
Exercice 83 (Méthode de Herbrand,*) Utiliser la méthode de Herbrand pour démontrer que l’ensemble de formules
suivant est insatisfaisable :
1. ∀x(Q(x) ∨ ¬P( f (x)))
2. ∀y(Q(y) ⇒ R(y))
3. ∀z(¬P(z) ⇒ Q(z) ∨ R(z))
4. ∀u¬R(u)
En particulier, vous devez transformer votre ensemble d’instances insatisfaisable en un ensemble de clauses équivalent.
Puis, vous devez démontrer la contradiction via une preuve par résolution propositionnelle à partir de ce dernier en-
semble.
Exercice 86 (Skolémisation et forme clausale) Skolémiser les formules suivantes (attention aux négations !) puis les
mettre en forme clausale.
1. ¬(∃xP(x) ∨ ∃xQ(x) ⇒ ∃x(P(x) ∨ Q(x))).
2. ¬(∀x∀y∀z(e(x, y) ∧ e(y, z) ⇒ ¬e(x, z)) ⇒ ¬∃x∀y e(x, y)).
3. ¬(¬∀xP(x) ∨ ¬∀xQ(x) ⇒ ¬(∀xP(x) ∧ ∀xQ(x))).
4. ∀x((∃yP(x, y) ⇒ ∃xQ(x)) ∧ ∃yP(x, y) ∧ ¬∃xQ(x)).
5. ¬(∃x∀y∀z((P(y) ⇒ Q(z)) ⇒ (P(x) ⇒ Q(x)))).
Exercice 87 (Unification) Les termes suivants sont-ils unifiables ? Si la réponse est oui, donner leur unificateur le plus
général, sinon justifier la réponse négative.
— h(g(x), f (a, y), z) et h(y, z, f (u, x)).
— h(g(x), f (a, y), z) et h(y, z, f (u, g(x))).
Exercice 88 (Unification) Donner les unificateurs les plus généraux des termes suivants s’ils existent :
1. R(a, f (x)) = R(y, f (g(y, b))),
2. R(y, f (x)) = R(x, f (g(y, b))),
3. Q(y, f (a), f (x)) = Q(g(a, b), x, f (y)), et
4. Q(y, f (x), g(y, x)) = Q(x, f (y), g( f (a), y)).
Exercice 89 (Unification) Donner les unificateurs les plus généraux des termes suivants s’ils existent :
1. pair(a, crypt(z, b)) et pair(x, y).
2. pair(crypt(x, b), crypt(y, b)) et pair(crypt(a, b), z).
3. crypt(pair(z, a), x) et crypt(pair(y, crypt(x, b)), b).
4. crypt(pair(a, z), x) et crypt(pair(y, crypt(x, b)), b).
5. f (x, y, g(a, a)) et f (g(y, y), z, z)
6. f (x, y, a) et f (y, g(z, z), x)
Exercice 90 (Unification avec plusieurs solutions) L’équation f (g(y), y) = f (u, z) a deux solutions « les plus géné-
rales »(rappel : elles sont donc équivalentes). Indiquer ces deux solutions.
Exercice 91 (Forme clausale et instanciation,*) Montrer que la formule suivante est valide en mettant sa négation sous
la forme clausale et en trouvant un ensemble contradictoire d’instances des clauses obtenues :
∀x(P(x) ⇒ Q(x)) ⇒ (∀xP(x) ⇒ ∀xQ(x)).
Exercice 92 (Forme clausale et preuve par résolution,**) Considérons les formules suivantes :
1. H1 = ∃xP(x) ⇒ ∀xP(x).
2. H2 = ∀x(P(x) ∨ Q(x)).
3. C = ∃x¬Q(x) ⇒ ∀xP(x).
Nous voulons montrer que C est conséquence de H1 et H2 par instanciation et par résolution.
1. Mettre en forme clausale l’ensemble des trois formules H1 , H2 , ¬C.
2. Trouver des instances contradictoires des clauses obtenues et montrer par résolution propositionnelle que ces
instances sont contradictoires.
5.6. Exercices 113/129
3. Donner une preuve directe de cette contradiction par factorisation, copie et résolution binaire. Il est possible que
seule la dernière règle soit utilisée.
Exercice 94 (Unification, résolution) Soient Γ1 = {P(x, f (x, b), u), ¬P(g(a), z, h(z))} l’ensemble des deux clauses uni-
taires et Γ2 l’ensemble des deux clauses unitaires {P(x, f (x, b), u), ¬P(g(z), z, h(z))}. Les ensembles ∀(Γ1 ) et ∀(Γ2 ) sont-
ils satisfaisables ou insatisfaisables ?
Exercice 95 (Skolémisation et preuve par résolution) Le but de cet exercice est de démontrer le syllogisme suivant :
Exercice 96 (Forme clausale et preuve par résolution,**) Considérons les formules suivantes :
1. A1 = ∃u∀v(P(u) ∧ (R(v) ⇒ Q(u, v))).
2. A2 = ∀u∀v(¬P(u) ∨ ¬S(v) ∨ ¬Q(u, v)).
3. A3 = ∃v(R(v) ∧ S(v)).
Montrer que la liste de ces trois formules est contradictoire par résolution :
1. Mettre en forme clausale les trois formules A1 , A2 , A3 .
114/129 Chapitre 5. Base de la démonstration automatique
2. Trouver des instances contradictoires des clauses obtenues et montrer cette contradiction par résolution proposi-
tionnelle.
3. Faire une preuve directe de ⊥ par factorisation, copie et résolution binaire.
Exercice 97 (Cohérence de la résolution au premier ordre) Prouver la cohérence de la résolution au premier ordre,
c’est-à-dire :
Soit Γ un ensemble de clauses et C une clause. Si Γ `1 f cb C alors ∀(Γ) |= ∀(C).
Exercice 98 (Forme clausale et preuve par résolution,**) Considérons les formules suivantes :
1. E1 = ∀x(x = x).
2. E2 = ∀x∀y(x = y ⇒ y = x).
3. E3 = ∀x∀y∀z∀t(x = y ∧ z = t ⇒ (x ∈ z ⇒ y ∈ t)).
4. C = ∀y∀z(y = z ⇒ ∀x(x ∈ y ⇔ x ∈ z)).
E1 , E2 , E3 sont des axiomes de l’égalité : E1 exprime que l’égalité est réflexive, E2 qu’elle est symétrique, E3 que c’est
une congruence relativement à l’appartenance. La transitivité de l’égalité ne sert pas dans cet exercice. C exprime que
deux ensembles égaux ont les mêmes éléments. Nous notons que dans cet exercice, le symbole égal est traité comme un
symbole de prédicat « ordinaire » dont le sens n’est pas fixé comme étant l’identité, mais que nous « définissons » par ses
propriétés. Autrement dit l’interdiction de l’égalité dans les formules, c’est en réalité l’interdiction de l’égalité comme
symbole de sens fixé. Montrer que C est conséquence des axiomes de l’égalité.
1. Mettre en forme clausale les trois formules E1 , E2 , E3 , ¬C.
2. Trouver des instances contradictoires des clauses obtenues.
3. Faire une preuve directe de ⊥ par factorisation, copie et résolution binaire.
Exercice 99 (Forme clausale et preuve par résolution,**) Considérons les formules suivantes :
1. H1 = ∀u(∃vR(u, v) ⇒ R(u, f (u))).
2. H2 = ∀u∃vR(u, v).
3. H3 = ∃uR( f ( f (u)), u).
4. C = ∃u∃v∃w(R(u, v) ∧ R(v, w) ∧ R(w, u)).
Montrer que C est conséquence de H1 , H2 , H3 .
1. Mettre en forme clausale les trois formules H1 , H2 , H3 , ¬C.
2. Trouver des instances contradictoires des clauses obtenues (montrez la contradiction par résolution proposition-
nelle).
3. Faire une preuve directe de cette contradiction par factorisation, copie et résolution binaire.
Exercice 100 (Forme clausale et preuve par résolution,**) Soit P(x, y) une formalisation de « x est père de y ». Soit
A(x, y) une formalisation de « x est aïeul de y ». Soient les trois formules :
1. H1 = ∀x∃yP(x, y).
2. H2 = ∀x∀y∀z(P(x, y) ∧ P(y, z) ⇒ A(x, z)).
3. C = ∀x∃yA(x, y).
Montrons que C est conséquence de H1 , H2 , de la façon suivante, transformer H1 , H2 , ¬C en leur forme clausale, puis
trouver des instances contradictoires des clauses obtenues (montrez la contradiction par résolution propositionnelle).
Enfin, dériver la clause vide par factorisation, copie, résolution binaire.
Exercice 101 (Formule de Bernays-Schonfinkel,***) Une formule BS (de Bernays-Schonfinkel) est une formule fermée,
sans symbole de fonction, de la forme ∃x1 . . . ∃xn ∀y1 . . . ∀y p B où B est sans quantificateur. Expliquer pourquoi nous
pouvons décider la satisfaisabilité d’une telle formule.
Chapitre 6
Sommaire
6.1 Règles pour la logique du premier ordre . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115
6.1.1 Règles des quantificateurs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116
6.1.2 Copie . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119
6.1.3 Les règles de l’égalité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119
6.2 Tactiques de preuves . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119
6.2.1 Raisonner en avant avec une hypothèse d’existence . . . . . . . . . . . . . . . . . . . . . . . . . 120
6.2.2 Raisonner en arrière pour généraliser . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120
6.2.3 Un exemple d’application des tactiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120
6.3 Cohérence du système . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122
6.4 Exercices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 124
E N plus des règles du chapitre 3, nous ajoutons les règles concernant les quantificateurs, la copie et l’égalité. Notre
système comporte toujours une seule règle pour enlever les hypothèses (la règle d’introduction de l’implication).
Les définitions de brouillon de preuve, environnement, contexte, formule utilisable restent inchangées. Nous montrons
la cohérence des règles de notre système, mais nous admettons sans preuve, que ce système est complet : des preuves
de complétude pour des systèmes de règles similaires peuvent être trouvées dans les livres [2, 11]. Contrairement au
cas propositionnel, il n’y a aucun algorithme pour décider si une formule est valide ou non valide (preuve donnée par
Alonzo Church et Alan Türing en 1936 et 1937 [4, 24]). Autrement dit, en admettant l’équivalence entre prouvable (sans
environnement) et valide, il n’y a pas d’algorithme qui, étant donné une formule, puisse nous en construire la preuve, ou
nous avertir que cette formule n’a pas de preuve.
Plan : Nous étendons d’abord les règles de la déduction naturelle proposées pour la logique propositionnelle. Nous
présentons ensuite deux nouvelles tactiques pour aider à la rédaction de preuves. Enfin, nous prouvons la cohérence de
notre système.
∃xA (A ⇒ B)
B ∃E
A<x := t>
∃I
∃xA
∀xA
∀E
A<x := t>
Nous justifions ci-dessous les conditions d’emploi de cette règle par un exemple montrant qu’un usage incorrect de la
règle peut conduire à prouver une formule non-valide.
Exemple 6.1.1 Nous montrons qu’un usage incorrect de la règle ∀E conduit à « prouver » une formule non valide.
À la ligne 2, nous n’avons pas respecté les conditions d’applications de la règle ∀E car le terme y n’est pas libre
pour x dans la formule ∃yP(x, y). Nous donnons une interprétation qui est un contre-modèle de la « conclusion » : soit I
l’interprétation de domaine {0, 1} avec PI =
La règle d’introduction du quantificateur universel, notée ∀I, signifie que si nous avons pu déduire la formule A
indépendemment de la valeur de x, nous pouvons généraliser en déduisant ∀xA. Ainsi, il est nécessaire que x ne soit libre
ni dans l’environnement de la preuve, ni dans le contexte de la ligne où nous avons déduit A.
A
∀I
∀xA
6.1. Règles pour la logique du premier ordre 117/129
Nous illustrons maintenant l’emploi de la règle d’introduction du quantificateur universel avec un exemple d’usage
correct (exemple 6.1.2) et un exemple d’usage incorrect (exemple 6.1.3) de la règle.
Exemple 6.1.3 Nous montrons qu’un usage incorrect de la règle ∀I conduit à « prouver » une formule non valide.
À la ligne 2, nous n’avons pas respecté les conditions d’applications de la règle ∀I car la prémisse P(x) est établie
dans le contexte P(x), ce qui interdit de généraliser sur x. Nous donnons un contre-modèle de la « conclusion » :
∃xA (A ⇒ B)
B ∃E
La condition d’emploi de cette règle étant complexe, nous illustrons l’emploi de la règle avec deux exemples d’usage
incorrect.
Exemple 6.1.4 Nous montrons qu’un usage incorrect de la règle ∃E conduit à « prouver » une formule non valide.
Nous n’avons pas respecté la condition que le contexte de la prémisse P(x) ⇒ ∀yQ(y) ne doit pas dépendre de x. Il est
clair que la conclusion obtenue n’est pas valide. Nous donnons une assignation (I, e) qui est un contre-modèle de cette
« conclusion » :
Exemple 6.1.5 Nous montrons qu’un usage incorrect de la règle ∃E conduit à « prouver » une formule non valide.
La conclusion de la règle ∃E est P(x), contrairement à la condition d’application de cette règle qui impose que la
conclusion ne doit pas dépendre de x. Nous donnons une interprétation qui est un contre-modèle de la cette « conclu-
sion » :
La règle d’introduction du quantificateur existentiel, notée ∃I, signifie que si une instance de la formule A où x est
remplacé par un terme t libre pour x est vraie, alors la formule ∃xA est vraie. Notez que cette règle est une simple
application du corollaire 4.3.38, page 83. Ce qui justifie la condition d’emploi. Pour s’en convaincre, il suffit d’étudier
l’exemple 4.3.37, qui précède le corollaire 4.3.38.
Ci-dessous, nous donnons un exemple d’usage correct de la règle d’introduction du quantificateur existentiel en dé-
montrant l’une des lois de De Morgan.
Exemple 6.1.6 (Lois de De Morgan) Nous montrons que pour toute formule A, ¬∀xA ⇒ ∃x¬A.
6.1.2 Copie
La règle de copie consiste à déduire d’une formule A, une autre formule A0 égale au changement près des variables
liées, au sens de la définition 4.4.5, page 88. Par exemple, ∀x∃yP(x, y) est une copie de ∀y∃xP(y, x).
A0
A Copie
Ré f lexivit é
t =t
s = t A<x := s>
Congruence
A<x := t>
Nous remarquons que la première règle n’a pas de prémisse. C’est ce que nous appelons aussi un axiome. Nous
remarquons aussi que les conditions d’emploi de la deuxième règle sont similaires à celles des règles ∀E et ∃I. Ces
conditions d’emploi se justifient de la même manière que précédemment.
Nous donnons maintenant deux exemples d’application des règles d’égalités.
Exemple 6.1.7 Prouvons que s = t ⇒ t = s, autrement dit prouvons que l’égalité est symétrique.
Exemple 6.1.8 Prouvons que s = t ∧ t = u ⇒ s = u, autrement dit prouvons que l’égalité est transitive.
1 1 Supposons s = t ∧ t = u
1 2
1 3
1 4
5 Donc s = t ∧ t = u ⇒ s = u
Supposons A
preuve de C dans l’environnement Γ, A
Donc A ⇒ C ⇒ I 1,_
C ∃E
2. Supposons que x soit libre dans Γ ou C. Nous choisissons une variable y « nouvelle », c’est-à-dire non libre dans
Γ, C et absente de A, puis nous nous ramenons au cas précédent, via la règle de copie. La preuve s’écrit alors :
La recherche de la preuve initiale a été réduite à la recherche d’une preuve dans un environnement plus simple. C’est
exactement le mode de raisonnement appliqué dans les cours de mathématiques quand nous cherchons une preuve d’une
formule C avec l’hypothèse ∃xP(x). Nous introduisons une constante « nouvelle » a vérifiant P(a) et nous prouvons C
sous l’hypothèse P(a).
2. Supposons que x est libre dans Γ. Nous choisissons une variable y « nouvelle », c’est-à-dire non libre dans Γ, puis
nous nous ramenons au cas précédent, via la règle de copie. La preuve s’écrit alors :
La recherche de la preuve initiale a été réduite à la recherche d’une preuve d’une formule plus simple dans le même
environnement. C’est exactement le mode de raisonnement appliqué dans les cours de mathématiques quand nous cher-
chons une preuve de ∀xP(x). Nous introduisons une constante « nouvelle » a et nous prouvons P(a). Puis nous ajoutons :
puisque le choix de a est arbitraire, nous avons ∀xP(x).
référence formule
i ∃x(P(x) ∧ ∀y(P(y) ⇒ x = y))
1 Supposons P(x) ∧ ∀y(P(y) ⇒ x = y)
2 P(x) ∧E1 1
3 ∃xP(x) ∃I 2, x
4 Donc P(x) ∧ ∀y(P(y) ⇒ x = y) ⇒ ∃xP(x) ⇒ I 1,2
5 ∃xP(x) ∃E i, 3
environnement
référence formule
i ∃x(P(x) ∧ ∀y(P(y) ⇒ x = y))
contexte numéro preuve règle
1 1 Supposons P(x) ∧ ∀y(P(y) ⇒ x = y)
1 2
1 3
1 4
1 5
1 6
1 7
1 8
1 9
1 10
1 11
1 12
1 13
1 14
15
16 ∀x∀y(P(x) ∧ P(y) ⇒ x = y)
122/129 Chapitre 6. Déduction naturelle au premier ordre : quantificateurs, copie et égalité
La tactique « utiliser une hypothèse d’existence » sert à produire la ligne 16. La tactique « introduire une implication »
sert à produire la ligne 15 : elle introduit l’hypothèse (1) dans laquelle x est une variable libre. Donc, pour appliquer la
tactique « obtenir une conclusion générale », il faut changer de variable dès la ligne 2. Observer aussi que la formule, ligne
3, est instanciée aux lignes 5 et 8.
Comme sur cet exemple, toute la difficulté des preuves est concentrée autour des règles ∀I et ∃E :
— dans le raisonnement en avant, il faut trouver les bonnes instanciations des formules commençant par un quantifi-
cateur existentiel.
— dans le raisonnement en arrière, il faut trouver la bonne instance permettant de déduire une formule commençant
par un quantificateur universel.
Propriété 6.3.1 Soient Γ un ensemble de formules, x une variable et A une formule. Supposons que x ne soit pas libre
dans Γ, alors nous avons : Γ |= A si et seulement si Γ |= ∀xA.
Preuve :
2
Si nous observons d’un œil critique cette preuve, nous observons que c’est une paraphrase, dans un autre formalisme,
de la loi ∀I. C’est l’équivalence ci-dessus, qui explique que la tactique « raisonner en arrière pour généraliser », est une
tactique utilisable sans risque. En effet, en admettant la complétude du système, lorsque x n’est pas libre dans Γ, il y a une
preuve de A dans l’environnement Γ si et seulement s’il a une preuve de ∀xA dans ce même environnement.
Propriété 6.3.2 Soient Γ un ensemble de formules, x une variable, A et B deux formules. Supposons que x ne soit libre ni
dans Γ, ni dans B, alors nous avons : Γ |= A ⇒ B si et seulement si Γ |= (∃xA) ⇒ B
Preuve :
⇒ Supposons que Γ |= A ⇒ B. Soit (I, e) une assignation modèle de Γ. Puisque x n’est pas libre dans Γ, pour tout
état f identique à e sauf pour la valeur de x, (I, f ) et (I, e) donnent la même valeur aux formules de Γ, donc (I, f )
est modèle de Γ. Puisque Γ |= A ⇒ B, pour tout état f identique à e sauf pour la valeur de x, (I, f ) est modèle de
A ⇒ B. Supposons que (I, e) est modèle de ∃xA, il existe g identique à e sauf pour la valeur de x tel que (I, g) est
modèle de A. Puisque pour tout état f identique à e sauf pour la valeur de x, (I, f ) est modèle de A ⇒ B, alors (I, g)
est modèle de B. Puisque x n’est pas libre dans B, (I, e) est modèle de B.
⇐ Supposons que Γ |= (∃xA) ⇒ B. Puisque la formule A ⇒ (∃xA) est valide (d’après le corollaire 4.3.38 page 83),
nous avons Γ |= A ⇒ B.
2
Si nous observons d’un œil critique cette preuve, nous voyons que c’est une paraphrase, dans un autre formalisme, de la
loi ∃E. C’est l’équivalence ci-dessus, qui explique que la tactique « raisonner en avant avec une hypothèse d’existence »,
est une tactique utilisable sans risque. En effet, en admettant la complétude du système, lorsque x n’est libre ni dans Γ,
ni dans B, il y a une preuve de B dans l’environnement Γ, A si et seulement s’il a une preuve de B dans l’environnement
Γ, ∃xA.
Théorème 6.3.3 (Cohérence de la déduction) Si une formule est déduite d’un environnement de formules alors elle en
est une conséquence.
6.3. Cohérence du système 123/129
Preuve : La preuve obéit au même plan que celle du même théorème dans le cas propositionnel (voir théorème 3.3.1
page 65) et nous en reprenons les notations en traitant uniquement le cas des nouvelles règles.
Soit Γ un ensemble de formules. Soit P une preuve de A dans cet environnement. Soient Ci la conclusion et Hi le
contexte de la i-ème ligne de la preuve P. Rappelons que les lignes d’une preuve sont numérotées à partir de 1 et que H0
est la liste vide.
Notons par Γ, Hi l’ensemble des formules de l’ensemble Γ et de la liste Hi .
Cas de base : Supposons que A est déduite de Γ par la preuve vide. Alors A est élément de Γ, donc Γ |= A. Puisque
H0 est la liste vide, nous pouvons conclure : Γ, H0 |= A.
Induction : Supposons que pour toute ligne i < k, Γ, Hi |= Ci . Montrons que Γ, Hk |= Ck .
Nous examinons uniquement le cas des nouvelles règles et pour simplifier nous ne faisons pas de distinctions entre
deux formules égales aux abréviations près de la négation et de l’équivalence.
— Supposons que Ck = ∀xA et que cette ligne ait été déduite, par la règle ∀I, de la formule A avec A = Ci et
0 ≤ i < k ou A ∈ Γ. Si A = Ci et 0 < i < k, par hypothèse de récurrence nous avons, Γ, Hi |= A. Si A ∈ Γ alors
Γ |= A. Puisque H0 est la liste vide, il existe i où 0 ≤ i < k tel que Γ, Hi |= A. Vu les conditions d’application
de la règle, x n’est pas libre dans Γ, Hi . Donc, d’après la propriété 6.3.1 page ci-contre, nous avons aussi
Γ, Hi |= ∀xA. Puisque la ligne i est utilisable sur la ligne k − 1 et que H0 est la liste vide, Hi est préfixe de Hk−1 .
Puisque le contexte n’est pas modifié par la ligne k, nous avons Hk−1 = Hk , donc Γ, Hk |= Ck .
— Supposons que Ck = A<x := t > et que cette ligne ait été déduite, par la règle ∀E, de la formule ∀xA avec
∀xA = Ci et 0 < i < k ou ∀xA ∈ Γ. Par hypothèse de récurrence ou parce que H0 est la liste vide, il existe i
où 0 ≤ i < k tel que Γ, Hi |= ∀xA. D’après les conditions d’application de la règle, le terme t est libre pour
la variable x dans la formule A. Donc, d’après le corollaire 4.3.38 page 83, la formule ∀xA ⇒ A<x := t> est
valide et par suite Γ, Hi |= A<x := t>. Puisque la ligne i est utilisable sur la ligne k − 1, et que H0 est la liste
vide, Hi est préfixe de Hk−1 . Puisque le contexte n’est pas modifié par la ligne k, nous avons Hk−1 = Hk , donc
Γ, Hk |= Ck .
— Supposons que Ck = ∃xA et que cette ligne ait été déduite, par la règle ∃I, de la formule A<x := t > avec
A<x := t > = Ci et 0 < i < k ou A<x := t >∈ Γ. Par hypothèse de récurrence ou parce H0 est la liste vide,
il existe i où 0 ≤ i < k tel que Γ, Hi |= A<x := t >. D’après les conditions d’applications de la règle, le
terme t est libre pour la variable x dans la formule A. Donc, d’après le corollaire 4.3.38 page 83, la formule
A<x := t>⇒ ∃xA est valide et par suite Γ, Hi |= ∃xA. Puisque la ligne i est utilisable sur la ligne k − 1, et que
H0 est la liste vide, Hi est préfixe de Hk−1 . Puisque le contexte n’est pas modifié par la ligne k, nous avons
Hk−1 = Hk , donc Γ, Hk |= Ck .
— Supposons que Ck = B et que cette formule ait été déduite, par la règle ∃E, de la formule ∃xA avec ∃xA = Ci
et 0 < i < k ou ∃xA ∈ Γ et de la formule A ⇒ B avec A ⇒ B = C j et 0 < j < k ou A ⇒ B ∈ Γ. Par hypothèse
de récurrence ou parce H0 est la liste vide, il existe i et j tels que 0 ≤ i < k, 0 ≤ j < k, Γ, Hi |= ∃xA et
Γ, H j |= A ⇒ B. Vu les conditions d’application de la règle, x n’est libre ni dans Γ, H j , ni dans B. Donc,
d’après la propriété 6.3.2 page précédente, nous avons aussi Γ, H j |= (∃xA) ⇒ B. Puisque les lignes i et j sont
utilisables sur la ligne k − 1, et que H0 est la liste vide, Hi et H j sont préfixes de Hk−1 . Puisque le contexte
n’est pas modifié par la ligne k, nous avons Hk−1 = Hk , donc Γ, Hk |= ∃xA et Γ, Hk |= (∃xA) ⇒ B. Par suite
Γ, Hk |= Ck .
— Supposons que Ck = A0 et que cette formule ait été déduite, par la règle de copie de la formule A avec A = Ci
et 0 < i < k ou A ∈ Γ. Par hypothèse de récurrence ou parce H0 est la liste vide, il existe i tel que 0 ≤ i < k,
Γ, Hi |= A. Puisque, d’après le théorème 4.4.6 page 88, les formules A et A0 sont équivalentes, nous avons
Γ, Hi |= A0 . Puisque la ligne i est utilisable sur la ligne k − 1, et que H0 est la liste vide, Hi est préfixe de Hk−1 .
Puisque le contexte n’est pas modifié par la ligne k, nous avons Hk−1 = Hk , donc Γ, Hk |= Ck .
— Supposons que Ck = (t = t). Puisque cette formule est valide (dans le sens attribué à l’égalité), Γ, Hk |= Ck .
— Supposons que Ck = A<x := t> et que cette ligne ait été déduite, par la règle de congruence, de la formule
s = t avec (s = t) = Ci et 0 < i < k ou (s = t) ∈ Γ et de la formule A<x := s> avec A<x := s>= C j et 0 < j < k
ou A<x := s>∈ Γ. Par hypothèse de récurrence ou parce H0 est la liste vide, il existe i et j tels que 0 ≤ i < k,
0 ≤ j < k, Γ, Hi |= (s = t) et Γ, H j |= A<x := s>. Puisque les lignes i et j sont utilisables sur la ligne k − 1,
et que H0 est la liste vide, Hi et H j sont préfixes de Hk−1 . Puisque le contexte n’est pas modifié par la ligne k,
nous avons Hk−1 = Hk , donc Γ, Hk |= (s = t) et Γ, Hk |= A<x := s>. D’après le théorème 4.3.36 page 83 et les
conditions d’application de la règle, nous avons : s = t, A<x := s>|= A<x := t>. Par suite Γ, Hk |= Ck .
Puisque la dernère ligne d’une preuve a un contexte vide, nous obtenons que sa conclusion est conséquence de Γ. 2
124/129 Chapitre 6. Déduction naturelle au premier ordre : quantificateurs, copie et égalité
6.4 Exercices
Exercice 102 (Déductions naturelles) Prouver en déduction naturelle du premier ordre les formules suivantes :
1. le fameux syllogisme, « Tout homme est mortel, Socrate est un homme, donc est mortel », que nous formalisons
par ∀x(H(x) ⇒ M(x)) ∧ H(socrate) ⇒ M(socrate).
2. ∀xP(x) ⇒ ∃yP(y).
3. ∀xP(x) ⇒ ∃xP(x).
4. ∀x(P(x) ∧ Q(x)) ⇒ ∀xP(x) ∧ ∀xQ(x). Notez que l’exemple 6.1.2 page 117 donne la preuve de la réciproque.
5. ∃x(P(x) ∨ Q(x)) ⇒ ∃xP(x) ∨ ∃xQ(x).
6. ∀x(P(x) ⇒ Q(x)) ∧ ∃xP(x) ⇒ ∃xQ(x).
7. ∃xP(x) ∨ ∃xQ(x) ⇒ ∃x(P(x) ∨ Q(x)). (**)
8. ∀x(P(x) ⇒ Q(x)) ∧ ∀x(Q(x) ⇒ R(x)) ⇒ ∀x(P(x) ⇒ R(x)).
9. ∀x (P(x) ⇒ Q(x)) ∧ ∃x ¬Q(x) ⇒ ∃x ¬P(x).
Dans cet exercice, les formules P(x) et Q(x) peuvent être remplacées par des formules quelconques.
Parmi les trois preuves suivantes une seule est correcte par déduction naturelle. Identifier la preuve correcte et justifier
pourquoi les deux autres ne le sont pas.
1.
2.
6.4. Exercices 125/129
3.
contexte numéro preuve règle
1 1 Supposons ∃x P(x) ∧ ∀x Q(x)
1 2 ∃x P(x) ∧E1 1
1 3 ∀x Q(x) ∧E2 1
1,4 4 Supposons P(x)
1 5 Donc P(x) ⇒ P(x) ⇒ I 4,4
1 6 P(x) ∃E 2,5
1 7 Q(x) ∀E 3, x
1 8 P(x) ∧ Q(x) ∧I 6,7
1 9 ∃x(P(x) ∧ Q(x)) ∃I 8, x
10 Donc ∃x P(x) ∧ ∀x Q(x) ⇒ ∃x(P(x) ∧ Q(x)) ⇒ I 1,9
Exercice 105 (Copie) Prouver par déduction naturelle que ∀x∀yP(x, y) ⇒ ∀x∀yP(y, x) en utilisant la règle de copie un
minimum de fois.
Exercice 106 (Déduction naturelle) Prouver les formules suivantes grâce à la déduction naturelle (notez que Q est une
variable propositionnelle) :
1. ∀x(Q ∧ P(x)) ⇒ Q ∧ ∀xP(x).
2. Q ∧ ∀xP(x) ⇒ ∀x(Q ∧ P(x)).
3. ∀x(Q ∨ P(x)) ⇒ Q ∨ ∀xP(x). (**)
4. Q ∨ ∀xP(x) ⇒ ∀x(Q ∨ P(x)).
5. ∃x(Q ∧ P(x)) ⇒ Q ∧ ∃xP(x).
6. Q ∧ ∃xP(x) ⇒ ∃x(Q ∧ P(x)).
7. ∃x(Q ∨ P(x)) ⇒ Q ∨ ∃xP(x).
8. Q ∨ ∃xP(x) ⇒ ∃x(Q ∨ P(x)). (*)
Dans cet exercice, la formule P(x) peut être remplacée par une formule quelconque. Par contre, Q peut être remplacée
seulement par une formule n’ayant pas x comme variable libre.
Exercice 107 (Preuve) Prouver la formule ¬∃xP(x) ⇒ ∀x¬P(x). Vérifier que P(x) peut être remplacée par une formule
quelconque. Remarque : cette formule est la réciproque de la formule prouvée à l’exemple 6.1.6 page 118.
Exercice 109 (Égalité,**) Prouver que la deuxième définition de « il existe un et un seul x » (voir sous-section 6.2.3
page 120) implique la première, autrement dit prouver la formule : ∃xP(x) ∧ ∀x∀y(P(x) ∧ P(y) ⇒ x = y) ⇒ ∃x(P(x) ∧
∀y(P(y) ⇒ x = y)).
Exercice 110 (Induction et déduction naturelle,***) Nous pouvons définir l’addition grâce aux deux formules :
(a) ∀n(n + 0 = n).
(b) ∀n∀p(n + s(p) = s(n + p)).
Ces deux formules permettent de faire des additions : nous pouvons grâce à elles prouver que s(0) + s(0) = s(s(0)). Mais
elles ne permettent pas de prouver les propriétés générales de l’addition, qui nécessitent d’avoir le principe de récurrence.
1. Montrer que des hypothèses (a) et (b), nous ne pouvons pas déduire ∀n(0 + n = n).
2. Nous donnons un nom à la propriété ci-dessus et nous posons le principe de récurrence sur cette propriété :
(c) ∀n(P(n) ⇔ 0 + n = n).
(d) P(0) ∧ ∀n(P(n) ⇒ P(s(n))) ⇒ ∀nP(n).
Prouver par la déduction naturelle que (a) ∧ (b) ∧ (c) ∧ (d) ⇒ ∀nP(n).
Exercice 111 (Examen 2009) Les preuves demandées ci-dessous devront être justifiées.
1. Donner une preuve en déduction naturelle avec les justifications de la validité de la formule :
(∃x p(x) ⇒ ∀x q(x)) ⇒ ∀x(p(x) ⇒ q(x)).
2. Donner une preuve en déduction naturelle avec les justifications de la validité de la formule :
∃x p(x) ∧ ∀x(p(x) ⇒ p( f (x))) ⇒ ∃x p( f ( f (x))).
3. Notons f n (x) le terme obtenu en appliquant n fois f à x.
Par exemple f 0 (x) = x, f 1 (x) = f (x), f 2 (x) = f ( f (x)).
Soient Γ, ∆ deux ensembles de formules et A, B deux formules. On rappelle que Γ ` A est vrai s’il y a une preuve
de A dans l’environnement Γ.
On donne ci-dessous des propriétés triviales de la relation `.
Monotonie : si Γ ` A et Γ ⊂ ∆ alors ∆ ` A.
Composition : si Γ ` A et Γ ` A ⇒ B alors Γ ` B.
(a) Donnez une preuve en déduction naturelle avec les justifications de ce que la propriété suivante est vraie :
∀x(p(x) ⇒ p( f (x))) ` ∃xp( f n (x)) ⇒ ∃x p( f n+1 (x))
(b) Déduire de la propriété ci-dessus, de la monotonie et de la composition que pour tout entier naturel n :
∃x p(x), ∀x(p(x) ⇒ p( f (x))) ` ∃x p( f n (x)) .
Exercice 112 (Examen 2012) Prouver les formules suivantes par déduction naturelle au premier ordre.
1. ¬∀xP(x) ∨ ¬∃yQ(y) ⇒ ¬(∀xP(x) ∧ ∃yQ(y)).
2. ∀x∀y(P(y) ⇒ R(x)) ⇒ ∃yP(y) ⇒ ∀xR(x).
3. ¬∀x¬P(x) ⇒ ∃xP(x).
Exercice 113 (Examen 2013) Prouver les formules suivantes par déduction naturelle au premier ordre.
1. ∃x(Q(x) ⇒ P(x)) ∧ ∀xQ(x) ⇒ ∃xP(x).
2. ∀x ∀y(R(x, y) ⇒ ¬R(y, x)) ⇒ ∀x¬R(x, x).
Exercice 114 (Quelques questions posées en examen) Démontrer les formules suivantes par déduction naturelle.
1. ∃x(P(x) ∨ Q(x)) ∧ ∀x¬Q(x) ⇒ ∃xP(x).
2. ∀x(P(x) ⇒ Q(x)) ∧ ∃x(P(x) ∧ R(x)) ⇒ ∃x(Q(x) ∧ R(x)).
3. ∃x¬(P(x) ∨ ¬P(x)) ⇒ ∀xP(x).
Bibliographie
[1] Collin Allen and Michael Hand. Logic Primer. MIT, 2001.
[2] Peter B. Andrews. An introduction to mathematical logic : to truth through proof. Academic Press, 1986.
[3] Franz Baader and Wayne Snyder. Unification theory. In John Alan Robinson and Andrei Voronkov, editors, Hand-
book of Automated Reasoning (in 2 volumes), pages 445–532. Elsevier and MIT Press, 2001.
[4] Alonzo Church. A note on the entscheidungsproblem. Journal of Symbolic Logic, 1(1) :40–41, 1936.
[5] Stephen A. Cook. The complexity of theorem-proving procedures. In Proceedings of the third annual ACM sympo-
sium on Theory of computing, STOC ’71, pages 151–158, New York, NY, USA, 1971. ACM.
[6] René Cori and Daniel Lascar. Logique mathématique Cours et exercices I. Calcul propositionnel, algèbres de Boole,
calcul des prédicats. Masson, 1993.
[7] René Cori and Daniel Lascar. Logique mathématique Cours et exercices II. Fonctions récursives, théorème de Gödel,
théorie des ensembles, théories des modèles. Masson, 1993.
[8] René David, Karim Nour, and Christophe Raffali. Introduction à la logique. Dunod, 2001.
[9] Martin Davis, George W. Logemann, and Donald W. Loveland. A machine program for theorem-proving. Commu-
nications of The ACM, 5 :394–397, 1962.
[10] Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM (JACM),
7(3) :201–215, 1960.
[11] Herbert B. Enderton. A mathematical Introduction to Logic. Academic Press, 2001.
[12] Gerhard Gentzen. Untersuchungen über das logische Schließen I. Mathematische Zeitschrift, 39 :176–210, 1935.
10.1007/BF01201353.
[13] Gerhard Gentzen. Untersuchungen über das logische Schließen II. Mathematische Zeitschrift, 39 :405–431, 1935.
10.1007/BF01201363.
[14] Roger Godement. Cours d’algèbre. Hermann, 1973.
[15] Gérard P. Huet. unification in typed lambda calculus. In Corrado Böhm, editor, Lambda-Calculus and Computer
Science Theory, Proceedings of the Symposium Held in Rome, March 25-27, 1975, volume 37 of Lecture Notes in
Computer Science, pages 192–212. Springer, 1975.
[16] Gérard P. Huet. Higher order unification 30 years later. In Victor Carreño, César Muñoz, and Sofiène Tahar, editors,
Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August
20-23, 2002, Proceedings, volume 2410 of Lecture Notes in Computer Science, pages 3–12. Springer, 2002.
[17] Michael Huth and Mark Ryan. Logic in Computer Science. Cambridge University Press, 2004.
[18] Jacquemin. Logique et Mathématiques 109 exercices corrigées. Masson, 1994.
[19] Stephen C. Kleene. Logique Mathématique. Armand Colin, 1971.
[20] Thierry Lucas, Isabelle Berlanger, and Isabelle De Greef. Initiation à la logique formelle. De Boeck, 2003.
[21] Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Trans. Program. Lang. Syst., 4 :258–
282, April 1982.
[22] William McCune. Prover9 and mace4. [Link] 2005–2010.
[23] J. Alan Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM (JACM),
12(1) :23–41, January 1965.
[24] Alan Turing. On computable numbers, with an application to the entscheidungsproblem. Proceedings of the London
Mathematical Society, 42 :230–265, 1937.
Index