# La "Model Elimination" de D.W.Loveland expliquée

Michel Lévy

► To cite this version:

Michel Lévy. La "Model Elimination" de D.W.Loveland expliquée. 2016. hal-01292062v2

HAL Id: hal-01292062

https://hal.science/hal-01292062v2

Preprint submitted on 17 Apr 2016

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# La "Model Elimination" de D.W.Loveland
expliquée

Michel Lévy

17 avril 2016

## Table des matières

<table><tr><td>1</td><td>Bases de la méthode</td><td>2</td></tr><tr><td>1.1</td><td>La ME pour la logique propositionnelle</td><td>2</td></tr><tr><td>1.2</td><td>La ME pour la logique du premier ordre</td><td>4</td></tr><tr><td>2</td><td>Production des lemmes dans le cas propositionnel</td><td>6</td></tr><tr><td>3</td><td>Production des lemmes en logique du premier ordre</td><td>11</td></tr><tr><td>4</td><td>Complétude de la méthode</td><td>12</td></tr><tr><td>4.1</td><td>Complétude de la méthode dans le cas propositionnel</td><td>12</td></tr><tr><td>4.2</td><td>Complétude de la méthode dans le cas du premier ordre</td><td>14</td></tr></table>

## Introduction

La méthode "Model Elimination" est une méthode de preuve très simple à programmer, ce qui a fait son succès. Nous utilisons pour la présenter les références suivantes [OD97], [Don78] et [Sut12]. Le dernier document présente de façon claire et concise la production des lemmes, sans cette aide, je ne serais pas parvenu à rédiger cette explication de la méthode de D.W.Loveland.

Le livre de [OD97], qui présente une méthode ancienne, datant de 1967, introduit un système formel original, proche de la résolution, pour faire des preuves par réfutation. Cependant ce livre, en mélangeant les cas propositionnels et du premier ordre, me semble difficile à comprendre et donne une explication peu convaincante de la correction des lemmes engendrés au cours d'une dérivation.

Mon exposé effectue une séparation claire entre le cas propostionnel et le cas du premier ordre, ce qui rend les preuves beaucoup plus simples. Il prouve en détail la correction des lemmes engendrés au cours des dérivations, en introduisant une propriété invariante au cours des dérivations.
# 1 Bases de la méthode

L'opposé du littéral *L* est $
eg L$ si *L* est un atome, et *M* si $L = 
eg M$. Dans la suite, on note par $\overline{L}$, l'opposé du littéral *L*.

Une chaine est une liste de B-littéraux et de A-littéraux (appelés aussi littéraux ancêtres). Un A-littéral est représenté par un littéral entre crochets. Un B-littéral est un littéral au sens usuel. La liste vide est notée $\square$.

Une chaine élémentaire est une liste de B-littéraux.

Une chaine est acceptable si elle commence (à sa gauche) par un B-littéral.

Sur les chaines, on définit trois opérations, la réduction, l'expansion et l'enlèvement.

Afin de faciliter la compréhension de la méthode appelée "Model Elimination" (en abrégé ME), nous en donnerons la version pour la logique propositionnelle et la version pour la logique du premier ordre.

## 1.1 La ME pour la logique propositionnelle

**Expansion :** Soit *LU* une chaine acceptable où *L* est le B-littéral à gauche de la chaine. La chaine $VW[L]U$ est obtenue par expansion de la chaîne *LU* avec la chaine élémentaire $V\overline{L}W$.

**Réduction :** Soit $LU[\overline{L}]V$ une chaine acceptable, où *L* est un B-littéral. La chaine $U[\overline{L}]V$ est obtenue par réduction de la chaine $LU[\overline{L}]V$.

**Enlèvement :** Soit $[L]U$ une chaine commençant par le A-littéral $[L]$. La chaine *U* est obtenue par enlèvement sur la chaine $[L]U$.

**Définition 1 (Dérivation)** Soit $\Gamma$ un ensemble de chaines élémentaires, une dérivation à partir de $\Gamma$ est une suite de chaines $C_i$ où $1 \le i \le n$ telle que pour i de 1 à n-1, la chaine $C_{i+1}$ est obtenue par une expansion de la chaine $C_i$ avec une chaine de $\Gamma$, par une réduction de la chaine $C_i$ ou par un enlèvement sur la chaine $C_i$.

Une chaine *C* est dérivée à partir de $\Gamma$ s'il y a une dérivation à partir de $\Gamma$, dont la première chaine est dans $\Gamma$ et dont la dernière chaine est *C*.

Soit *K* une chaine. On lui associe une formule normale $fn(K)$, qui donne le sens de la chaine.

**Définition 2 (Forme normale d'une chaine)**

* $fn(\square) = \perp$ où $\perp$ est la formule toujours fausse.

* $fn(UL) = fn(U) + L$ où $+$ est la disjonction, *L* est un B-littéral et *U* une chaine.

* $fn(U[L]) = fn(U) * L$ où $*$ est la conjonction, $[L]$ est un A-littéral et *U* une chaine.

Notons que, d'après cette définition, une chaine élémentaire est une disjonction de ses B-littéraux.

Quand il n'y a pas d'ambiguïté, on identifie une chaine et la formule normale qui lui est associée. Prenons un exemple. Soit *L* un littéral, $fn([L]) = fn(\square) * L = \perp * L$. Par
suite, la formule $fn([L])$ est équivalente à $\perp$, qui est le sens de la chaine vide. Quand
cela ne crée pas d'ambuïguité, l'équivalence et l'égalité entre formules et chaines sont
confondues, donc on se permet d'écrire $[L] = \square$.

Nous montrons ci-dessous que les chaines dérivées de $\Gamma$ en sont des conséquences
(dans le sens de la conséquence logique). Cette propriété est appelée la cohérence de la
méthode.

Au cours d'une dérivation, on peut créer des lemmes, qui sont des chaines élémentaires conséquences de $\Gamma$. Il est clair que pour obtenir des conséquences de $\Gamma$, on peut utiliser des expansions à partir de chaines de $\Gamma$ et à partir des lemmes créés au cours des dérivations à partir de $\Gamma$.

Dans les ouvrages [OD97] et [Don78], l'enlèvement est incorporé aux deux autres opérations. À la fin d'une expansion ou d'une réduction, on effectue tous les enlèvements nécessaires pour obtenir à nouveau une chaine acceptable. Mais il m'a paru utile, en suivant l'exemple de [Sut12], de distinguer cette opération pour faciliter la compréhension de la création et de l'utilisation des lemmes.

**Lemme 3 (monotonie des chaines)** Soient $U, U', V$ trois chaines. Soit $\Gamma$ un ensemble de formules. Supposons que $\Gamma \models U \Rightarrow U'$. Alors $\Gamma \models UV \Rightarrow U'V$.

*Preuve :* Supposons que $\Gamma \models U \Rightarrow U'$.

Montrons la conclusion par récurrence sur la longueur de $V$.

Si $V$ est la chaine vide, c'est évident.

Supposons que $V = WL$ où $L$ est un littéral.

Par hypothèse de récurrence, $\Gamma \models UW \Rightarrow U'W$.

Par définition du sens des chaines, $UWL = (UW) + L$ et $U'WL = (U'W) + L$.

À cause de la monotonie de la disjonction, $\Gamma \models (UW) + L \Rightarrow (U'W) + L$,

donc $\Gamma \models UWL \Rightarrow U'WL$.

Le cas où $V = W[L]$ est analogue, car la conjonction est aussi monotone. $\square$

**Corollaire 4 (monotonie des chaines)** Soient $U, U', V$ trois chaines. Soit $\Gamma$ un ensemble de formules. Supposons que $\Gamma \models U = U'$. Alors $\Gamma \models UV = U'V$.

Ce corollaire est une conséquence immédiate du lemme précédent, car l'équiva-
lence $U = U'$ est la conjonction de $U \Rightarrow U'$ et $U' \Rightarrow U$.

**Lemme 5 (cohérence de l'enlèvement)** Soit $L$ un littéral et $U$ une chaine. On a :
$[L]U = U$

*Preuve :* On a vu ci-dessus que $[L] = \square$. D'après le corollaire 4, $[L]U = U$ $\square$

**Lemme 6 (cohérence de la réduction)** Soit $L$ un littéral et $U, V$ deux chaines. On a
$\models LU[\bar{L}]V \Rightarrow U[\bar{L}]V$.

*Preuve :* D'après le sens des chaines, $LU[\bar{L}] = (LU) * \bar{L}$.

D'après le sens de la négation, $\bar{L} \models L \Rightarrow \square$.

D'après le lemme 3 de monotonie, $\bar{L} \models LU \Rightarrow U$.
Par suite $LU[\bar{L}] \models U$ et $LU[\bar{L}] \models \bar{L}$, donc $LU[\bar{L}] \models U * \bar{L}$.

Puisque $U * \bar{L} = U[\bar{L}]$, et d'après les propriétés de la conséquence, $\models LU[\bar{L}] \Rightarrow U[\bar{L}]$.

D'après le lemme 3, $\models LU[\bar{L}]V \Rightarrow U[\bar{L}]V$. $\square$

**Lemme 7 (cohérence de l'expansion)** Soit $\Gamma$ un ensemble de chaines élémentaires.

Soit $K$ une chaine donnant, par expansion avec une chaine de $\Gamma$, la chaine $K'$.

On a : $\Gamma \models K \Rightarrow K'$.

*Preuve :* Par définition de l'expansion, il y a un littéral $L$ et une chaine $U$ telle que $K = LU$. Il y a une chaine de $\Gamma$ qui s'écrit $V\bar{L}W$ et $K' = VW[L]U$.

La chaine élémentaire $V\bar{L}W$ est équivalente à $L \Rightarrow VW$.

Par suite $\Gamma \models L \Rightarrow VW$, donc $\Gamma \models L \Rightarrow VW * L$.

D'après le sens des chaines, $(VW) * L = VW[L]$, donc $\Gamma \models L \Rightarrow VW[L]$.

Par le lemme 3, on en déduit $\Gamma \models K \Rightarrow K'$. $\square$

**Théorème 8 (cohérence de la méthode)** Soit $\Gamma$ un ensemble de chaines élémentaires

et $K$ une chaine dérivée de $\Gamma$. On a : $\Gamma \models K$.

*Preuve :* Puisque $K$ est dérivée (voir 1) de $\Gamma$, il y a une dérivation $K_i$ où $1 \le i \le n$ (voir 1) de $K$ à partir de $\Gamma$ et $K_1 \in \Gamma$.

Puisque $K_1 \in \Gamma$, on a $\Gamma \models K_1$.

Des lemmes 7, 6, 5, il résulte que : pour tout $i$ entre 1 et $n-1$, $\Gamma \models K_i \Rightarrow K_{i+1}$.

Donc par récurrence sur la longueur des dérivations :

pour tout $i$ où $1 \le i \le n$, $\Gamma \models K_i$.

Puisque $K$ est la dernière chaine de la dérivation, $\Gamma \models K$. $\square$

**Corollaire 9 (preuve d'insatisfaisabilité)** Soit $\Gamma$ un ensemble de chaines élémentaires.

Si $\square$ est dérivée de $\Gamma$ alors $\Gamma$ est insatisfaisable.

*Preuve :* Supposons $\square$ dérivée de $\Gamma$. Alors d'après le théorème ci-dessus, $\Gamma \models \square$.

Puisque $\square$ est la formule fausse (n'ayant aucun modèle), $\Gamma$ n'a aucun modèle. $\square$

## 1.2 La ME pour la logique du premier ordre

**Expansion :** Soit $LU$ une chaine acceptable où $L$ est le B-littéral à gauche de la chaine.

Soit $C$ une chaine élémentaire.

Soit $C'$ une copie de la chaine $C$, dont les variables ne figurent pas dans $LU$.

Supposons que $C' = WMW$ où $M$ est un littéral et qu'il existe $\sigma$ un unificateur principal de $L$ et de l'opposé du littéral $M$. Alors la chaine $(VW[L]U)\sigma$ est obtenue par expansion de la chaîne $LU$ avec la chaine $C$.

**Réduction :** Soit $LU[M]V$ une chaine acceptable, où $L$ est le littéral le plus à gauche de la chaine et $[M]$ un littéral ancêtre, tel qu'il y a un unificateur principal $\sigma$ entre $L$ et l'opposé de $M$ alors la chaine $(U[M]V)\sigma$ est obtenue par réduction de la chaine $LU[M]V$.
**Enlèvement** : Soit $[L]U$ une chaine commençant par le $A$-littéral $[L]$. La chaine $U$ est obtenue par enlèvement sur la chaine $[L]U$

La fermeture universelle d'une formule $A$ est notée $\forall(A)$. C'est la formule obtenue en quantifiant universellement toutes les variables libres de $A$.

Soit $\Gamma$ un ensemble de formules. La fermeture universelle de $\Gamma$, notée $\forall(\Gamma)$ est l'ensemble des fermetures universelles des formules de $\Gamma$.

Dans la suite nous utilisons la notion de conséquence (logique) dans son sens le plus usuel. Une formule est conséquence d'un ensemble de formules, si tout modèle de l'ensemble (donnant des valeurs aux symboles de relations et de fonctions, ainsi qu'aux variables) est modèle de la formule.

Avec cette notion de conséquence $\forall x P(x) \models P(x)$, mais $P(x) \not\models \forall x P(x)$.

Nous verrons que les chaines dérivées d'un ensemble $\Gamma$ de chaines élémentaires sont conséquences de $\forall(\Gamma)$ : c'est cette propriété qui est, pour la logique du premier ordre, appelée la cohérence de la méthode. Au cours d'une dérivation, on peut créer des lemmes, qui sont des chaines élémentaires conséquences de $\forall(\Gamma)$. Il est clair que pour obtenir des conséquences de la fermeture universelle de $\Gamma$, on peut utiliser des expansions à partir de $\Gamma$ et à partir des lemmes créés au cours des dérivations à partir de $\Gamma$.

Soit $\sigma$ une substitution. On note $A\sigma$ la formule obtenue en remplaçant toutes les variables libres de $A$ par leur valeur dans la substitution. Lorsque la formule $A$ n'a pas de quantificateurs, on a $\forall(A) \models A\sigma$.

**Lemme 10 (cohérence de la réduction)** Soit $K$ une chaine et $K'$ une chaine obtenue par réduction de $K$. On a : $\models \forall(K) \Rightarrow \forall(K')$.

*Preuve* : Par définition de la réduction, il y a deux littéraux $L$ et $M$, deux chaines $U$ et $V$, une substitution $\sigma$ telle que $K = LU[M]V$, les littéraux $L\sigma$ et $M\sigma$ sont opposés et $K' = (U[M]V)\sigma$.

D'après les propriétés de la fermeture universelle, $\forall(K) \models (LU[M]V)\sigma$.

D'après la cohérence de la réduction pour la logique propositionnelle 6, puisque $M\sigma = \overline{L\sigma}$, nous avons : $\models (LU[M]V)\sigma \Rightarrow (U[M]V)\sigma$.

Donc $\forall(K) \models K'$. D'après les propriétés de la conséquence $\forall(K) \Rightarrow \forall(K')$.

☐

**Lemme 11 (cohérence de l'expansion)** Soit $\Gamma$ un ensemble de chaines élémentaires. Soit $K$ une chaine donnant par expansion avec une chaine de $\Gamma$ la chaine $K'$. On a : $\forall(\Gamma) \models \forall(K) \Rightarrow \forall(K')$.

*Preuve* : Par définition de l'expansion, il y a un littéral $L$ et une chaine $U$ telle que $K = LU$. Il y a une chaine de $\Gamma$ qui s'écrit $VMW$ et une substitution $\sigma$ telle que $L\sigma$ et $M\sigma$ sont deux littéraux opposés et $K' = (VW[M]U)\sigma$.

Puisque les littéraux $L\sigma$ et $M\sigma$ sont opposés, la chaine élémentaire $(VMW)\sigma$ est équivalente à $L\sigma \Rightarrow (VW)\sigma$.

Par suite $\forall(\Gamma) \models L\sigma \Rightarrow (VW)\sigma$, donc $\forall(\Gamma) \models L\sigma \Rightarrow (VW)\sigma * L\sigma$.

D'après le sens des chaines, $(VW)\sigma * L\sigma = ((VW)[L])\sigma$, donc $\forall(\Gamma) \models L\sigma \Rightarrow ((VW)[L])\sigma$.

Par le lemme de monotonie 3, on en déduit $\forall(\Gamma) \models K\sigma \Rightarrow K'$.

D'après la propriété des fermetures universelles, $\forall(K) \models K\sigma$.
D'après les propriétés de la conséquence, $\forall(\Gamma), \forall(K) \models K'$.

Puisque les hypothèses sont sans variables libres, $\forall(\Gamma), \forall(K) \models \forall(K')$.

Et par suite $\forall(\Gamma) \models \forall(K) \Rightarrow \forall(K')$.

☐

**Théorème 12 (cohérence de la méthode)** *Soit Γ un ensemble de chaines élémentaires et K une chaine dérivée de Γ. On a : $\forall(\Gamma) \models \forall(K)$.*

*Preuve :* Puisque K est dérivée (voir 1) de Γ, il y a une dérivation $K_i$ où $1 \le i \le n$ (voir 1) de K à partir de Γ et $K_1 \in \Gamma$.

Puisque $K_1 \in \Gamma$, et d'après les propriétés de la conséquence, on a $\forall(\Gamma) \models \forall(K_1)$.

Des lemmes 11, 10, 5, il résulte que :

pour tout $i$ entre 1 et $n-1$, $\forall(\Gamma) \models \forall(K_i) \Rightarrow \forall(K_{i+1})$.

Donc par récurrence sur la longueur des dérivations :

pour tout $i$ où $1 \le i \le n$, $\forall(\Gamma) \models \forall(K_i)$.

Puisque K est la dernière chaine de la dérivation, $\forall(\Gamma) \models \forall(K)$.

☐

**Corollaire 13 (preuve d'insatisfaisabilité)** *Soit Γ un ensemble de chaines élémentaires. Si la chaine vide est dérivée de Γ alors $\forall(\Gamma)$ est insatisfaisable.*

*Preuve :* Supposons ☐ dérivée de Γ. Alors d'après le théorème ci-dessus, $\forall(\Gamma) \models \square$.

Puisque ☐ est la formule fausse (n'ayant aucun modèle), $\forall(\Gamma)$ n'a aucun modèle. ☐

☐

## 2 Production des lemmes dans le cas propositionnel

À chaque A-littéral d'une chaine, on associe un entier appelé la portée du littéral.

Lors d'une expansion, la portée du nouvel A-littéral est nulle.

Lors d'une réduction, la portée du A-littéral qui sert à effectuer la réduction peut être modifiée. Si le nombre de A-littéraux à gauche de ce A-littéral est plus grande que sa portée actuelle, sa portée devient ce nombre.

Lors de l'enlèvement d'un A-littéral, *un lemme* consistant en la négation tous les A-littéraux dont la portée est égale au nombre de A-littéraux à leur gauche est engendrée. Les portées non nulles de ces A-littéraux sont diminuées de 1.

Remarquons que, au cours d'une dérivation, la portée d'un A-littéral est au plus égale au nombre de A-littéraux à sa gauche. C'est vrai pour la première chaine d'une dérivation, car cette chaine n'a pas de A-littéral. Cette propriété est conservée lors de la création d'un A-littéral par expansion, car sa portée initiale est 0. Cette propriété est aussi conservée par réduction, puisque la portée du A-liitéral utilisée dans la réduction devient égale au nombre de A-littéraux à sa gauche et elle est aussi conservée par l'enlèvement d'un A-littéral.

De cette remarque, il résulte que lorsqu'on enlève le A-littéral $[L]$, sa portée est nulle, donc sa négation fait partie du lemme produit.

Pour faciliter la compréhension de la création des lemmes et la preuve de leur correction, on répète ce qui vient d'être dit, en redéfinissant les trois opérations expansion, réduction et enlèvement, en y ajoutant le calcul des portées nécessaire pour la création des lemmes.
**Expansion** : Soit $LU$ une chaine où $L$ est le B-littéral à gauche de la chaine.

La chaine $VW[L]U$ est obtenue par *expansion* de la chaîne $LU$ avec la chaine élémentaire $V\bar{L}W$.

La portée du nouveau littéral ancêtre $[L]$ est nulle.

**Réduction** : Soit $LU[\bar{L}]V$ une chaine acceptable, où $L$ est le B-littéral le plus à gauche de la chaine et $\bar{L}$ un littéral ancêtre. La chaine $U[\bar{L}]V$ est obtenue par réduction de la chaine $LU[\bar{L}]V$.

Si le nombre de A-littéraux strictement à gauche de ce littéral ancêtre est supérieur à sa portée avant réduction, cette portée devient égale à ce nombre.

**Enlèvement** : Soit $[L]U$ une chaine commençant par le A-littéral $[L]$. La chaine $U$ est obtenue par enlèvement de la chaine $[L]U$.

Un lemme consistant en la négation de ce A-littéral et de tous les autres A-littéraux dont la portée est égale au nombre de A-littéraux à leur gauche est engendré. Les portées non nulles de ces A-littéraux sont diminuées de 1.

L'ajout des lemmes peut *faciliter ou compliquer* les dérivations. Elle peut les faciliter, parce l'usage d'un lemme évite de refaire la dérivation qui a produit ce lemme. Elle peut les compliquer, parce qu'on ajoute des lemmes trop nombreux et inutiles.

Il y a plusieurs politiques d'utilisation des lemmes. On peut les ajouter au cours d'une dérivation, ou lors de la construction d'un arbre des dérivations (une dérivation pouvant ajouter des lemmes utilisés dans une autre dérivation). On peut sélectionner les "meilleurs" lemmes, par exemple les plus courts. On peut remplacer des chaines d'entrées par des lemmes qui les subsument.

Nous n'entrerons pas dans cette politique d'usage des lemmes, qui a fait l'objet de beaucoup d'articles. Nous nous contenterons de prouver que les lemmes engendrés dans une dérivation sont bien des conséquences des chaines d'entrées de la dérivation.

Soit $\Gamma$ un ensemble de chaines élémentaires. Nous présentons une propriété des chaines, vérifiée par toute chaine de $\Gamma$, et conservée par chaque étape expansion avec une chaine de $\Gamma$, réduction, enlèvement. Cette propriété est donc vérifiée par toute chaine dérivée de $\Gamma$ et nous permet de prouver la correction des lemmes.

**Définition 14 (Propriété des chaines dérivées)** Soit $\Gamma$ un ensemble de chaines élémentaires et soit $K$ une chaine. Il existe $n$, où $n \ge 0$, des littéraux $L_i$ où $1 \le i \le n$, des entiers $k_i$ où $1 \le i \le n$, où $k_i$ est la portée du littéral $L_i$, et des chaines élémentaires $U_i$ où $1 \le i \le n+1$ tels que $K = U_1[L_1^{k_1}]...U_n[L_n^{k_n}]U_{n+1}$.

Soit $C_i$ l'ensemble de littéraux défini par $C_i = \{L_j \mid i \le j, j - i \le k_j \le j - 1\}$. On identifie cet ensemble avec la conjonction de ses éléments.

$K$ vérifie la propriété des chaines dérivées relativement à $\Gamma$ si pour $i$ où $1 \le i \le n$, $L_i \in C_i$ et $\Gamma \models C_i \Rightarrow U_1..U_i$.

Le A-literal $L_j^{k_j}$ est utilisé dans la réduction des descendants de $L_{j-k_j}$. Donc pour $k_j = j - 1$ il est utilisé pour réduire des descendants de $L_1$ et pour $k_j = j - i$, il sert à réduire des descendants de $L_i$.

Ainsi $C_i$ est l'ensemble des A-littéraux utilisés pour réduire un B-littéral descendant des A-littéraux $L_1, \dots, L_i$.
Je dois reconnaitre que j’étais incapable de comprendre la preuve de la correction des lemmes à la seule lecture du livre de D.W.Loveland [Don78]. C’est ce qui m’a poussé à rédiger cette explication de méthode ME. Le plus difficile fut de trouver la propriété des chaines qui est invariante au cours des dériva\c\i\es et qui permet d’expliquer la correction des lemmes.

**Lemme 15 (Invariance de la propriété des chaines dérivées)** Soit $\Gamma$ un ensemble de chaines élémentaires et soit $K$ une chaine vérifiant la propriété des chaines dérivées relativement à $\Gamma$. Alors cette même propriété est vérifiée par la chaine $K'$ obtenue par expansion avec une chaine de $\Gamma$, réduction ou enlèvement sur $K$.

Le lemme produit lors de l'enlèvement est conséquence de $\Gamma$.

*Preuve :* Pour la chaine $K$, nous reprenons les notations de la propriété ci-dessus 14.

Puisque $K'$ est une chaine, il existe $p$, où $p \ge 0$, des littéraux $L'_i$ où $1 \le i \le p$, des entiers $k'_i$ où $1 \le i \le p$, et des chaines élémentaires $U'_i$ où $1 \le i \le p+1$ tels que
$$K' = U'_1[L'_1^{k'_1}]...U'_p[L'_p^{k'_p}]U'_{p+1}.$$

Soit $C'_i$ l'ensemble de littéraux défini par $C'_i = \{L'_j \mid i \le j, j - i \le k'_j \le j - 1\}$.

* Supposons que la chaine $K'$ a été produite par expansion de $K$ avec une chaine de $\Gamma$.

Supposons que $K$ commence par le B-littéral $L$ et que l'expansion a été produite avec la chaine $V\bar{L}W$ élément de $\Gamma$.

Notons que $p = n + 1$. Puisqu'un nouveau A-littéral $L'_1 = L$ a été ajouté, on a pour $i$ où $2 \le i \le n+1$, $L'_i = L_{i-1}$, $U'_{i+1} = U_i$.

Puisque le marquage des portées ne change pas (sauf pour le nouvel A-littéral), nous avons pour $i$ où $2 \le i \le n+1$, $L_i^{k'_i} = L_{i-1}^{k_{i-1}}$. En clair la portée du $i$-ème A-littéral de $K'$ est la même que la portée du $i-1$-ème littéral de $K$. Donc pour $2 \le i \le n+1$, on a : $C'_i = C_{i-1}$.

Puisque le nouveau A-littéral est introduit comme $L'_1$ avec la portée 0, par définition de $C'_1$, nous avons :

$$ (a) : L'_{1} \in C'_{1} $$

D'après les hypothèses sur $K$, pour $i$ où $1 \le i \le n$, $L_i \in C_i$, nous avons :

pour $i$ où $1 \le i \le n$, $L_{i+1}' \in C_{i+1}',$ donc, en remplaçant $i+1$ par $j$ et $n+1$ par $p$, on a :

pour $j$ où $2 \le j \le p$, $L_j' \in C_j'$. En y ajoutant la condition (a), on obtient :

$$ (b) : \text{ pour } i \text{ où } 1 \le i \le p, L_i' \in C_i' $$

Ce qui est la première partie de la propriété que doit vérifier $K'$. Il reste à vérifier que pour $j$ où $1 \le j \le p$, $\Gamma \models C'_j \Rightarrow U'_1...U'_j$.

Vu les notations de $K$ et $K'$, on a $U_1 = LX$, $U'_1 = VW$, $U'_2 = X$. Rappelons que l'expansion a été réalisée sur le littéral $L$ avec la chaine $V\bar{L}W$, qui est élément de $\Gamma$.

Puisque cette chaine est équivalente à $L \Rightarrow VW$, il en résulte que $\Gamma \models L \Rightarrow U'_1$ et par le lemme 3, que $\Gamma \models U_1 \Rightarrow U'_1 U'_2$.

D'après la propriété des chaines dérivées de $K$, nous avons pour $i$ où $1 \le i \le n$, $\Gamma \models C_i \Rightarrow U_1...U_i$.
D'après les correspondances déjà citées entre $K$ et $K'$, nous avons

(c) : pour $i$ où $1 \le i \le n$, $\Gamma \models C'_{i+1} \Rightarrow U_1 U'_3 \dots U'_{i+1}$

Puisque $V\bar{L}W \in \Gamma$ et que cette chaine est équivalente à $L \Rightarrow VW$, nous avons
$\Gamma \models L \Rightarrow VW$. Rappelons que $U_1 = LX, VW = U'_1, X = U'_2$. D'après le lemme de
monotonie 3 :

(d) : $\Gamma \models U_1 \Rightarrow U'_1 U'_2$.

De (c) et (d), on déduit que pour $i$ où $1 \le i \le n$, $\Gamma \models C'_{i+1} \Rightarrow U'_1 U'_2 U'_3 \dots U'_{i+1}$

En remplaçant $i+1$ par $j$, on obtient : (e) : pour $j$ où $2 \le j \le p$, $\Gamma \models C'_j \Rightarrow U'_1 \dots U'_j$

Nous savons déjà que $L'_1$ est élément de la conjonction $C'_1$, donc $\Gamma \models C'_1 \Rightarrow U'_1$.

Par suite pour $j$ où $1 \le j \le p$, $\Gamma \models C'_j \Rightarrow U'_1 \dots U'_j$ ce qui termine la preuve que $K'$, obtenue par expansion de $K$, conserve la propriété des chaines dérivées.

* Supposons que $K'$ ait été obtenue par réduction de $K$.

Dans ce cas $p = n$, et les A-littéraux n'ont pas changé. Seule la partie $U_1$ de la
chaine $K$ a été modifiée. En résumé, pour $i$ de 1 à $n$, $L'_i = L_i$ et pour $i$ de 2 à $n+1$,
$U'_i = U_i$.

La chaine $U_1$ s'écrit $LX$ et il y a un A-littéral $L_i$ où $i \ge 1$ et $L_i = \bar{L}$ et $U'_1 = X$.

Par définition de la réduction, la portée du littéral $L'_i$ est égale à $i-1$ (le nombre
de A-littéraux à gauche de $L'_i$) dans $K'$. Dans la suite nous réservons $i$ comme
l'indice du littéral ayant causé la réduction.

Puisque pour tout $j$ tel que $1 \le j \le n$ et $j \ne i$, $k_j = k'_j$ et que $k'_i = i - 1$, nous
avons pour tout $j$ tel que $1 \le j \le n$, $C'_j = C_j \cup \{L_i\}$.

Puisque $K$ verifie pour tout $j$ tel que $1 \le j \le n$, $L_j \in C_j$, et que pour tout $j$ tel
que $1 \le j \le n$, $L'_j = L_j$ et $C'_j = C_j \cup \{L_i\}$, nous avons :

pour $j$ tel que $1 \le j \le n$, $L'_j \in C'_j$ est une propriété vérifiée par $K'$.

Ainsi $K'$ verifie la première partie de la propriété des chaines dérivées. Il reste à
prouver que pour $j$ de $1$ à $n-1$, $\Gamma \models C'_j \Rightarrow U'_1 \dots U'_j$.

Puisque $L_i = \bar{L}$ et que pour tout $j$ tel que $1 \le j \le n$, $C'_j = C_j \cup \{L_i\}$, nous avons :

(a) : pour tout $j$ où $1 \le j \le n$, $\models C'_j \Rightarrow \bar{L}$.

D'après le lemme 3, nous avons :

(b) : $\models \bar{L} \Rightarrow U_1 \Rightarrow U'_1$

Des propositions (a) et (b), on déduit :

(c) : pour tout $j$ où $1 \le j \le n$, $\models C'_j \Rightarrow U_1 \Rightarrow U'_1$.

Puisque, pour tout $j$, $C'_j = C_j \cup \{L_i\}$ et que ces ensembles sont considérés comme
la conjonction de leurs éléments, nous avons, pour tout $1 \le i \le n$, $\models C'_i \Rightarrow C_i$.

Vu la propriété des chaines dérivées vérifiée par $K$, nous avons :

$\Gamma \models C_i \Rightarrow U_1 \dots U_i$.

Puisque $C'_i$ implique $C_i$, nous avons :

(d) : $\Gamma \models C'_i \Rightarrow U_1 \dots U_i$.

D'après (c), (d) et puisque pour $1 < i$, $U_i = U'_i$, nous avons :

pour tout $i$ où $1 \le i \le n$, $\Gamma \models C'_i \Rightarrow U'_1 \dots U'_i$.

Par suite la chaine $K'$ dérivée par réduction de $K$, vérifie aussi la propriété des
chaines dérivées.
* Supposons que la chaine $K'$ ait été obtenue par enlèvement sur la chaine $K$.
Nous montrons tout d'abord que lemme créé lors l'enlèvement est conséquence de $\Gamma$. Lors de l'enlèvement, $U_1 = \square$.

D'après la propriété des chaines dérivées vérifiée par $K$, on a pour $i$ où $1 \le I \le n$, $\Gamma \models C_i \Rightarrow U_1 \dots U_i$.

Par suite $\Gamma \models C_1 \Rightarrow \square$. Noter que $C_1$ est la conjonction (et l'ensemble) des littéraux $L_i$, dont la portée est $i-1$, c'est-à-dire le nombre de A-littéraux à gauche de $L_i$.

La formule $C_1 \Rightarrow \square$ est équivalente à la disjonction des opposés de ces littéraux, représentée par la chaine élémentaire comportant la liste des opposés de ces littéraux. Le lemme engendré, lors de l'enlèvement, est donc bien une conséquence de $\Gamma$.

La décrémentation des portées, après l'enlèvement du premier A-littéral de $K$, fait que les autres A-littéraux de $K$ qui avaient leur portée égale au nombre de leur A-littéraux à gauche, restent les mêmes dans $K'$. Formellement, cela veut dire que là où nous avions $k_j = j-1$ dans $K$, nous avons $k'_{j-1} = j-2$ dans $K'$. Cette remarque implique que pour $j$ tel que $2 \le j \le n$, $C_j = C'_{j-1}$.

Dans le cas de l'enlèvement, $p = n-1$, $U_1 = \square$ et d'après notre notation de $K'$, pour $j$ de 2 à $n$, $L_j = L'_{j-1}$, pour $j$ de 2 à $n+1$, $U_j = U'_{j-1}$.

La chaine $K$ verifie : pour $j$ tel que $1 \le j \le n$, $L_j \in C_j$ et $\Gamma \models C_j \Rightarrow U_1 \dots U_j$.

Puisque $L_j = L'_{j-1}$, $C_j = C'_{j-1}$, $U_j = U'_{j-1}$ et $U_1 = \square$, nous avons pour $j$ tel que $2 \le j \le n$, $L'_{j-1} \in C'_{j-1}$ et $\Gamma \models C'_{j-1} \Rightarrow U'_1 \dots U'_{j-1}$

En remplaçant $j-1$ par $k$ et sachant $p = n-1$, nous concluons que : pour $k$ tel que $1 \le k \le p$, $L'_k \in C'_k$ et $\Gamma \models C'_k \Rightarrow U'_1 \dots U'_k$.

Ainsi l'enlèvement conserve bien la propriété des chaines dérivées.

□

**Théorème 16** Soit $\Gamma$ un ensemble de chaines élémentaires. Toutes les chaines d'une dérivation à partir de $\Gamma$ et commençant par une chaine de $\Gamma$ vérifient la propriété des chaines dérivées 14 et les lemmes produits au cours de cette dérivation sont conséquences de $\Gamma$.

*Preuve* : La chaine $C$ à l'origine d'une telle dérivation, n'ayant aucun A-littéral et étant élément de $\Gamma$, vérifie la propriété des chaines dérivées. En effet, en absence de A-littéraux, puisque la conjonction d'un ensemble vide (de littéraux) est toujours vraie, cette propriété se réduit à $\Gamma \models C$. Puisque $C$ est élément de $\Gamma$, la propriété est vérifiée.

Cette propriété étant préservée par chaque étape d'une dérivation d'après 15, toutes les chaines de la dérivation la vérifient.

Lors d'un enlèvement sur une chaine vérifiant la propriété des chaines dérivées 14, le lemme produit est conséquence de $\Gamma$. Puisque toutes les chaines d'une dérivation vérifient cette propriété, lors de chaque enlèvement au cours de la dérivation, les lemmes produits sont conséquences de $\Gamma$. □
### 3 Production des lemmes en logique du premier ordre

Le marquage des portées est presque le même que dans le cas propositionnel. Lors d'une expansion, la portée du nouvel A-littéral est nulle. Lors d'une réduction, la portée du A-littéral qui sert à effectuer la réduction *peut être modifiée*. Si le nombre de A-littéraux à gauche de ce A-littéral est plus grande que sa portée actuelle, sa portée *devient* ce nombre. Lors de l'enlèvement d'un A-littéral, *un lemme* consistant en les opposés de tous les A-littéraux dont la portée est égale au nombre de A-littéraux à leur gauche est engendrée. Les portées non nulles de ces A-littéraux (sauf évidemment celui qui a été enlevé) sont diminuées de 1. Pour éviter toute ambiguïté on redéfinit les trois opérations expansion, réduction et enlèvement, en y ajoutant le calcul des portées nécessaire pour la création des lemmes.

**Expansion :** Soit $LU$ une chaine acceptable où $L$ est le B-littéral à gauche de la chaine.

Soit $C$ une chaine élémentaire.

Soit $C'$ une copie de la chaine $C$, dont les variables ne figurent pas dans $LU$.

Supposons que $C' = WMW$ où $M$ est un littéral et qu'il existe $\sigma$ un unificateur principal de $L$ et de l'opposé du littéral $M$. Alors la chaine $(VW[L]U)\sigma$ est obtenue par *expansion* de la chaîne $LU$ avec la chaine $C$.

La portée du nouveau littéral ancêtre $[L\sigma]$ est nulle.

Notons aussi que les portées définies dans $U$ et dans $U\sigma$ sont conservées, plus précisement la portée du $i$-ème littéral de la chaine $U$ et la chaine $U\sigma$ sont identiques, en bref les portées sont préservées par substitution.

**Réduction :** Soit $LU[M]V$ une chaine acceptable, où $L$ est le B-littéral le plus à gauche de la chaine et $[M]$ un littéral ancêtre, tel qu'il y a un unificateur principal $\sigma$ entre $L$ et l'opposé de $M$ alors la chaine $(U[M]V)\sigma$ est obtenue par réduction de la chaine $LU[M]V$.

Si le nombre de A-littéraux strictement à gauche de ce littéral ancêtre est supérieur à sa portée avant réduction, cette portée devient égale à ce nombre.

Comme pour l'expansion, les portées des autres A-littéraux sont préservées par substitution.

**Enlèvement :** Soit $[L]U$ une chaine commençant par le A-littéral $[L]$. La chaine $U$ est obtenue par enlèvement de la chaine $[L]U$.

Un lemme consistant en la négation de ce A-littéral et de tous les autres A-littéraux dont la portée est égale au nombre de A-littéraux à leur gauche est engendré. Les portées non nulles de ces A-littéraux sont diminuées de 1.

Nous ne faisons pas dans le cas du premier ordre, toutes les preuves nécessaires pour assurer la correction des lemmes. Nous donnons seulement la propriété des chaines dérivées, invariante au cours des dérivations et nous admettons cette invariance. Dans la propriété de la chaine dérivée, on constate que la seule différence avec le cas propositionnel est le remplacement de $\Gamma$ par sa fermeture universelle $\forall(\Gamma)$.

La preuve de l'invariance de la propriété ci-dessous, à chaque étape d'une dérivation, est analogue au cas propositionnel, compliquée par les substitutions. Nous laissons cette preuve au lecteur courageux.
**Définition 17 (Propriété des chaines dérivées)** Soit $\Gamma$ un ensemble de chaines élémentaires et soit $K$ une chaine.

Il existe $n$, où $n \ge 0$, des littéraux $L_i$ où $1 \le i \le n$, des entiers $k_i$ où $1 \le i \le n$, où $k_i$ est la portée du littéral $L_i$, et des chaines élémentaires $U_i$ où $1 \le i \le n+1$ telles que
$$K = U_1[L_1^{k_1}]...U_n[L_n^{k_n}]U_{n+1}.$$

Soit $C_i$ l'ensemble de littéraux défini par $C_i = \{L_j \mid i \le j, j - i \le k_j \le j - 1\}$. On identifie l'ensemble $C_i$ avec la conjonction de ses éléments.

$K$ vérifie la propriété des chaines dérivées relativement à $\Gamma$ si pour i où $1 \le i \le n$, $L_i \in C_i$ et $\forall(\Gamma) \models C_i \Rightarrow U_1..U_i$.

**Théorème 18** Soit $\Gamma$ un ensemble de chaines élémentaires. Tout lemme produit durant une dérivation à partir de $\Gamma$ est une conséquence of $\forall(\Gamma)$.

*Preuve:* Soit $K$ une chaine dérivée de $\Gamma$, commençant par un A-littéral. Le lemme produit par l'enlèvement de cet A-littéral est la chaine élémentaire composée par les opposés des A-littéraux de la chaine dont la portée est égale au nombre de A-littéraux à leur gauche.

D'après l'invariance de la propriété des chaines dérivées, nous savons que $K$ vérifie cette propriété. Donc $\forall(\Gamma) \models C_1 \Rightarrow \Box$, où $C_1$ est la conjonction des A-littéraux de la chaine, dont la portée est égale au nombre de littéraux à leur gauche. Le lemme engendré est équivalent à la formule $C_1 \Rightarrow \Box$, donc il est conséquence de $\forall(\Gamma)$. $\Box$

# 4 Complétude de la méthode

Nous montrons la complétude de la méthode. Soit $\Gamma$ un ensemble de chaines élémentaires. Dans le cas propositionnel, on montre que si $\Gamma$ est insatisfaisable, alors la chaine vide est dérivée de $\Gamma$. Dans le cas du premier ordre, on montre que si $\forall(\Gamma)$ est insatisfaisable, alors la chaine vide est dérivée de $\Gamma$.

## 4.1 Complétude de la méthode dans le cas propositionnel

**Propriété 19** Soit $\Gamma$ un ensemble de chaines élémentaires. Soit $C$ une chaine et $D_1, \dots, D_k$ une dérivation à partir de $\Gamma$. Alors $D_1 C, \dots D_k C$ est aussi une dérivation à partir de $\Gamma$.

*Preuve:* Il suffit de vérifier que si la chaine $E$ donne $F$ par expansion à partir de $\Gamma$ (respectivement réduction ou enlèvement) alors $EC$ donne $FC$ par expansion à partir de $\Gamma$ (respectivement réduction ou enlèvement). $\Box$

**Théorème 20** Soit $\Gamma$ un ensemble minimalement insatisfaisable de chaines élémentaires. Pour toute chaine élémentaire $C \in \Gamma$, il y a une dérivation (au sens de 1) de la clause vide, commençant par la clause $C$, à partir de $\Gamma$.
*Preuve* : Appelons longueur d'un ensemble de chaines, la somme des longueurs des chaines de l'ensemble. La preuve est faite par récurrence sur la longueur de Γ. Supposons le théorème vérifié quand la longueur de Γ est inférieur à *n*. Soit Γ de longueur *n*. Montrons que le théorème est encore vérifié.

Soit $C$ une clause de $\Gamma$. On distingue deux cas suivant que $C$ est une clause unitaire ou non unitaire.

* $C$ est unitaire, c'est-à-dire est une chaine de longueur 1. Soit $L$ l'unique littéral de la chaine.

Dans $\Gamma$, il y a une chaine $D = U\overline{L}V$. Supposons que, au contraire, aucune chaine de $\Gamma$ ne comporte le littéral $\overline{L}$. Si $\Gamma - \{C\}$ avait un modèle $v$, alors $v[L := 1]$ serait modèle de $\Gamma$. Puisque $\Gamma$ est insatisfaisable, $\Gamma - \{C\}$ est aussi insatisfaible, ce qui contredit le fait que $\Gamma$ est minimalement insatisfaisable.

Soit $D' = UV$ et $\Delta = (\Gamma - \{D\}) \cup \{D'\}$. On vérifie facilement que $\Delta$ et $\Gamma$ sont équivalents. Puisque $\Gamma$ est minimalement insatisfaisable, $\Gamma - \{D\}$ est satisfaisable, dont tout sous-ensemble minimalement insatisfaisable de $\Delta$ comporte $D'$. Soit $\Lambda$ un tel sous-ensemble. Puisque la longueur de $\Delta$ est inférieure à $n$, donc aussi celle de $\Lambda$, l'hypothèse de récurrence s'applique à $\Lambda$. Donc il y a une dérivation $R_0, \dots, R_k$ de la clause vide commançant par $D'$ à partir de $\Lambda$. D'après la propriété 19, $R_0[L], \dots, R_k[L]$ est une dérivation de la chaine $[L]$ commençant par $D'[L]$ à partir de $\Lambda$.

La clause $C$ où $C = L$ donne par extension avec $D$, la chaine $D'[L]$. Par suite $C, R_0[L], \dots, R_k[L]$, $\square$ est une dérivation, commençant par $C$, de la chaine vide à partir de $\Gamma$.

* $C$ n'est pas unitaire, donc $C = LC'$ où $L$ est un littéral et $C'$ une chaine non vide. Soit $\Delta$ un sous-ensemble minimalement insatisfaisable de $(\Gamma - \{C\}) \cup \{L\}$ et $\Lambda$ un sous-ensemble minimalement insatisfaisable de $(\Gamma - \{C\}) \cup \{C'\}$. Puisque $\Gamma$ est minimalement insatisfaisable, $L \in \Delta$ et $C' \in \Delta$.

Puisque les longueurs de $\Delta$ et de $\Lambda$ sont inférieurs à $n$, par hypothèse de récurrence, il y a une dérivation $R_0, \dots, R_k$ commençant par $L$ et terminée par la clause vide à partir de $\Delta$ ainsi qu'une dérivation $S_0, \dots, S_l$ commençant pas $C'$ et terminée par la clause vide à partir de $\Lambda$.

D'après la propriété 19, $R_0S_0, \dots, R_kS_0$ est une dérivation commençant par $C$ et terminée par $C'$ à partir de $\Gamma$. Par suite $R_0S_0, \dots, R_kS_0, S_1, \dots, S_l$ est une dérivation commençant par $C$ et terminée par la clause vide à partir de $\Gamma$.

$\square$

**Corollaire 21** *Soit Γ un ensemble insatisfaisable de chaines élémentaires sans variables. La chaine vide est dérivée de Γ.*

*Preuve* : Puisque $\Gamma$ est insatisfaisable, il contient un ensemble $\Delta$ minimalement insatisfaisable. D'après le théorème 20, la chaine vide est dérivée de $\Delta$, donc aussi de $\Gamma$.
$\square$
## 4.2 Complétude de la méthode dans le cas du premier ordre

La preuve de la complétude suit le modèle usuel. Soit $\Gamma$ un ensemble de chaines élémentaires. Supposons que $\forall(\Gamma)$ est insatisfaisable. Alors, d'après les résultats de Herbrand, il existe un ensemble fini insatisfaisable $\Delta$ d'instances des chaines de $\Gamma$ sur le domaine de Herbrand. D'après la sous-section préccédente, il existe une dérivation de la chaine vide commençant par une chaine de $\Delta$. On montre que cette dérivation "propositionnelle" peut être relevée en une dérivation "au premier ordre" de la chaine vide, commençant par une chaine de $\Gamma$, à partir de $\Gamma$.

**Lemme 22 (Relèvement de l'expansion)** Soit $C$ une chaine et $D$ une chaine élémentaire. Soit $C'$ une instance sans variable de $C$, $D'$ une instance sans variable de $D$ et $E'$ une expansion propositionnelle de $C'$ avec $D'$. Il existe $E$ une expansion au premier ordre de $C$ avec $D$ d'instance $E'$.

*Preuve :* Puisque $E'$ est une expansion de $C'$ avec $D'$, la chaine $C'$ s'écrit $lu$ où $l$ est un littéral et la chaine $D'$ s'écrit $v\bar{l}w$ et $E' = vw[l]u$.

Puisque $C'$ est une instance de $C$, il existe une substitution $\sigma$ telle que $C = LU$ où $L$ est un littéral tel que $L\sigma = l$ et $U$ une chaine telle que $U\sigma = u$.

Puisque $D'$ est une instance de $D$, il existe une substitution $\tau$ telle que $D = VMW$ où $M$ est un littéral tel que $M\tau = \bar{l}$, $V$ est une chaine vérifiant $V\tau = v$ et $W$ une chaine vérifiant $W\tau = w$.

Soit $\rho$ un renommage de $D$ tel que $D\rho$ et $C$ n'aient pas de variable commune. $\rho$ est une bijection entre les variables de $D$ et celles de $D\rho$. Notons $\rho^{-1}$ l'inverse de $\rho$ (sur les variables de $D\rho$). Soit $\pi$ la substitution suivante :

- pour $x$ variable de $C$, $x\pi = x\sigma$

- pour $x$ variable de $D\rho$, $x\pi = x\rho^{-1}\tau$

- pour tout autre variable $x$, $x\pi = x$

Puisque $C$ et $D\rho$ n'ont pas de variable commune, la substitution $\pi$ est bien définie.

Par définition de $\pi$, nous avons d'une part $L\sigma = l = L\pi$. D'autre part, on a $\bar{M}\tau = l = \bar{M}\rho\rho^{-1}\tau$ car $\rho\rho^{-1}$ est l'identité, et, par définition de $\pi$, on obtient $L\pi = l = \bar{M}\rho\pi$.

Donc $\pi$ unifie $L$ et $\bar{M}\rho$. Soit $\lambda$ l'unificateur principal de ces deux littéraux. Il existe une substitution $\lambda'$ telle que $\pi = \lambda\lambda'$.

Soit $E = (VW)\rho\lambda[L]\lambda(U\lambda)$. $E$ est une expansion au premier ordre de $C$ avec $D$ et $E\lambda' = E'$, donc $E'$ est une instance de $E$. En effet :

$$ \text{— } (VW)\rho\lambda\lambda' = (VW)\rho\pi = (VW)\rho\rho^{-1}\tau = (VW)\tau = vw $$

$$ \text{— } [L]\lambda\lambda' = [L]\pi = [L]\sigma = l $$

$$ \text{— } U\lambda\lambda' = U\pi = U\sigma = u $$

□

**Lemme 23 (Relèvement de la réduction)** Soit $C$ une chaine, $C'$ une instance sans variable de $C$ et $D'$ obtenue par réduction propositionnelle de $C'$. Il existe $D$ une réduction au premier ordre de $C$ ayant comme instance $D'$.
Preuve : La preuve (simple) est laissée au lecteur. ☐

**Lemme 24 (Relèvement d'un enlèvement)** Soit C une chaine, C' une instance sans variable de C et D' obtenue par enlèvement sur C'. Il existe D une chaine obtenue par enlèvement sur C ayant comme instance D'.

Preuve : La preuve (triviale) est laissée au lecteur. ☐

**Théorème 25** Soit $\Gamma$ un ensemble de chaines élémentaires, $\Delta$ un ensemble d'instances sans variables des chaines de $\Gamma$ et $C_1, \dots, C_k$ une dérivation propositionnelle à partir de $\Delta$ commençant par une chaine de $\Delta$. Il existe une dérivation au premier ordre $D_1, \dots, D_k$ à partir de $\Gamma$ commençant par une chaine de $\Gamma$, telle que pour $i$ où $1 \le i \le k$, la chaine $C_i$ est une instance de $D_i$.

Preuve : Par récurrence sur $k$. Pour $k=1$, le théorème est conséquence de ce que $C_1$ est une instance d'une chaine de $\Gamma$. Supposons le théorème vérifié pour $k$. Soit $C_1, \dots, C_k, C_{k+1}$ une dérivation propositionnelle à partir de $\Delta$ commençant par une chaine de $\Delta$.

Par hypothèse de récurrence, il existe une dérivation au premier ordre $D_1, \dots, D_k$ à partir de $\Gamma$ commençant par une chaine de $\Gamma$, telle que pour $i$ où $1 \le i \le k$, la chaine $C_i$ est une instance de $D_i$.

Supposons $C_{k+1}$ obtenue par expansion de $C_k$ avec une chaine de $\Delta$. Puisque $C_k$ est une instance de $D_k$ et qu'un chaine de $\Delta$ est une instance d'une chaine de $\Gamma$, d'après le lemme 22, il existe $E$ une expansion au premier ordre de $D_k$ avec une chaine de $\Gamma$ ayant pour instance $C_{k+1}$. On prend donc $D_{k+1} = E$.

Grâce aux lemmes 23 et 24, les cas où $C_{k+1}$ est obtenue par réduction ou enlevement sont analogues. ☐

**Corollaire 26 (Complétude la méthode Model Elimination)** Soit $\Gamma$ un ensemble de chaines élémentaires telle que $\forall(\Gamma)$ est insatisfaisable. La chaine vide est dérivée (au premier ordre) de $\Gamma$.

Preuve : Puisque $\forall(\Gamma)$ est insatisfaisable, d'après les résultats de Herbrand, il existe un ensemble fini $\Delta$ insatisfaisables de chaines sans variables instances de chaines de $\Gamma$. D'après le corollaire 21, il existe une dérivation *propositionnelle* de la clause vide.

D'après le theoreme 25, il existe une dérivation *au premier ordre* commençant par une chaine de $\Gamma$ et terminée par une chaine, dont la clause vide est une instance. La dernière chaine de cette dérivation est donc la clause vide. Par suite la clause vide est dérivée au premier ordre de $\Gamma$. ☐
Références

[Don78] Donald.W.Loveland. *Automated Theorem Proving : A Logical Basis*. North-Holland, 1978.

[OD97] O.L.Astrachan and D.W.Loveland. The use of lemmas in the model elimination procedure. *Journal of Automated Reasoning*, 19:117–141, 1997.

[Sut12] Geoff Sutcliffe. Chain format linear refinements. http://www.cs.miami.edu/home/geoff/Courses/CSC648-12S/Content/ChainFormat.shtml, 2012.