<figure><img src="image_1.png" /></figure>

HAL
open science

# Une logique pour représenter des variations propositionnelles (version étendue)

Nicolas François, Thomas Laure, Jean Lieber

► To cite this version:

Nicolas François, Thomas Laure, Jean Lieber. Une logique pour représenter des variations propositionnelles (version étendue). Université de Lorraine (France). 2023, pp.30. hal-04147988

HAL Id: hal-04147988

https://inria.hal.science/hal-04147988

Submitted on 1 Jul 2023

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.

Public Domain
# Une logique pour représenter des variations propositionnelles
(version étendue)

Nicolas François<fnref n="1" />

Thomas Laure²

Jean Lieber<fnref n="1" />

1 Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France

2 DIENS, École Normale Supérieure, CNRS, Université PSL, 75005 Paris, France

Juin 2023

Ce document est une version longue de l'article éponyme (si on excepte le « version étendu ») accepté pour publication dans les actes des journées d'intelligence artificielle fondamentale de 2023 <fnref n="1" />. Il contient des preuves que l'article ne contenait pas.

## Résumé

La logique propositionnelle (comme d'autres logiques) peut être vue comme une façon de représenter des ensembles d'états du monde (les interprétations). La représentation de variations d'un ensemble d'états du monde à un autre est motivée par des travaux sur le raisonnement à partir de cas : la comparaison entre deux problèmes et le passage d'une solution à une autre peuvent être vus comme des variations d'un ensemble d'états à un autre. Cela a conduit à une notation pour représenter ces variations (une syntaxe) et ce rapport étudie comment associer à cette notation une sémantique en théorie des modèles dans laquelle une interprétation est un couple d'interprétations en logique propositionnelle (un des états et l'autre). Le rapport entame une étude classique de cette logique (syntaxe, sémantique, équivalences, NP-complétude de la satisfiabilité, etc.) et de façons d'associer à un couple de formules propositionnelles une formule de cette logique. Le rapport se termine par une discussion envisageant une poursuite de cette étude et des applications potentielles.

## Sommaire

<table><tr><td>1 Introduction et motivations</td><td>2</td></tr><tr><td>2 Rappels sur la logique propositionnelle</td><td>4</td></tr><tr><td>3 La logique des variations propositionnelles</td><td>4</td></tr><tr><td>3.1 Syntaxe</td><td>4</td></tr><tr><td>3.2 Sémantique</td><td>5</td></tr><tr><td>3.3 Propriétés</td><td>5</td></tr><tr><td>4 Variation d'une formule propositionnelle à une autre</td><td>8</td></tr><tr><td>4.1 Définition d'un opérateur de variation</td><td>8</td></tr><tr><td>4.2 Une extension de la syntaxe de la logique des variations propositionnelles</td><td>8</td></tr><tr><td>4.3 Étude de l'opérateur ▷</td><td>10</td></tr><tr><td>4.4 D'autres opérateurs de variations entre formules</td><td>13</td></tr></table>

<footnote n="1">1. https://pfia23.icube.unistra.fr/conferences/jiaf/</footnote>
L'étape (2) s'appuie typiquement sur des connaissances d'adaptation, souvent représentées par des règles d'adaptation. En général, la prémisse d'une telle règle contient une variation entre problèmes et sa conclusion, une variation entre solutions : « Si deux problèmes varient selon $\Delta x$ alors leurs solutions varient selon $\Delta y$. » De telles règles peuvent être apprises à partir de la base de cas, selon un principe introduit dans [9] et qui a été appelé l'heuristique des variations entre cas (case difference heuristics, voir par exemple [12]<fnref n="3" />). L'idée est d'appliquer un processus d'apprentissage artificiel avec comme jeu d'apprentissage des couples $(\Delta x^{ij}, \Delta y^{ij})$ où $(x^i, y^i), (x^j, y^j) \in BC$ et $\Delta x^{ij}$ (resp., $\Delta y^{ij}$) est la variation entre $x^i$ et $x^j$ (resp., entre $y^i$ et $y^j$).

Dans certaines applications du RàPC, les problèmes et les solutions peuvent être représentés (ou traduits) sous la forme de propriétés booléennes, qu'on peut coder sous la forme de conjonctions de variables booléennes. Par exemple, on peut considérer les deux problèmes suivants :

$$x^i = a \wedge \neg b \wedge \neg c \wedge d$$

$$x^j = a \wedge \neg b \wedge c \wedge \neg d$$

La variation entre ces problèmes a été notée de la façon suivante dans certains travaux sur l'apprentissage de connaissances d'adaptation s'appuyant sur cette heuristique des variations :

$$\Delta x^{ij} = a^{=v} \wedge b^{=f} \wedge c^{+} \wedge d^{-}$$

où $a^v$ signifie que la propriété booléenne varie selon $v$ où $v = =v$ (resp. $v = =f$) signifie « reste à $v$ (resp. à $f$) » et $v = +$ (resp. $v = -$) signifie « change de $f$ à $v$ » (resp. de $v$ à $f$).

À titre d'exemple, l'apprentissage de règles d'adaptation a été étudiée pour un système de RàPC culinaire [5]. Supposons qu'on trouve dans un livre de recettes (constituant la base de cas) des couples de recettes de desserts similaires dont la première contient des pommes et de la cannelle et la seconde, des poires et du chocolat (mais pas de poires ni de chocolat dans la première et pas de pommes ni de cannelle dans la seconde). À partir de ces couples, on peut apprendre la règle d'adaptation suivante :

Dans les recettes de desserts avec des pommes et de la cannelle, on peut remplacer ces deux ingrédients par des poires et du chocolat.

Cette règle d'adaptation peut s'écrire par l'expression suivante :

$$R = rDessert^{=v} \wedge iPomme^{-} \wedge iCannelle^{-} \wedge iPoire^{+} \wedge iChocolat^{+} \quad (1)$$

(où $rDessert$ est la propriété d'être une recette de dessert, $iPomme$, celle d'être une recette avec des pommes, etc.).

Les expressions telles que celles présentées ci-dessus ne constituent à ce stade qu'une *notation*, pas un formalisme logique, puisqu'on dispose d'une syntaxe mais pas de sémantique permettant de définir des inférences. L'objectif de ce rapport est de définir une telle sémantique et d'entamer son étude. Partant de la logique propositionnelle finie ($\mathcal{LP}, \models$), sera définie la logique $(\Delta \mathcal{LP}, \models)$ dont la syntaxe contient les formules telles que celle de la notation introduite ci-dessus et la sémantique sera définie en théorie des modèles.

La section 2 rappelle des notions et notations relatives à la logique propositionnelle finie. La section 3 définit la logique $(\Delta \mathcal{LP}, \models)$ et présente quelques résultats élémentaires à son sujet. Étant donné deux formules propositionnelles $\alpha$ et $\beta$, comment définir leurs variations par une formule de $(\Delta \mathcal{LP}, \models)$ ? La section 4 étudie cette question. Le rapport se termine par une discussion (section 5) qui montre que les directions de recherche pour poursuivre ce travail sont nombreuses.

<footnote n="3">3. Les auteurs ont hésité entre le terme « différence » et le terme « variation ». L'argument qui a fait préférer le second est qu'on s'attend à ce que la différence entre un objet et lui-même soit indépendante de cet objet, ce qu'on attend moins d'une variation.</footnote>
## 2 Rappels sur la logique propositionnelle

Soit $\mathcal{V}$ un ensemble fini et non vide de symboles, appelés variables. Une formule est soit une variable (atome de cette logique) soit une expression d'une des formes suivantes : $\neg\alpha$, $\alpha_1 \wedge \alpha_2$ et $\alpha_1 \vee \alpha_2$, où $\alpha$, $\alpha_1$ et $\alpha_2$ sont des formules. On étend cette syntaxe avec d'autres connecteurs considérés comme des abréviations (où $a$ est une variable) : $\bot = a \wedge \neg a$, $\top = \neg \bot$, $\alpha_1 \rightarrow \alpha_2 = \neg \alpha_1 \vee \alpha_2$, $\alpha_1 \leftrightarrow \alpha_2 = (\alpha_1 \rightarrow \alpha_2) \wedge (\alpha_2 \rightarrow \alpha_1)$ et $\alpha_1 \oplus \alpha_2 = \neg(\alpha_1 \leftrightarrow \alpha_2)$. $\mathcal{LP}$ est l'ensemble des formules de cette logique. Pour éviter d'écrire trop de parenthèses, on utilise la priorité des connecteurs usuelle : $\neg$ avant les autres ; $\wedge$ et $\vee$ avant les autres connecteurs sauf $\neg$. Ainsi $\neg a \vee b \rightarrow c \wedge \neg d$ se lira $((\neg a) \vee b) \rightarrow (c \wedge (\neg d))$. Un littéral est une formule de la forme $a$ ou de la forme $\neg a$ où $a \in \mathcal{V}$. La taille d'une formule $\alpha$, $|\alpha|$, est le nombre d'occurrences de connecteurs de $\alpha$.

Une interprétation $\mathcal{I}$ est une fonction de $\mathcal{V}$ dans $\{f, v\}$ où $f$ et $v$ dénotent respectivement les valeurs booléennes « faux » et « vrai ». L'ensemble des interprétations est dénoté par $\Omega$. Pour $\mathcal{I} \in \Omega$ et $\alpha \in \mathcal{LP}$, on définit $\mathcal{I} \models \alpha$ — « $\mathcal{I}$ satisfait $\alpha$ » — de la façon suivante (pour $a \in \mathcal{V}$ et $\alpha, \alpha_1, \alpha_2 \in \mathcal{LP}$) :

$$ \neg \mathcal{I} \models a \text{ si } \mathcal{I}(a) = v; $$

$$ \neg \mathcal{I} \models \neg \alpha \text{ si } \mathcal{I} \not\models \alpha; $$

$$ \neg \mathcal{I} \models \alpha_1 \wedge \alpha_2 \text{ si } \mathcal{I} \models \alpha_1 \text{ et } \mathcal{I} \models \alpha_2. $$

$$ \neg \mathcal{I} \models \alpha_1 \vee \alpha_2 \text{ si } \mathcal{I} \models \alpha_1 \text{ ou } \mathcal{I} \models \alpha_2 \text{ (ou les deux).} $$

Un modèle d'une formule $\alpha$ est une interprétation $\mathcal{I}$ qui satisfait $\alpha$ et l'ensemble des modèles de $\alpha$ est dénoté par $M(\alpha)$. Une formule $\alpha_1$ entraîne une formule $\alpha_2$, noté $\alpha_1 \models \alpha_2$, si $M(\alpha_1) \subseteq M(\alpha_2)$. Les formules $\alpha_1$ et $\alpha_2$ sont équivalentes, noté $\alpha_1 \equiv \alpha_2$, si $M(\alpha_1) = M(\alpha_2)$. Une formule $\alpha$ est une tautologie (noté $\models \alpha$) si $M(\alpha) = \Omega$. Une formule $\alpha$ est satisfiable si $M(\alpha) \neq \emptyset$.

Une façon équivalente de considérer la logique propositionnelle consiste à considérer chaque formule $\alpha \in \mathcal{LP}$ comme une représentation d'un sous-ensemble $M(\alpha)$ de $\Omega$. La logique propositionnelle peut alors être vue comme l'étude de $2^\Omega$, l'ensemble des parties de $\Omega$ via l'utilisation d'intersections, d'unions et de complémentaires (l'algèbre de Boole finie $(2^\Omega, \cap, \cup, \neg)$).

Soit $\mathcal{B} = \{\alpha_1, \alpha_2, \dots, \alpha_p\}$ un ensemble fini de formules. $\bigwedge \mathcal{B}$ dénote $\alpha_1 \wedge \alpha_2 \wedge \dots \wedge \alpha_p$. $\bigvee \mathcal{B}$ dénote $\alpha_1 \vee \alpha_2 \vee \dots \vee \alpha_p$. On écrira $\mathcal{B} \models \beta$ si $\bigwedge \mathcal{B} \models \beta$, pour $\beta \in \mathcal{LP}$.

## 3 La logique des variations propositionnelles

Cette section définit la logique $(\Delta\mathcal{LP}, \models)$ sur la base de la logique propositionnelle $(\mathcal{LP}, \models)$.

### 3.1 Syntaxe

Soit $\mathcal{D}$ l'ensemble de symboles suivant :

$$ \mathcal{D} = \mathcal{D}_0 \cup \mathcal{D}_1 \quad \text{où} \quad \mathcal{D}_0 = \{=f, =v, +, -\} \text{ et } \mathcal{D}_1 = \{=, \neq, f\bullet, \bullet f, v\bullet, \bullet v\} $$

Un $v \in \mathcal{D}$ est appelé symbole de variation ; si $v \in \mathcal{D}_0$, $v$ est un symbole de variation primitif.

$\Delta\mathcal{LP}$ est l'ensemble des expressions obtenues en substituant dans les formules propositionnelles les variables par des expressions $a^v$ où $a \in \mathcal{V}$ et $v \in \mathcal{D}$. Un tel $a^v$ est appelé atome de cette logique. Par exemple, si $a, b, c \in \mathcal{V}$, $a \equiv v \vee \neg(b^+ \wedge c^-) \in \Delta\mathcal{LP}$.

Une formule de $(\Delta\mathcal{LP}, \models)$ est un élément de $\Delta\mathcal{LP}$. On définit donc formellement une formule de cette logique comme étant soit un atome, soit d'une des formes suivantes : $\neg\varphi$, $\varphi_1 \wedge \varphi_2$ et $\varphi_1 \vee \varphi_2$. Les connecteurs $\top, \bot, \rightarrow$ et $\leftrightarrow$ sont utilisés en tant qu'abréviations, comme en logique propositionnelle (par exemple, $\varphi_1 \rightarrow \varphi_2 = \neg\varphi_1 \vee \varphi_2$). La taille d'une formule $\varphi \in \Delta\mathcal{LP}$, notée $|\varphi|$, est le nombre d'occurrences de connecteurs de $\varphi$.
## 3.2 Sémantique

Une interprétation en logique propositionnelle représente un état du monde particulier. Dans la logique des variations, on considérera qu'une interprétation représente un changement d'un état du monde à un autre. Ainsi, on définit une interprétation pour la sémantique de cette logique par un couple d'interprétations pour la sémantique de $(\mathcal{LP}, \models)$. Formellement, soit $\Delta\Omega = \Omega \times \Omega$. On notera un élément $(\mathcal{I}, \mathcal{J}) \in \Delta\Omega$ par $\mathcal{IJ}$ (sans parenthèse ni virgule, pour simplifier).

Étant donné $\mathcal{IJ} \in \Delta\Omega$ et $\varphi \in \Delta\mathcal{LP}$, il reste à définir la relation $\mathcal{IJ} \models \varphi$ (« $\mathcal{IJ}$ satisfait $\varphi$»). On commence par le faire sur les atomes (pour $a \in \mathcal{V}$) :

- Avec symboles de variations primitifs :

$$- \mathcal{IJ} \models a^{\text{=f}} \text{ si } \mathcal{I} \not\models a \text{ et } \mathcal{J} \not\models a;$$

$$- \mathcal{IJ} \models a^{\text{=v}} \text{ si } \mathcal{I} \models a \text{ et } \mathcal{J} \models a;$$

$$- \mathcal{IJ} \models a^{\text{+}} \text{ si } \mathcal{I} \not\models a \text{ et } \mathcal{J} \models a;$$

$$- \mathcal{IJ} \models a^{-} \text{ si } \mathcal{I} \models a \text{ et } \mathcal{J} \not\models a;$$

- Avec symboles de variations non primitifs :

$$- \mathcal{IJ} \models a^{\text{=}} \text{ si } \mathcal{IJ} \models a^{\text{=f}} \text{ ou } \mathcal{IJ} \models a^{\text{=v}};$$

$$- \mathcal{IJ} \models a^{\neq} \text{ si } \mathcal{IJ} \models a^{\text{+}} \text{ ou } \mathcal{IJ} \models a^{-};$$

$$- \mathcal{IJ} \models a^{\text{f}\bullet} \text{ si } \mathcal{IJ} \models a^{\text{=f}} \text{ ou } \mathcal{IJ} \models a^{\text{+}};$$

$$- \mathcal{IJ} \models a^{\bullet\text{f}} \text{ si } \mathcal{IJ} \models a^{\text{=f}} \text{ ou } \mathcal{IJ} \models a^{-};$$

$$- \mathcal{IJ} \models a^{\text{v}\bullet} \text{ si } \mathcal{IJ} \models a^{\text{=v}} \text{ ou } \mathcal{IJ} \models a^{-};$$

$$- \mathcal{IJ} \models a^{\bullet\text{v}} \text{ si } \mathcal{IJ} \models a^{\text{=v}} \text{ ou } \mathcal{IJ} \models a^{\text{+}}.$$

La sémantique des connecteurs est définie de façon similaire à ce qu'elle était en logique propositionnelle (pour $\varphi, \varphi_1, \varphi_2 \in \Delta\mathcal{LP}$) :

$$- \mathcal{IJ} \models \neg\varphi \text{ si } \mathcal{IJ} \not\models \varphi;$$

$$- \mathcal{IJ} \models \varphi_1 \wedge \varphi_2 \text{ si } \mathcal{IJ} \models \varphi_1 \text{ et } \mathcal{IJ} \models \varphi_2;$$

$$- \mathcal{IJ} \models \varphi_1 \vee \varphi_2 \text{ si } \mathcal{IJ} \models \varphi_1 \text{ ou } \mathcal{IJ} \models \varphi_2.$$

Les notions introduites en logique propositionnelle relatives à la sémantique se transposent aisément : notion de modèle, $\mathcal{M}(\varphi) = \{\mathcal{IJ} \in \Delta\Omega \mid \mathcal{IJ} \models \varphi\}$, conséquence logique $\varphi_1 \models \varphi_2$, tautologie, satisfiability d'une formule, etc.

Une façon équivalente de considérer la sémantique de cette logique consiste à considérer chaque formule $\varphi \in \Delta\mathcal{LP}$ comme une représentation du sous-ensemble $\mathcal{M}(\varphi)$ de $\Delta\Omega = \Omega \times \Omega$, i.e. d'une relation binaire sur $\Omega$.

## 3.3 Propriétés

**Représentabilité d'un ensemble d'interprétations par une formule.** Certaines définitions de formules dans la suite du rapport seront données par leurs ensembles de modèles, donc à l'équivalence logique près. Ce genre de définition est acceptable car tout sous-ensemble de $\Delta\Omega$ est représentable dans $\Delta\mathcal{LP}$ :

$$\text{pour tout } A \subseteq \Delta\Omega, \text{ il existe } \varphi \in \Delta\mathcal{LP} \text{ telle que } \mathcal{M}(\varphi) = A \qquad (2)$$

**Preuve de (2).** Soit $\mathcal{IJ} \in \Delta\Omega$, et soit la formule

$$\psi_{\mathcal{IJ}} = \bigwedge \left\{ a^{\text{var}(\mathcal{I}(a), \mathcal{J}(a))} \mid a \in \mathcal{V} \right\} \\ \text{où } \text{var} : (\mathbf{f}, \mathbf{f}) \mapsto \text{=f} \quad (\mathbf{v}, \mathbf{v}) \mapsto \text{=v} \quad (\mathbf{f}, \mathbf{v}) \mapsto \text{+} \quad (\mathbf{v}, \mathbf{f}) \mapsto \text{-}$$

On démontre d'abord que, pour toute $a \in \mathcal{V}$, $\mathcal{IJ} \models a^{\text{var}(\mathcal{I}(a), \mathcal{J}(a))}$ (il suffit de considérer les quatre cas pour s'en convaincre). Inversement, si quelle que soit $a \in \mathcal{V}$, $\mathcal{I}_1\mathcal{J}_1 \models a^{\text{var}(\mathcal{I}(a), \mathcal{J}(a))}$ entraîne $\mathcal{I}_1(a) = \mathcal{I}(a)$ et $\mathcal{J}_1(a) = \mathcal{J}(a)$, alors $\mathcal{I}_1\mathcal{J}_1 = \mathcal{IJ}$. Par conséquent, $\mathcal{M}(\psi_{\mathcal{IJ}}) = \{\mathcal{IJ}\}$. Soit alors $\varphi = \bigvee\{\psi_{\mathcal{IJ}} \mid \mathcal{IJ} \in A\}$. On en déduit que $\mathcal{M}(\varphi) = A$. ■
**Équivalences et mise sous forme normale.** Les résultats suivants (et leurs preuves) se transposent aisément de résultats de la logique propositionnelle (les formules considérées ci-dessous sont toutes éléments de $\Delta\mathcal{L}\mathcal{P}$) :

— Théorème de la déduction et son corollaire :

$$ \varphi_1 \models \varphi_2 \quad \text{ssi} \quad \models \varphi_1 \rightarrow \varphi_2 $$

$$ \varphi_1 \equiv \varphi_2 \quad \text{ssi} \quad \models \varphi_1 \leftrightarrow \varphi_2 $$

— Lien entre tautologies et formules satisfiables :

$$ \models \varphi \quad \text{ssi} \quad \neg \varphi \text{ est insatisfiable} $$

— Lois de De Morgan.

— Involutivité de $\neg$, commutativité de $\wedge$ et $\vee$, associativité de $\wedge$ et $\vee$, distributivité de $\wedge$ sur $\vee$, distributivité de $\vee$ sur $\wedge$, etc. (toutes ces propriétés étant vérifiées modulo l'équivalence logique). Les résultats suivants découlent des définitions :

$$ \left. \begin{array}{lclcl} a^{=} & \equiv & a^{=f} & \lor & a^{=v} & a^{\neq} & \equiv & a^{+} & \lor & a^{-} & a^{f\bullet} & \equiv & a^{=f} & \lor & a^{+} \\ a^{\bullet f} & \equiv & a^{=f} & \lor & a^{-} & a^{v\bullet} & \equiv & a^{=v} & \lor & a^{-} & a^{\bullet v} & \equiv & a^{=v} & \lor & a^{+} \end{array} \right| \qquad (3) $$

On peut faire les transformations suivantes sur une formule de $(\Delta\mathcal{L}\mathcal{P}, \models)$, transformations qui conservent l'équivalence logique. Dans un premier temps, on peut supprimer tous les atomes $a^v$ où $v \in \mathcal{D}_1$ en utilisant les équivalences (3). Dans un deuxième temps, on peut utiliser une transformation mettant sous une forme normale négative (où $\neg$ n'apparaît que devant les atomes) comme on le fait en logique propositionnelle (en utilisant les lois de De Morgan et l'involutivité de $\neg$ modulo $\equiv$). Enfin, on peut appliquer l'équivalence suivante (de gauche à droite), pour $a \in \mathcal{V}$ et $v \in \mathcal{D}_0$ :

$$ \neg a^v \equiv \bigvee_{w \in \mathcal{D}_0 \setminus \{v\}} a^w \qquad (4) $$

De cette façon, on peut écrire toute formule de $(\Delta\mathcal{L}\mathcal{P}, \models)$ comme une formule n'utilisant pas le connecteur $\neg$ ni les symboles de variation non primitifs. L'idée d'une telle transformation est qu'elle pourrait servir de prétraitement dans une procédure de test de satisfiabilité s'appuyant sur la méthode des tableaux sémantiques [15], pour laquelle un conflit serait n'importe quelle paire d'atomes $\{a^v, a^w\}$ où $a \in \mathcal{V}$, $v, w \in \mathcal{D}_0$ et $v \neq w$. Cette idée sera évoquée à nouveau à la section 5.3.

**Preuve de (4).** Soit $\text{var}^{-1}$ la fonction inverse de la fonction var introduite dans la preuve de (2). Pour $\mathcal{I}\mathcal{J} \in \Delta\Omega$ on a les équivalences

$$ \begin{array}{l} \mathcal{I}\mathcal{J} \models \neg a^v \text{ssi } \mathcal{I}\mathcal{J} \not\models a^v \\ \quad \text{ssi } (\mathcal{I}(a), \mathcal{J}(a)) \neq \text{var}^{-1}(v) \\ \quad \text{ssi } (\mathcal{I}(a), \mathcal{J}(a)) \in \{\mathbf{f}, \mathbf{v}\}^2 \setminus \{\text{var}^{-1}(v)\} \\ \text{ssi } \mathcal{I}\mathcal{J} \models a^w \text{ pour un } w \in \mathcal{D}_0 \setminus \{v\} \\ \quad \text{ssi } \mathcal{I}\mathcal{J} \models \bigvee_{w \in \mathcal{D}_0 \setminus \{v\}} a^w \end{array} $$

Ce qui permet de conclure.

<figure><img src="image_2.png" /></figure>

On peut noter que le choix, parmi les symboles de variations, de $\{=\mathbf{f}, =\mathbf{v}, +, -\}$ comme ensemble de variations primitives pourrait être changé : il existe d'autres sous-ensembles de $\mathcal{D}$ permettant de générer $\mathcal{D}$ par des connecteurs logiques. Par exemple, c'est le cas de $\{\mathbf{f}\bullet, \bullet\mathbf{f}, \mathbf{v}\bullet, \bullet\mathbf{v}\}$ puisqu'on a les équivalences suivantes :

$$ a^{=f} \equiv a^{f\bullet} \wedge a^{\bullet f} \qquad a^{=v} \equiv a^{v\bullet} \wedge a^{\bullet v} $$

$$ a^{+} \equiv a^{f\bullet} \wedge a^{\bullet v} \qquad a^{-} \equiv a^{v\bullet} \wedge a^{\bullet f} $$
**Satisfiabilité et plongement.** Soit $SAT_Δ$ le problème de décision qui, étant donné une formule $\varphi$ de $(\Delta LP, \models)$ détermine si $\varphi$ est satisfiable. Le problème $SAT_Δ$ est NP-complet. On peut prouver cela en montrant que $SAT_Δ$ est dans NP puis en montrant que $SAT_Δ$ est NP-difficile.

On peut prouver que $SAT_Δ$ est dans NP en exhibant un algorithme polynomial non déterministe répondant à ce problème : il suffit de construire un algorithme avec un oracle qui choisit une interprétation $\mathcal{I}\mathcal{J}$ qui satisfait $\varphi$ si $\varphi$ est satisfiable, et de tester que c'est effectivement le cas.

On peut prouver que $SAT_Δ$ est NP-difficile en montrant que le problème SAT peut être réduit en temps polynomial à $SAT_Δ$. Étant donné $\alpha \in LP$, soit $\hat{\alpha} \in \Delta LP$ défini en remplaçant toutes les occurrences de variables propositionnelles $a$ dans $\alpha$ par $a^{=v}$. On appelle $\hat{\alpha}$ le plongement de $\alpha$. Par exemple, si $\alpha = a \wedge \neg(b \vee c)$ alors, $\hat{\alpha} = a^{=v} \wedge \neg(b^{=v} \vee c^{=v})$. On peut montrer le résultat suivant, pour $\mathcal{I} \in \Omega$ et $\alpha \in LP$ :

$$ \mathcal{I} \models \alpha \quad \text{ssi} \quad \mathcal{II} \models \hat{\alpha} \qquad (5) $$

**Preuve de (5).** Ce résultat se montre ainsi, par récurrence sur $|\alpha|$. Dans le cas de base $|\alpha| = 0$, $\alpha = a$ pour un $a \in V$ et, par définition de la sémantique de $=v$, on a bien l'équivalence $\mathcal{I} \models a \quad \text{ssi} \quad \mathcal{II} \models a^{=v}$. Supposons à présent qu'on ait bien (5) pour toute formule $\alpha$ telle que $|\alpha| \le k$ (pour un entier naturel $k$). Soit $\alpha \in LP$ telle que $|\alpha| = k + 1$. Trois cas sont à considérer :

**cas 1** Si $\alpha = \beta_1 \wedge \beta_2$ avec $\beta_1$ et $\beta_2$ deux formules de tailles inférieures ou égales à $k$, sur lesquelles l'hypothèse de récurrence s'applique donc. On a alors les équivalences suivantes :

$$ \begin{align*} \mathcal{I} \models \alpha & \text{ssi } \mathcal{I} \models \beta_1 \text{ et } \mathcal{I} \models \beta_2 \\ \text{ssi } \mathcal{II} \models \beta_1 & \text{ et } \mathcal{II} \models \beta_2 & \text{(par hypothèse de récurrence)} \\ \text{ssi } \mathcal{II} \models \beta_1 & \wedge \beta_2 = \beta_1 \wedge \beta_2 = \hat{\alpha} \end{align*} $$

**cas 2** Si $\alpha = \beta_1 \vee \beta_2$ avec $\beta_1, \beta_2 \in LP$. On a alors :

$$ \begin{align*} \mathcal{I} \models \alpha & \text{ssi } \mathcal{I} \models \beta_1 \text{ ou } \mathcal{I} \models \beta_2 \\ \text{ssi } \mathcal{II} \models \beta_1 & \text{ ou } \mathcal{II} \models \beta_2 & \text{(par hypothèse de récurrence)} \\ \text{ssi } \mathcal{II} \models \beta_1 & \vee \beta_2 = \beta_1 \vee \beta_2 = \hat{\alpha} \end{align*} $$

**cas 3** Si $\alpha = \neg\beta$ où $\beta \in LP$. On a alors :

$$ \begin{align*} \mathcal{I} \models \alpha & \text{ssi } \mathcal{I} \models \beta \\ \text{ssi } \mathcal{II} \models \beta & \text{(par hypothèse de récurrence)} \\ \text{ssi } \mathcal{II} \models \neg\beta & = \neg\beta = \hat{\alpha} \end{align*} $$

Dans les trois cas, on a bien l'équivalence (5) pour $\alpha$. Selon le principe de la preuve par récurrence, cette équivalence est bien démontrée. ■

On peut ensuite montrer l'équivalence (pour $\alpha \in LP$) suivante :

$$ \alpha \text{ est satisfiable} \quad \text{ssi} \quad \hat{\alpha} \text{ est satisfiable} \qquad (6) $$

Par conséquent, si on dispose d'un algorithme pour $SAT_Δ$, en utilisant cette équivalence, on peut construire un algorithme pour SAT avec un pont polynomial (le calcul $\alpha \mapsto \hat{\alpha}$ étant linéaire en la taille de la formule). Donc, $SAT_Δ$ est NP-difficile : le problème NP-complet SAT peut être réduit en temps polynomial à $SAT_Δ$.

**Preuve de (6).** L'implication de gauche à droite est une conséquence directe de (5).

La réciproque peut se montrer par la contraposée : on suppose que $\alpha$ est insatisfiable et on va en déduire que $\hat{\alpha}$ est insatisfiable. On peut mettre $\alpha$ sous FND (forme normale disjonctive 4) en appliquant un

<footnote n="4">4. Pour rappel, une formule sous FND est une disjonction de conjonctions de littéraux où un littéral est une formule d'une des formes $a$ (littéral positif) et $\neg a$ (littéral négatif) avec $a \in V$.</footnote>
processus systématique (utilisant l'involutivité de $\neg$, la distributivité de $\vee$ sur $\wedge$, etc.) pour aboutir à une formule $\alpha_{\text{FND}}$. En utilisant ce même processus sur $\hat{\alpha}$ on aboutit à une formule $(\hat{\alpha})_{\text{FND}} = \hat{\alpha}_{\text{FND}}$. La mise sous FND préserve l'équivalence dans les deux logiques, donc $\alpha_{\text{FND}} \equiv \alpha$ et $\hat{\alpha}_{\text{FND}} \equiv \hat{\alpha}$. Or $\alpha$ est insatisfiable, donc $\alpha_{\text{FND}}$ l'est également ce qui signifie que chaque terme de la disjonction $\alpha_{\text{FND}}$ est une conjonction insatisfiable de littéraux. Dans une telle conjonction, on a nécessairement une variable $a$ apparaissant dans un littéral positif et dans un littéral négatif (sinon, la conjonction de littéraux serait satisfiable). Par conséquent, $\hat{\alpha}_{\text{FND}}$ est une disjonction de conjonctions de littéraux, chacune de ces conjonctions contenant un terme $a^{\neg v}$ et un terme $\neg a^{\neg v}$. Or, $a^{\neg v} \wedge \neg a^{\neg v}$ est insatisfiable dans $(\Delta\mathcal{L}\mathcal{P}, \models)$. Donc, chaque conjonction constituant $\hat{\alpha}_{\text{FND}}$ est insatisfiable et donc $\alpha_{\text{FND}}$ est également insatisfiable. Comme $\hat{\alpha}_{\text{FND}} \equiv \hat{\alpha}$, on en conclut que $\hat{\alpha}$ est insatisfiable et c'est ce qu'il fallait démontrer.

Un corollaire de (6) est le suivant, pour $\mathcal{B}$, un ensemble fini de formules propositionnelles et $\alpha \in \mathcal{LP}$:

$$ \mathcal{B} \models \alpha \quad \text{ssi} \quad \hat{\mathcal{B}} \models \hat{\alpha} \qquad (7) $$

où $\hat{\mathcal{B}} = \{\hat{\beta} \mid \beta \in \mathcal{B}\}$. Cela permet de justifier $a$ *posteriori* le terme de plongement : on peut considérer que l'injection $\alpha \mapsto \hat{\alpha}$ permet de représenter (dans un sens cohérent avec la relation de conséquence logique) la logique $(\mathcal{LP}, \models)$ au sein de la logique $(\Delta\mathcal{L}\mathcal{P}, \models)$. On pourrait aussi se servir de ce plongement en étendant la syntaxe de $(\Delta\mathcal{L}\mathcal{P}, \models)$ par celle de $(\mathcal{LP}, \models)$, considérant, par exemple, que $a \wedge b^+$ est une notation pour $a^{\neg v} \wedge b^+$. Nous éviterons néanmoins de le faire dans ce rapport.

**Preuve de (7).** Soit $\gamma = \neg (\bigwedge \mathcal{B} \wedge \neg \alpha)$ : les assertions « $\mathcal{B} \models \alpha$» et « $\gamma$ est satisfiable » sont équivalentes entre elles, de même que les assertions « $\hat{\mathcal{B}} \models \hat{\alpha}$» et « $\hat{\gamma}$ est satisfiable ». En appliquant l'équivalence (6) sur $\gamma$ cela permet de conclure.

■

# 4 Variation d'une formule propositionnelle à une autre

Soit $\alpha, \beta \in \mathcal{LP}$, on cherche à exprimer la variation de $\alpha$ à $\beta$, qu'on notera $\alpha \triangleright \beta$ et qui sera une formule de $(\Delta\mathcal{L}\mathcal{P}, \models)$. Plusieurs définitions non équivalentes de l'opérateur $\triangleright$ peuvent $a$ *priori* être envisagées. Dans cette section, celle qui nous semble la plus simple est étudiée : elle est définie à la section 4.1. Elle permet aussi d'introduire une extension de la syntaxe de $(\Delta\mathcal{L}\mathcal{P}, \models)$ ne modifiant pas sa sémantique (section 4.2). Une étude des propriétés de cet opérateur de variation est présentée à la section 4.3. Enfin, d'autres définitions de la variation entre formules propositionnelles sont présentées brièvement, leur étude détaillée étant une perspective (section 4.4).

## 4.1 Définition d'un opérateur de variation

L'opérateur $\triangleright$ qu'on cherche à définir doit $a$ *minima* correspondre à l'exemple donné en introduction : on s'attend à ce que $x^i \triangleright x^j \equiv \Delta x^{ij}$. La définition proposée ci-dessous vérifie cela et est donnée à l'équivalence logique près, par l'ensemble de ses modèles :

$$ \mathcal{M}(\alpha \triangleright \beta) = \mathcal{M}(\alpha) \times \mathcal{M}(\beta) \qquad (8) $$

En d'autres termes, on considère les variations entre tout modèle de $\alpha$ et tout modèle de $\beta$.

## 4.2 Une extension de la syntaxe de la logique des variations propositionnelles

Les atomes $a^v$ où $a \in \mathcal{V}$ et $v \in \mathcal{D}_0$ peuvent s'exprimer à l'aide de l'opérateur $\triangleright$ défini ci-dessus :

$$ a^{\neg f} \equiv \neg a \triangleright \neg a $$

$$ a^{\neg v} \equiv a \triangleright a $$

$$ a^+ \equiv \neg a \triangleright a $$

$$ a^- \equiv a \triangleright \neg a $$

On peut généraliser cela en introduisant la notation $\alpha^v$ pour toute formule propositionnelle $\alpha$ et tout $v \in \mathcal{D}_0$ :

$$ \alpha^{\neg f} \equiv \neg \alpha \triangleright \neg \alpha $$

$$ \alpha^{\neg v} \equiv \alpha \triangleright \alpha $$

$$ \alpha^+ \equiv \neg \alpha \triangleright \alpha $$

$$ \alpha^- \equiv \alpha \triangleright \neg \alpha $$
Et on peut étendre cela aux symboles de variation non primitifs :

$$
\begin{align*}
\alpha^{=} &= \alpha^{=}^{f} \lor \alpha^{=}^{v} \\
\alpha^{\neq} &= \alpha^{+} \lor \alpha^{-} \\
\alpha^{f\bullet} &= \alpha^{=}^{f} \lor \alpha^{+} \equiv \neg\alpha \triangleright \top \\
\alpha^{\bullet f} &= \alpha^{=}^{f} \lor \alpha^{-} \equiv \top \triangleright \neg\alpha \\
\alpha^{v\bullet} &= \alpha^{=}^{v} \lor \alpha^{-} \equiv \alpha \triangleright \top \\
\alpha^{\bullet v} &= \alpha^{=}^{v} \lor \alpha^{+} \equiv \top \triangleright \alpha
\end{align*}
$$

Cette extension de la syntaxe ne change pas la sémantique : comme on peut exprimer $\alpha \triangleright \beta$ dans la syntaxe de la logique avant extension, on peut également considérer les $\alpha^v$ (pour $\alpha$ une formule propositionnelle qui n'est pas une variable) comme une abréviation pratique (qui pourrait aussi avoir un intérêt en terme de temps de calculs).

Cette syntaxe étendue se justifie par le fait que la définition de la satisfaction d'un atome $a^v$ par une interprétation $\mathcal{IJ}$ (cf. section 3.2) s'étend aux formules $\alpha^v$, pour tout $\alpha \in \mathcal{LP}$. Ainsi, $\mathcal{IJ} \models \alpha^{=}^f$ ssi $\mathcal{I} \not\models \alpha$ et $\mathcal{J} \not\models \alpha$; $\mathcal{IJ} \models \alpha^+^s$ ssi $\mathcal{I} \not\models \alpha$ et $\mathcal{J} \models \alpha$, etc.

Les $\alpha^v$, pour $\alpha \in \mathcal{LP}$ et $v \in \mathcal{D}_0$ sont deux à deux incohérents et leur disjonction est une tautologie :

$$
\text{si } w, x \in \mathcal{D}_0 \text{ et } w \neq x, \alpha^w \wedge \alpha^x \models \perp \quad (9)
$$

$$
\models \alpha^{=}^{f} \lor \alpha^{=}^{v} \lor \alpha^{+} \lor \alpha^{-} \qquad (10)
$$

Donc, si $\alpha \in \mathcal{LP}$ est satisfiable et n'est pas une tautologie alors $\{M(\alpha^{=}^{f}), M(\alpha^{=}^{v}), M(\alpha^{+}), M(\alpha^{-})\}$ est une partition de $\Delta\Omega^5$.

Dans la suite du rapport, on considérera qu'une formule $\varphi \in \Delta\mathcal{LP}$ est n'importe quelle expression respectant cette syntaxe étendue.

On définit la substitution d'une variable $a$ par une formule propositionnelle $\alpha$ dans une formule
$\varphi \in \Delta\mathcal{LP}$ (notation : $\varphi[a\backslash\alpha]$) de façon classique : $a^v[a\backslash\alpha] = \alpha^v$, $x^v[a\backslash\alpha] = x^v$ pour $x \in \mathcal{V} \setminus \{a\}$, $\neg\psi[a\backslash\alpha] = \neg(\psi[a\backslash\alpha])$, $(\varphi_1 \wedge \varphi_2)[a\backslash\alpha] = (\varphi_1[a\backslash\alpha]) \wedge (\varphi_2[a\backslash\alpha])$ et $(\varphi_1 \vee \varphi_2)[a\backslash\alpha] = (\varphi_1[a\backslash\alpha]) \vee (\varphi_2[a\backslash\alpha])$. La substitution d'une variable par une formule propositionnelle dans une tautologie de $(\Delta\mathcal{LP}, \models)$ est une tautologie. Formellement, avec $a \in \mathcal{V}$, $\alpha \in \mathcal{LP}$ et $\varphi \in \Delta\mathcal{LP}$ :

$$
\text{si } \models \varphi \text{ alors } \models \varphi[a\setminus\alpha] \qquad (11)
$$

La preuve de cette implication s'appuie sur le lemme ci-dessous (qui est prouvé plus bas) :

Soit $\psi \in \Delta\mathcal{LP}$, une disjonction d'atomes $a^v$ où $v \in \mathcal{D}_0$. On a l'équivalence :
$$ \models \psi \quad \text{ssi} \quad \text{il existe } b \in \mathcal{V} \text{ telle que pour tout } v \in \mathcal{D}_0, b^v \text{ est un terme de la disjonction } \psi. \quad (12) $$

Preuve de (11). Supposons que $\models \varphi$. Soit $\varphi_{\text{FNC}}$, une formule équivalente à $\varphi$ de la forme suivante :
$\varphi_{\text{FNC}} = \bigwedge \{\varphi_k \mid k \in \{1, 2, \dots, p\}\}$ où chaque $\varphi_k$ est une disjonction d'atomes $a^v$ où $v \in \mathcal{D}_0$: pour
obtenir $\varphi_{\text{FNC}}$, on effectue une série de transformations partant de $\varphi$, d'abord en revenant à la syntaxe de
départ (dans laquelle on n'a une occurrence de $\alpha^v$ que si $\alpha \in \mathcal{V}$), puis on se débarrasse des symboles
de variations non primitifs, puis, on utilise les mêmes opérations que pour la mise sous forme normale
conjonctive en logique propositionnelle et enfin, on applique de gauche à droite l'équivalence (4) autant
de fois que nécessaire.

Comme $\varphi_{\text{FNC}} \equiv \varphi$ et que $\varphi$ est une tautologie, chacun des $\varphi_k$ est une tautologie. D'après le lemme (12),
pour un $\varphi_k$ donné, il existe une variable $b$ telle que $\varphi_k$ contient les quatre atomes $b^v$ pour tout $v \in \mathcal{D}_0$.
Deux cas sont à considérer :

<footnote n="5">5. La condition $\alpha$ est satisfiable et n'est pas une tautologie n'est là que parce que l'ensemble vide ne peut pas être élément d'une partition : si $\alpha \models \perp$ (resp. $\models \alpha$) alors $M(\alpha^{=}^{v}) = M(\alpha^{+}) = M(\alpha^{-}) = \emptyset$ (resp. $M(\alpha^{=}^{f}) = M(\alpha^{+}) = M(\alpha^{-}) = \emptyset$).</footnote>
**cas 1** Si $b = a$, la substitution $\varphi_k[a\alpha]$ est donc une disjonction contenant quatre termes deux à deux différents $\alpha^v$ ($v \in D_0$) et on peut en déduire que $\varphi_k[a\alpha]$ est une tautologie.

**cas 2** Si $b \neq a$ alors $\varphi_k[a\alpha]$ contient les quatre atomes $b^v$ ($v \in D_0$) et est donc une tautologie.

Dans tous les cas, les $\varphi_k[a\alpha]$ sont toutes des tautologies et donc $\varphi_{\text{FNC}}[a\alpha]$ est une tautologie.

Or, $\varphi_{\text{FNC}}[a\alpha] \equiv \varphi[a\alpha]$ (on peut le démontrer en appliquant sur $\varphi[a\alpha]$ la séquence d'opérations qui a permis de passer de $\varphi$ à $\varphi_{\text{FNC}}$). Donc $\varphi[a\alpha]$ est une tautologie, ce qui conclut la preuve. ■

**Preuve de (12).** On fait cette preuve par l'absurde : supposons que $\models \psi$ et que pour toute $b \in \mathcal{V}$, il existe $v_b \in D_0$ telle que $b^{v_b}$ n'est pas dans la disjonction $\psi$ (il y a potentiellement plusieurs valeurs $v_b$, on en choisit une selon un choix arbitraire). Soit alors $\mathcal{IJ} \in \Delta\Omega$ définie comme suit, pour $b \in \mathcal{V}$ :

$$ \mathcal{I}(b) = \left\{ \begin{array}{ll} \mathbf{v} & \text{si } v_b \in \{\mathbf{v}, -\} \\ \mathbf{f} & \text{sinon} \end{array} \right. \qquad \mathcal{J}(b) = \left\{ \begin{array}{ll} \mathbf{v} & \text{si } v_b \in \{\mathbf{v}, +\} \\ \mathbf{f} & \text{sinon} \end{array} \right. $$

Donc, pour tout $b \in \mathcal{V}$, $\mathcal{IJ} \models b^{v_b}$ et donc, $\mathcal{IJ} \not\models b^v$ pour $v \in D_0 \setminus \{v_b\}$. Soit alors $\chi = \bigvee_{b \in \mathcal{V}} \bigvee_{v \in D_0 \setminus \{v_b\}} b^v$. On a donc $\mathcal{IJ} \not\models \chi$. Par hypothèse, l'ensemble des termes de $\psi$ est un sous-ensemble de l'ensemble des termes de la disjonction $\chi$, d'où $\psi \models \chi$. Par conséquent, $\mathcal{IJ} \not\models \psi$ et cela contredit l'hypothèse $\models \psi$, ce qui permet de conclure cette preuve par l'absurde. ■

## 4.3 Étude de l'opérateur ▷

On notera $\mathcal{LP}^{\text{sat}}$ (resp. $\Delta\mathcal{LP}^{\text{sat}}$) l'ensemble des formules $\alpha \in \mathcal{LP}$ (resp. $\varphi \in \Delta\mathcal{LP}$) qui sont satisfiables.

**Articulation de ▷ avec les connecteurs.** L'opération ▷ est « distributive » sur $\land$ et sur $\lor$ modulo l'équivalence $^6$. Formellement, pour $\alpha, \alpha_1, \alpha_2, \beta, \beta_1, \beta_2 \in \mathcal{LP}$ :

$$ \begin{align*} \alpha \triangleright (\beta_1 \land \beta_2) &\equiv (\alpha \triangleright \beta_1) \land (\alpha \triangleright \beta_2) \\ \alpha \triangleright (\beta_1 \lor \beta_2) &\equiv (\alpha \triangleright \beta_1) \lor (\alpha \triangleright \beta_2) \\ (\alpha_1 \land \alpha_2) \triangleright \beta &\equiv (\alpha_1 \triangleright \beta) \land (\alpha_2 \triangleright \beta) \\ (\alpha_1 \lor \alpha_2) \triangleright \beta &\equiv (\alpha_1 \triangleright \beta) \lor (\alpha_2 \triangleright \beta) \end{align*} $$

Par ailleurs, pour $\alpha, \beta \in \mathcal{LP}$, on a :

$$ \begin{align} \alpha \triangleright \beta &\equiv (\alpha \triangleright \top) \land (\top \triangleright \beta) \tag{13} \\ \neg(\alpha \triangleright \beta) &\equiv (\neg\alpha \triangleright \beta) \lor (\alpha \triangleright \neg\beta) \lor (\neg\alpha \triangleright \neg\beta) \equiv \alpha^{\bullet\text{f}} \lor \beta^{\bullet\text{f}} \nonumber \end{align} $$

Le résultat suivant permet de calculer $\Delta x^{ij}$ en fonction de $x^i$ et $x^j$ (cf. introduction). Soit $\alpha, \beta \in \mathcal{LP}$ équivalents à une conjonction de littéraux. Alors, $\alpha \triangleright \beta$ est une conjonction d'atomes de $(\Delta\mathcal{LP}, \models)$. Plus précisément :

$$ \begin{align} \text{si } \alpha &\equiv \bigwedge_{a \in \mathcal{V}} \ell(a) \text{ et } \beta \equiv \bigwedge_{a \in \mathcal{V}} m(a) \text{ avec } \ell(a), m(a) \in \{a, \neg a, \top\} \notag \\ \text{alors } \alpha \triangleright \beta &\equiv \bigwedge_{a \in \mathcal{V}} \ell(a) \triangleright m(a) \tag{14} \end{align} $$

et $\ell(a) \triangleright m(a)$ est équivalent à un atome ou à $\top$, selon le tableau suivant :

<footnote n="6">6. Les guillemets sont justifiés d'une part par le fait que la distributivité est définie d'habitude sur des opérations internes (alors que ▷ est externe), d'autre part, par le fait que $\land$ et $\lor$ sont des connecteurs (pas des opérations).</footnote>
<table><thead><tr><th></th><th>m(a) = a</th><th>m(a) = ¬a</th><th>m(a) = T</th></tr></thead><tbody><tr><th>ℓ(a) = a</th><td>a<sup>=v</sup></td><td>a<sup>=</sup></td><td>a<sup>v•</sup></td></tr><tr><th>ℓ(a) = ¬a</th><td>a<sup>+</sup></td><td>a<sup>=f</sup></td><td>a<sup>f•</sup></td></tr><tr><th>ℓ(a) = T</th><td>a<sup>•v</sup></td><td>a<sup>•f</sup></td><td>T</td></tr></tbody></table>

**Preuve de (14).** La preuve se fait en appliquant (13) de gauche à droite sur $\alpha \triangleright \beta$, en utilisant la distributivité à gauche et à droite de $\triangleright$ sur $\land$, pour obtenir la conjonction sur $a \in \mathcal{V}$ de $(\ell(a) \triangleright T) \land (T \triangleright m(a))$. En appliquant (13) de droite à gauche, on obtient le résultat désiré.

De façon plus détaillée, on a :

$$ \alpha \triangleright \beta \equiv (\alpha \triangleright T) \land (T \triangleright \beta) \qquad (\text{d'après (13)}) $$

$$ \equiv \left( \left( \bigwedge_{a \in \mathcal{V}} \ell(a) \right) \triangleright T \right) \land \left( T \triangleright \left( \bigwedge_{a \in \mathcal{V}} m(a) \right) \right) $$

$$ \equiv \left( \bigwedge_{a \in \mathcal{V}} \ell(a) \triangleright T \right) \land \left( \bigwedge_{a \in \mathcal{V}} T \triangleright m(a) \right) $$

$$ \equiv \bigwedge_{a \in \mathcal{V}} (\ell(a) \triangleright T) \land (T \triangleright m(a)) $$

$$ \equiv \bigwedge_{a \in \mathcal{V}} \ell(a) \triangleright m(a) \qquad (\text{d'après (13)}) $$

■

**Étude fonctionnelle de $\triangleright$.** L'opérateur $\triangleright$ n'est pas injectif, en particulier parce que si $\alpha$ est insatisfiable ou $\beta$ est insatisfiable, alors $\alpha \triangleright \beta \equiv \perp$. En revanche, la restriction de $\triangleright$ à $\mathcal{L}P^{\text{sat}} \times \mathcal{L}P^{\text{sat}}$ est injective :

$$ \begin{array}{l} \textbf{si } \alpha_1, \beta_1, \alpha_2, \beta_2 \in \mathcal{L}P^{\text{sat}} \text{ et } \alpha_1 \triangleright \beta_1 \equiv \alpha_2 \triangleright \beta_2 \\ \textbf{alors } \alpha_1 \equiv \alpha_2 \text{ et } \beta_1 \equiv \beta_2 \end{array} \qquad (15) $$

L'opérateur $\triangleright$ n'est pas non plus surjectif, mais son ensemble image est intéressant à étudier. Soit les opérations $\mathbf{G}: \Delta\mathcal{L}\mathbf{P} \to \mathcal{L}\mathbf{P}$ et $\mathbf{D}: \Delta\mathcal{L}\mathbf{P} \to \mathcal{L}\mathbf{P}$ définies, à la syntaxe près, pour $\varphi \in \Delta\mathcal{L}\mathbf{P}$, par :

$$ \mathcal{M}(\mathbf{G}(\varphi)) = \{\mathcal{I} \in \Omega \mid \text{il existe } \mathcal{J} \in \Omega \text{ telle que } \mathcal{I}\mathcal{J} \models \varphi\} $$

$$ \mathcal{M}(\mathbf{D}(\varphi)) = \{\mathcal{J} \in \Omega \mid \text{il existe } \mathcal{I} \in \Omega \text{ telle que } \mathcal{I}\mathcal{J} \models \varphi\} $$

$\mathbf{G}(\varphi)$ (resp. $\mathbf{D}(\varphi)$) peut être compris comme une « projection » à gauche (resp. à droite) de $\varphi$. Soit alors

$$ \mathbf{F}(\varphi) = \mathbf{G}(\varphi) \triangleright \mathbf{D}(\varphi) $$

$\mathbf{F}$ est un opérateur de fermeture sur $(\Delta\mathcal{L}\mathbf{P}, \models)$ (modulo $\equiv$) :

$$ \varphi \models \mathbf{F}(\varphi) $$

$$ \mathbf{F}(\mathbf{F}(\varphi)) \equiv \mathbf{F}(\varphi) $$

$$ \text{si } \varphi_1 \models \varphi_2 \text{ alors } \mathbf{F}(\varphi_1) \models \mathbf{F}(\varphi_2) $$

pour $\varphi, \varphi_1, \varphi_2 \in \Delta\mathcal{L}\mathbf{P}$. Si $\varphi \equiv \mathbf{F}(\varphi)$, on dira que $\varphi$ est fermée pour $\mathbf{F}$. L'image de $\mathcal{L}\mathbf{P}^2$ par $\triangleright$ est l'ensemble des formules de $\Delta\mathcal{L}\mathbf{P}$ fermées pour $\mathbf{F}$.

Cette notion de fermeture est proche de celle qu'on trouve en analyse formelle de concepts (AFC [8]) et l'AFC pourrait être utilisée pour une représentation compacte de formules de $(\Delta\mathcal{L}\mathbf{P}, \models)$ de la façon suivante. Soit $\varphi \in \Delta\mathcal{L}\mathbf{P}$. Comme $\triangleright$ n'est pas surjective, $\varphi$ ne peut pas nécessairement s'écrire sous la forme $\alpha \triangleright \beta$, mais on va l'écrire sous la forme d'une disjonction de telles formules, il restera alors à
écrire chaque $\alpha$ et chaque $\beta$ de façon compacte (ce qui est un problème de logique propositionnelle). Pour ce faire, on considère un tableau dont les lignes sont indexées par les $\mathcal{I} \in \mathcal{G}(\varphi)$ et les colonnes, par les $\mathcal{J} \in \mathcal{D}(\varphi)$ et tel qu'il y ait une incidence sur la case de ligne $\mathcal{I}$ et de colonne $\mathcal{J}$ ssi $\mathcal{I}\mathcal{J} \models \varphi$. En appliquant un algorithme d'AFC, on cherche l'ensemble $\{(A_k, B_k)\}_{k \in \{1,2,...,p\}}$ des rectangles maximaux de ce tableau <fnref n="7" />. De cette façon, pour tout $k \in \{1, 2, ..., p\}$, en introduisant $\alpha_k, \beta_k \in \mathcal{L}\mathcal{P}^{\text{sat}}$ tels que $\mathcal{M}(\alpha_k) = A_k$ et $\mathcal{M}(\beta_k) = B_k$, on peut montrer que $\varphi \equiv \bigvee_{k \in \{1,2,...,p\}} \alpha_k \triangleright \beta_k$.

**Inversion des variations.** Pour $\varphi \in \Delta\mathcal{L}\mathcal{P}$, on définit $\text{inv}(\varphi) \in \Delta\mathcal{L}\mathcal{P}$ obtenue en remplaçant chaque occurrence dans $\varphi$ d'un $v \in \mathcal{D}$ par $\text{inv}(v)$ de la façon suivante :

$$
\begin{align*}
\text{inv}(v) &= v && \text{pour } v \in \{=\text{f}, =\text{v}, =, \neq\} \\
\text{inv}(\text{+}) &= - && \text{inv}(-) &= \text{+} \\
\text{inv}(\text{f}\bullet) &= \bullet\text{f} && \text{inv}(\bullet\text{f}) &= \text{f}\bullet \\
\text{inv}(\text{v}\bullet) &= \bullet\text{v} && \text{inv}(\bullet\text{v}) &= \text{v}\bullet
\end{align*}
$$

On peut montrer alors qu'on a, pour $\alpha, \beta \in \mathcal{L}\mathcal{P}$ :

$$
\beta \triangleright \alpha \equiv \operatorname{inv}(\alpha \triangleright \beta) \qquad (16)
$$

**Preuve de (16).** On prouve d'abord par récurrence sur $|\varphi|$ le résultat suivant :

$$
\mathcal{M}(\operatorname{inv}(\varphi)) = \{\mathcal{J}\mathcal{I} \mid \mathcal{I}\mathcal{J} \in \mathcal{M}(\varphi)\} \quad (17)
$$

Dans le cas de base, $|\varphi| = 0$, $\varphi$ est un atome $a^v$. On considère à titre d'exemple uniquement le cas où $v = +$, les $|\mathcal{D}| - 1 = 9$ autres cas se prouvent de façon similaire. Pour $\mathcal{I}\mathcal{J} \in \Delta\Omega$ :

$$
\mathcal{I}\mathcal{J} \models a^{+} \quad \text{ssi} \quad \mathcal{I} \not\models a \text{ et } \mathcal{J} \models a \quad \text{ssi} \quad \mathcal{J} \models a \text{ et } \mathcal{I} \not\models a \quad \text{ssi} \quad \mathcal{J}\mathcal{I} \models a^{-} \quad \text{ssi} \quad \mathcal{J}\mathcal{I} \models \text{inv}(a^{+})
$$

Supposons que (17) soit réalisé pour toute formule de taille inférieure ou égale à $k$. Soit $\varphi \in \Delta\mathcal{L}\mathcal{P}$ telle que $|\varphi| = k + 1$. Trois cas sont à considérer :

**cas 1** Si $\varphi = \neg\psi$ où $\psi \in \Delta\mathcal{L}\mathcal{P}$ est de taille $k$, on a :

$$
\begin{align*}
\mathcal{I}\mathcal{J} \models \varphi \quad \text{ssi} \quad \mathcal{I}\mathcal{J} \not\models \psi \quad \text{ssi} \quad \mathcal{J}\mathcal{I} \not\models \text{inv}(\psi) \quad \text{(par hypothèse de récurrence)} \\
\text{ssi} \quad \mathcal{J}\mathcal{I} \models \neg(\text{inv}(\psi)) = \text{inv}(\neg\psi) = \text{inv}(\varphi)
\end{align*}
$$

**cas 2** Si $\varphi = \psi_1 \wedge \psi_2$ où $\psi_1, \psi_2 \in \Delta\mathcal{L}\mathcal{P}$ sont de tailles inférieures ou égales à $k$, on a :

$$
\begin{align*}
\mathcal{I}\mathcal{J} \models \varphi \quad \text{ssi} \quad \mathcal{I}\mathcal{J} \models \psi_1 \text{ et } \mathcal{I}\mathcal{J} \models \psi_2 \\
\text{ssi} \quad \mathcal{J}\mathcal{I} \models \text{inv}(\psi_1) \text{ et } \mathcal{J}\mathcal{I} \models \text{inv}(\psi_2) \quad \text{(par hypothèse de récurrence)} \\
\text{ssi} \quad \mathcal{J}\mathcal{I} \models \text{inv}(\psi_1) \wedge \text{inv}(\psi_2) = \text{inv}(\psi_1 \wedge \psi_2) = \text{inv}(\varphi)
\end{align*}
$$

**cas 3** Si $\varphi = \psi_1 \lor \psi_2$ où $\psi_1, \psi_2 \in \Delta\mathcal{L}\mathcal{P}$ sont de tailles inférieures ou égales à $k$, on a :

$$
\begin{align*}
\mathcal{I}\mathcal{J} \models \varphi \quad \text{ssi} \quad \mathcal{I}\mathcal{J} \models \psi_1 \text{ ou } \mathcal{I}\mathcal{J} \models \psi_2 \\
\text{ssi} \quad \mathcal{J}\mathcal{I} \models \text{inv}(\psi_1) \text{ ou } \mathcal{J}\mathcal{I} \models \text{inv}(\psi_2) \quad \text{(par hypothèse de récurrence)} \\
\text{ssi} \quad \mathcal{J}\mathcal{I} \models \text{inv}(\psi_1) \lor \text{inv}(\psi_2) = \text{inv}(\psi_1 \lor \psi_2) = \text{inv}(\varphi)
\end{align*}
$$

Ensuite, en appliquant ce résultat à $\varphi = \alpha \triangleright \beta$, on obtient :

$$
\begin{align*}
\mathcal{M}(\text{inv}(\alpha \triangleright \beta)) &= \{\mathcal{J}\mathcal{I} \mid \mathcal{I}\mathcal{J} \in \mathcal{M}(\alpha \triangleright \beta)\} = \{\mathcal{J}\mathcal{I} \mid \mathcal{I} \in \mathcal{M}(\alpha) \text{ et } \mathcal{J} \in \mathcal{M}(\beta)\} \\
&= \mathcal{M}(\beta) \times \mathcal{M}(\alpha) = \mathcal{M}(\beta \triangleright \alpha)
\end{align*}
$$

<figure><img src="image_3.png" /></figure>

<footnote n="7">7. On rappelle qu’un rectangle d’un tel tableau (appelé contexte en AFC) est un $A \times B$ où $A \neq \emptyset$ est un ensemble de lignes et $B \neq \emptyset$, un ensemble de colonnes, tel qu’il y a une incidence sur toute $(\mathcal{I}, \mathcal{J}) \in A \times B$. Un rectangle $A \times B$ est maximal s’il n’existe aucun rectangle le contenant strictement.</footnote>
## 4.4 D'autres opérateurs de variations entre formules

On peut envisager d'autres opérateurs de variations que $▷$. L'un d'entre eux est considéré en fin de rapport (section 5.6.3) et cet opérateur est une généralisation de l'opérateur $▷$ au sens où tout modèle de $\alpha \succ \beta$ est un modèle de la variation de $\alpha$ à $\beta$ au sens de cet opérateur. On va considérer dans cette section des opérateurs plus spécifiques que $▷$: l'idée est que prendre tous les couples $\mathcal{I}\mathcal{J}$ tels que $\mathcal{I} \models \alpha$ et $\mathcal{J} \models \beta$ (comme c'est le cas avec $\alpha \succ \beta$) peut être considéré comme insuffisamment restrictif.

La question qui se pose alors est celle des critères de restriction sur ces couples. Pour ce faire, une idée inspirée d'opérateurs de révision des croyances fondés sur des distances $dist$ sur $\Omega$ consiste à ne garder dans $\mathcal{M}(\alpha \succ \beta)$ que les $\mathcal{I}\mathcal{J}$ qui minimisent $dist(\mathcal{I}, \mathcal{J})$. Formellement, on définit, à l'équivalence près, l'opérateur $▷^{dist}$ (pour $\alpha, \beta \in \mathcal{LP}$) par

$$ \mathcal{M}(\alpha \succ^{dist} \beta) = \{\mathcal{I}\mathcal{J} \in \mathcal{M}(\alpha \succ \beta) \mid \mathrm{dist}(\mathcal{I}, \mathcal{J}) = \mathrm{dist}^*\} \\ \text{où } \mathrm{dist}^* = \mathrm{dist}(\mathcal{M}(\alpha), \mathcal{M}(\beta)) $$

La révision de $\alpha$ par $\beta$ au sens d'un opérateur de révision $\ast^{dist}$ paramétré par une distance peut être définie par $\mathcal{J} \models \alpha \ast^{dist} \beta$ si $\mathrm{dist}(\mathcal{M}(\alpha), \mathcal{J}) = \mathrm{dist}^* [11]^8$. On a alors immédiatement $\mathrm{D}(\alpha \succ^{dist} \beta) \equiv \alpha \ast^{dist} \beta$ et aussi $\mathcal{G}(\alpha \succ^{dist} \beta) \equiv \beta \ast^{dist} \alpha$ (la seconde propriété est liée au fait que $\mathrm{dist}$ est symétrique). Il devrait être possible (mais c'est laissé en perspective) d'étudier les opérateurs de variations entre formules propositionnelles associées à d'autres opérateurs de révision (pas seulement ceux paramétrés par des distances) voire à d'autres opérateurs du domaine des changements de croyances (tels que les opérateurs de mise à jour).

# 5 Discussion

Ce rapport a présenté un début d'étude d'une logique des variations propositionnelles. Une tentative de construire des liens avec des travaux proches est présentée en section 5.1. Cette étude est très incomplète et peut se poursuivre de plusieurs façons, en particulier la recherche d'un système formel correct et complet pour cette logique (§5.2), la conception d'algorithmes d'inférences (§5.3), l'étude d'applications de ce formalisme (§5.4) et celle d'autres logiques des variations, s'appuyant sur d'autres logiques que la logique propositionnelle finie (§5.5). Cette discussion se termine par la présentation de plusieurs (autres) questions ouvertes (section 5.6).

## 5.1 Des travaux proches

Assez étonnamment, nous n'avons pas trouvé de travaux vraiment proches de ce travail, ce qui signifie potentiellement qu'un tel travail très proche nous a échappé (nous pensons avoir cherché sérieusement). Néanmoins, on peut tenter de faire le lien avec différents travaux.

La notion de variation propositionnelle peut évoquer la notion de différence entre fonctions booléennes (une formule de $(\mathcal{LP}, \models)$ pouvant être vue comme une représentation d'une fonction de $\{f, v\}^{|V|}$ dans $\{f, v\}$), ce qui est étudié dans les travaux d'André Thayse [16]. Dans ces travaux, la différence entre deux fonctions booléennes est calculée par un ou exclusif et ces travaux mènent à un calcul différentiel sur les fonctions booléennes inspiré des travaux en analyse sur les nombres réels (développements de Taylor, etc.). Néanmoins, si on reprend l'objectif initial de ce travail, à savoir représenter des variations utiles, en particulier pour le RàPC, le simple usage du ou exclusif s'avère insuffisant. Par exemple, la symétrie de $\oplus (\alpha \oplus \beta \equiv \beta \oplus \alpha)$ ne permet pas d'exprimer des variations orientées, i.e. de distinguer le passage de $f$ à $v$ du passage de $v$ à $f$.

<footnote n="8">8. Techniquement, dans [11], l'opérateur $\ast^{dist}$ est défini pour $dist$ étant la distance de Hamming (ce qui fait qu'il coïncide avec l'opérateur de Dalal [6]). Cependant, la généralisation à toute distance sur $\Omega$ est immédiate et satisfait les postulats AGM [1].</footnote>
La donnée d'une interprétation $\mathcal{IJ} \in \Delta\Omega$ équivaut à la donnée de la fonction qui à $a \in \mathcal{V}$ associe $(\mathcal{I}(a), \mathcal{J}(a)) \in \{\mathbf{f}, \mathbf{v}\}^2$ (correspondant aux quatre éléments de $\mathcal{D}_0$). Il est donc légitime de s'interroger sur les liens entre $(\Delta\mathcal{LP}, \models)$ et une logique avec quatre valeurs de vérité, comme c'est le cas de la logique de Belnap-Dunn [3], d'autant que les valeurs de vérité de cette logique sont parfois représentées par des couples de booléens. D'un point de vue sémantique, le lien n'est pas direct, puisque $(\Delta\mathcal{LP}, \models)$ est une logique avec deux valeurs de vérité. Par ailleurs, le nombre 4 de valeurs de vérité pour la logique de Belnap-Dunn est un fondement de cette logique alors que pour la logique des variations, il n'apparaît que comme une conséquence du choix de la logique propositionnelle comme point de départ pour construire cette logique : d'autres choix sont envisageables comme ce sera évoqué à la section 5.5 et peuvent conduire à des ensembles $\mathcal{D}_0$ de symboles de variation primitifs de cardinaux différents de 4. On peut néanmoins s'interroger sur une relation potentielle entre ces deux logiques, par exemple au niveau algorithmique. Ce travail n'a pas été fait et est une perspective potentielle.

Un lien peut être établi entre $(\Delta\mathcal{LP}, \models)$ et les logiques modales. Syntaxiquement, on pourrait considérer les symboles de variation comme autant de modalités. Sémantiquement, on pourrait définir $\models$ par la sémantique de Kripke en associant à chaque $\mathcal{IJ} \in \Delta\Omega$ un ensemble de deux mondes, $w_1$ et $w_2$, étiquetés respectivement par $\mathcal{I}$ et $\mathcal{J}$ et une relation d'accessibilité réduite à $\{(w_1, w_2)\}$. Ce lien pourrait être détaillé et étudié, même s'il apparaît à première vue comme excessif d'utiliser des logiques modales pour ne considérer que deux états (alors qu'en général, dans la sémantique de Kripke, l'ensemble des mondes et la relation d'accessibilité change d'une interprétation à une autre) et que, par ailleurs, il n'y a pas d'équivalent ici à l'emboîtement des modalités.

## 5.2 Un système formel pour $(\Delta\mathcal{LP}, \models)$

Cette section présente un système formel correct et complet pour la logique des variations proposicionnelles en expliquant comment il a été construit.

Le point de départ a été $S_H$, le système formel de Hilbert, qui est correct et complet pour la logique propositionnelle. Cela passe par une réduction aux connecteurs $\neg$ et $\rightarrow$ (sans perte d'expressivité, les autres connecteurs pouvant être définis comme des abréviations utilisant ces deux connecteurs) et à l'usage d'un ensemble réduit de symboles de variations : les symboles de variations primitifs sont suffisants et nous les avons tous considérés. Les schémas d'axiomes de $S_H$ ont été repris et d'autres ont été ajoutés qui concernent les symboles de variations. Le fait que $\{\mathcal{M}(\alpha^v) \mid v \in \mathcal{D}_0\}$ soit une partition de $\Delta\Omega$ (pour $\alpha$ satisfiable et non tautologique) nous a semblé nécessaire à exprimer pour assurer la complétude et il s'est avéré suffisant. Cela se traduit ainsi :

- D'après (9), pour tout $w, x \in \mathcal{D}_0$ avec $w \neq x$, $\models \neg(\alpha^w \wedge \alpha^x)$, ce qui se traduit sous la forme de ce schéma d'axiomes :

$$ \alpha^w \rightarrow \neg\alpha^x \quad (\text{pour } \alpha \in \mathcal{LP} \text{ et } w, x \in \mathcal{D}_0 \text{ avec } w \neq x) $$

- La relation (10) donne une tautologie qui peut être transformée en ce schéma d'axiomes :

$$ \neg\alpha^w \rightarrow (\neg\alpha^x \rightarrow (\neg\alpha^y \rightarrow \alpha^z)) \quad (\text{pour } \alpha \in \mathcal{LP} \text{ et } w, x, y, z \in \mathcal{D}_0 \text{ deux à deux distincts}) $$

En utilisant le *modus ponens* (seule règle d'inférence de $S_H$), on obtient un système formel dont il est facile de montrer qu'il est correct pour $(\Delta\mathcal{LP}, \models)$, en particulier puisque tous ses axiomes sont des tautologies. Une étude plus exhaustive de ce système est donnée en annexe A, notamment sa preuve de complétude.

Une perspective (déjà bien entamée) est la définition d'un autre système formel qui soit plus pratique à utiliser en pratique, de la même façon que la déduction naturelle est plus facile à utiliser que $S_H$.

## 5.3 Des algorithmes d'inférences

Les problèmes de décision associés à $(\Delta\mathcal{LP}, \models)$ se ramènent au problème SAT$_{\Delta}$ de la même manière que ceux associés à $(\mathcal{LP}, \models)$ se ramènent à SAT.
La méthode la plus simple à implanter pour SAT<sub>Δ</sub> consiste en une énumération des *IJ* ∈ ΔΩ, mais comme |ΔΩ| = 4^|V|, c'est une méthode très coûteuse. Plusieurs pistes sont envisageables pour trouver un algorithme plus efficace en pratique.

L'une d'elles a déjà été évoquée à la section 3.3 : elle consiste à chercher un algorithme appliquant
la méthode des tableaux sémantique pour SAT<sub>Δ</sub>. Un tel algorithme a été spécifié et implanté et ses
correction et complétude ont été prouvées (voir annexe B).

Une autre serait de chercher une traduction du problème SAT<sub>Δ</sub> en un problème SAT et de profiter
des algorithmes efficaces en pratique pour SAT. On sait qu'il existe des traductions polynomiales entre
ces deux problèmes, puisqu'ils sont tous les deux NP-complet. Il s'agirait alors de trouver une traduction
concrète qui soit efficace.

5.4 Applications potentielles

5.4.1 Au RàPC

Comme cela a été détaillé dans l'introduction, des travaux sur le RàPC, notamment pour l'appren-
tissage de connaissances d'adaptation (dans des travaux déjà anciens [7], plus récents [13] ou en cours),
ont conduit à la syntaxe de la logique des variations, mais ne produisent des expressions qui n'étaient pas
des formules logiques, avant qu'une sémantique y soit associée (et c'est l'objet principal de ce rapport).

À titre d'exemple, la règle d'adaptation *R* donnée en introduction (équation (1)) permet de résoudre
le problème d'adaptation donné par le cas (*x*<sup>s</sup>, *y*<sup>s</sup>) (représentation abstraite d'une recette de tarte aux
pommes) et le problème *x*<sup>cible</sup> (requête « Je veux une recette de dessert avec des poires. ») suivants :

$$
x^s \wedge y^s = \mathrm{rDessert} \wedge \mathrm{iPomme} \wedge \mathrm{iCannelle} \wedge \mathrm{iP\^ateBris\^ee} \wedge \neg \mathrm{iPoire} \wedge \neg \mathrm{iChocolat}
$$

$$
x^{\text{cible}} = \text{rDessert} \wedge \text{iPoire}
$$

Le résultat attendu de cette adaptation est $y^{cible} \in \mathcal{LP}$ telle que

$$
x^{\text{cible}} \wedge y^{\text{cible}} \equiv \mathbf{rDessert} \wedge \mathbf{iPoire} \wedge \mathbf{iChocolat} \wedge \mathbf{iP\^ateBris\^ee} \wedge \neg \mathbf{iPomme} \wedge \neg \mathbf{iCannelle}
$$

Une question encore ouverte est comment spécifier une telle adaptation s’appuyant sur R. Une façon de
faire qui coïncide avec le résultat attendu dans cet exemple, mais mérite d’être examinée, est la suivante.
D’abord, on vérifie que R est applicable sur le problème d’adaptation en testant la satisfiability de (x^s ∧
y^s ▷ x^cible) ∧ R (qui est satisfiable dans l’exemple). Puis, on définit l’ensemble des solutions candidates :

$$
Y = \{ y \in \mathcal{LP} \mid x^s \wedge y^s \triangleright x^{\text{cible}} \wedge y \models R \}
$$

Un $y \in Y$ n'entraîne pas nécessairement iPâteBrisée dans l'exemple : cette variable n'apparaît pas dans R. Il faut un autre critère de choix et celui de la conservation maximale du cas source (disant qu'on ne fait une modification que quand elle est nécessaire) permet d'avoir le terme iPâteBrisée.

5.4.2 À la révision des croyances

Comme le RàPC, le domaine du changement des croyances est un domaine dans lequel on considère
à la fois des assertions sur ce qui est vérifié à un moment donné (les croyances d'un agent donné à un
instant donné) et sur ce qui change ou est susceptible de changer. Pour cette raison, on peut envisager
d'utiliser le formalisme de représentation des variations présenté ici pour exprimer partiellement des
connaissances sur le changement de croyances (partiellement, car ce formalisme exprime des variations
mais ne permet pas d'exprimer des préférences entre variations). Pour explorer plus avant cette idée, on
peut s'appuyer sur les liens entre l'adaptation en RàPC et la révision des croyances (voir par exemple [4]).

Une autre idée fait suite à ce qui a été présenté en section 4.4, avec l'introduction d'un opérateur
▷dist qui est inspiré de la révision *dist*, puisque α ▷dist β permet d'exprimer dans (ΔLP, |=) à la fois
la révision α *dist* β et la révision β *dist* α (la seconde exprimant les modèles de α les plus proches
des modèles de β et intervenant dans la minimisation de la distance). Ainsi, α ▷dist β serait une façon de
réifier le changement de croyances de la révision de α par β et pas uniquement son résultat.
## 5.5 Vers d'autres logiques des différences

Le principe de construction de $(\Delta LP, \models)$ à partir de $(LP, \models)$ peut se généraliser à la construc-
tion d'une logique $(\Delta L, \models)$ partant d'une logique $(L, \models)$ dont la relation $\models$ est définie en théorie des
modèles :

- Syntaxiquement, il suffit de remplacer les atomes $a$ de $\mathcal{L}$ par des atomes $a^v$ ($v \in \mathcal{D}$) de $\Delta \mathcal{L}$;

- Sémantiquement, on définira une interprétation de $(\Delta \mathcal{L}, \models)$ comme étant un couple d'interpréta-
tions de $(\mathcal{L}, \models)$ et le reste suit le schéma de définition de $(\Delta \mathcal{LP}, \models)$.

De cette façon, on peut définir une logique des variations à partir du calcul des prédicats du premier ordre, par exemple, ou d'un de ses fragments décidables. On peut aussi appliquer ce principe sur $(\Delta LP, \models)$ pour obtenir une logique des variations de variations propositionnelles $(\Delta\Delta LP, \models)$, dont on pourrait imaginer (au moins théoriquement) qu'elle puisse s'appliquer à un système de RàPC dont l'étape d'adaptation serait un système de RàPC (travaillant sur des cas d'adaptation, voir, p. ex., [10]).

Une autre façon de généraliser ce travail concerne l'extension vers d'autres symboles de variations, pour des logiques dans lesquelles on aurait des variables non propositionnelles, par exemple des variables s'interprétant comme des nombres ou des valeurs nominales (et non des booléens). À titre d'illustration, considérons la variable âge, représentant l'âge d'une personne, pour comparer deux personnes, une de 150 ans et l'autre de 200 ans. On pourrait noter cette variation de la première personne à la seconde par âge<sup>ajouter(50)</sup> et en déduire (en s'appuyant sur des connaissances sur les variations) qu'on aura âge< (ajouter 50 ans à un âge c'est faire croître cet âge). Ce genre de symboles de variation a été introduit dans [2] qui cite, à titre d'autres exemples, les relations de l'algèbre de Allen utilisées comme symboles de variations entre deux intervalles.

## 5.6 Autres questions ouvertes

Ce rapport présente plusieurs perspectives, souvent bien entamées. Cette dernière section présente plusieurs autres, moins étudiées.

### 5.6.1 Composition des variations

Soit $\varphi$ et $\psi$, deux formules de $(\Delta LP, \models)$, représentant donc des variations propositionnelles. L'idée de les composer semble naturelle : on peut définir $\psi \circ \varphi$, la composition de $\varphi$ par $\psi$, de la même façon qu'on compose les relations binaires $M(\varphi)$ et $M(\psi)$ sur $\Omega$, i.e. pour $\mathcal{I}, \mathcal{K} \in \Omega : \mathcal{IK} \models \psi \circ \varphi$ s'il existe $\mathcal{J} \in \Omega$ telle que $\mathcal{IJ} \models \varphi$ et $\mathcal{JK} \models \psi$. En particulier, on peut montrer, avec cette définition, que, pour $\alpha, \beta, \gamma \in LP^{\text{sat}}, (\beta \succ \gamma) \circ (\alpha \succ \beta) \equiv \alpha \succ \gamma$. L'étude de cet opérateur de composition reste à faire. Par exemple, on peut montrer qu'on a $\alpha^+ \circ \alpha^- \equiv \alpha^{=v}, \alpha^+ \circ \alpha^+ \equiv \perp$ etc. (pour $\alpha \in LP$), mais il reste à étudier l'articulation entre la composition et les connecteurs.

Cette étude de la composition est motivée par l'étude de la composition des règles d'adaptation pour le raisonnement à partir de cas. En particulier, on peut s'intéresser à la question de la recherche d'une famille génératrice pour la composition de règles d'adaptation : cette problématique est encore peu étudiée (voir [17]) et mériterait de l'être dans l'optique de l'apprentissage de connaissances d'adaptation (par exemple pour réduire le nombre de règles d'adaptation apprises à valider par un expert).

### 5.6.2 Relation de conséquence dans $(\Delta LP, \models)$ modulo une base de $(LP, \models)$

Soit $\mathcal{B}$, une base de connaissances de la logique propositionnelle. Une perspective de ce travail serait d'étudier la relation $\models_B$ sur la logique des variations propositionnelles définie, pour $\varphi, \psi \in \Delta LP$ par $\varphi \models_B \psi$ si, pour toute $\mathcal{IJ} \in M(\mathcal{B}) \times M(\mathcal{B})$, $\mathcal{IJ} \models \varphi$ entraîne $\mathcal{IJ} \models \psi$. En particulier, les relations $\models$ et $\models_\emptyset$ coïncident. L'étude de cette relation devrait être utile en particulier pour l'organisation des règles d'adaptation d'un système de RàPC, étant donné les connaissances du domaine $\mathcal{B}$ de ce système.
### 5.6.3 Un fragment de $(\Delta\mathcal{L}P, \models)$

La logique des variations propositionnelles permet d'exprimer à la fois des changements – via les symboles de variations `+` et `-` – et des persistances – via les symboles de variations `=f` et `=v`. On peut s'intéresser à ne retenir que les changements, ce qui conduit à définir un fragment $(\Delta^{\pm}\mathcal{L}P, \models)$ de la logique des variations, pour lesquels les seuls symboles de variations permis soient `+` et `-`. Ce fragment est strict : il existe des formules de $\Delta\mathcal{L}P$ qui ne sont équivalentes à aucune formule de $\Delta^{\pm}\mathcal{L}P$, comme par exemple $a^{=v}$. On peut prouver cela en montrant, pour $\varphi \in \Delta^{\pm}\mathcal{L}P$, l'équivalence suivante pour toute $a \in \mathcal{V}$ : $\varphi \wedge a^{=v}$ est satisfiable ssi $\varphi \wedge a^{=f}$ est satisfiable. Comme $a^{=v} \wedge a^{=v}$ est satisfiable mais que $a^{=v} \wedge a^{=f}$ ne l'est pas, on en conclut que $a^{=v}$ n'est pas expressible dans $(\Delta^{\pm}\mathcal{L}P, \models)$.

Un intérêt de ce fragment serait de « forcer » à exprimer des variations plus générales. Par exemple, si on prend $\alpha, \beta \in \mathcal{L}P^{\text{sat}}$, la variation $\alpha \succ \beta$ ne réalise pas de généralisation puisqu'elle permet de « retrouver » $\alpha$ et $\beta$ (cf. (15)). Supposons qu'on trouve un moyen d'associer à toute formule $\varphi \in \Delta\mathcal{L}P$ une formule $\varphi^{\pm} \in \Delta^{\pm}\mathcal{L}P$ qui soit une généralisation minimale de $\varphi$ : $\varphi \models \varphi^{\pm}$ et, pour toute formule $\psi \in \Delta^{\pm}\mathcal{L}P$ telle que $\varphi \models \psi$, on aurait $\varphi^{\pm} \models \psi$. L'existence pour toute formule $\varphi \in \Delta\mathcal{L}P$ d'une telle formule $\varphi^{\pm}$ est une question ouverte (son unicité, à l'équivalence près, est facile à montrer). Dans le cas où une telle formule existerait (ou, du moins, existerait pour les formules fermées), on pourrait définir $(\alpha \succ \beta)^{\pm}$ qui serait une façon plus générale que $\alpha \succ \beta$ de traiter de la variation de $\alpha$ vers $\beta$.

La conjecture suivante sur $\varphi^{\pm}$ est proposée. Soit $\sim$ la relation d'équivalence sur $\Delta\Omega$ définie de la façon suivante (pour $\mathcal{I}_1\mathcal{J}_1, \mathcal{I}_2\mathcal{J}_2 \in \Delta\Omega$) : $\mathcal{I}_1\mathcal{J}_1 \sim \mathcal{I}_2\mathcal{J}_2$ si pour toute $a \in \mathcal{V}$, $\mathcal{I}_1\mathcal{J}_1 \models a^{=\neg}$ ssi $\mathcal{I}_2\mathcal{J}_2 \models a^{=\neg}$ et $\mathcal{I}_1\mathcal{J}_1 \models a^{=\dagger}$ ssi $\mathcal{I}_2\mathcal{J}_2 \models a^{=\dagger}$. Soit alors $\mathcal{C}\ell_{\sim}(\mathcal{I}\mathcal{J})$ la classe d'équivalence d'une $\mathcal{I}\mathcal{J} \in \Delta\Omega$. Nous pensons que le résultat suivant est correct :

$$ \mathcal{M}(\varphi^{\pm}) = \bigcup \{\mathcal{C}\ell_{\sim}(\mathcal{I}\mathcal{J}) \mid \mathcal{I}\mathcal{J} \in \mathcal{M}(\varphi)\} \quad (\text{conjecture}) $$

pour toute formule $\varphi$ de la logique des variations propositionnelles.

## 6 Remerciements

Les auteurs tiennent à remercier les relecteurs de l'article soumis et accepté aux JIAF (dont ce rapport est une version étendue) pour leurs remarques constructives et encourageantes, ainsi qu'Henri Prade pour plusieurs conseils judicieux qui ont été utiles à cet article.

Les annexes qui suivent réunissent des preuves de résultats annoncées dans le corps du document et qui était souvent trop longues pour ledit corps.

# A Un système formel correct et complet « à la Hilbert » pour $(\Delta\mathcal{L}P, \models)$

## A.1 Un système formel « à la Hilbert » pour $(\Delta\mathcal{L}P, \models)$

Dans cette partie, on limitera la syntaxe aux atomes de la forme $a^v$, avec $a \in \mathcal{V}$ et $v \in \mathcal{D}_0$, et aux connecteurs `->` et `~`. On a vu que cela ne réduit pas l'expressivité de la syntaxe, et cela va permettre d'obtenir un système formel très ramassé.

On réutilise les schémas d'axiomes du système de Hilbert pour la logique propositionnelle, pour les formules de $(\Delta\mathcal{L}P, \models)$ :

$$ (SA1) : \varphi \rightarrow (\psi \rightarrow \varphi) $$

$$ (SA2) : (\varphi \rightarrow (\psi \rightarrow \theta)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \theta)) $$

$$ (SA3) : (\neg\varphi \rightarrow \neg\psi) \rightarrow (\psi \rightarrow \varphi) $$
auxquels on adjoint deux schémas d'axiomes supplémentaires, décrivant le partitionnement de l'ensemble des interprétations par les symboles de variation primitifs : si $v$, $w$, $x$ et $y$ sont des éléments de $\mathcal{D}_0$ deux à deux distincts.

$$ (SA4) : \alpha^v \to \neg\alpha^w $$

$$ (SA5) : \neg\alpha^v \to (\neg\alpha^w \to (\neg\alpha^x \to \alpha^y)) $$

Enfin, on utilise l'unique règle d'inférence (*modus ponens*) :

$$ \frac{\varphi \quad \varphi \to \psi}{\psi} \quad \text{m.p.} $$

Nous noterons $A_{x_\Delta}$ l'ensemble des axiomes engendré par les cinq schémas d'axiomes (SA1), (SA2), (SA3), (SA4) et (SA5), $RI_\Delta = \{m.p.\}$, et $S_{\Delta H} = (A_{x_\Delta}, RI_\Delta)$. La relation d'inférence associée à ce système formel sera noté $\vdash^\Delta$: $\mathcal{B} \vdash^\Delta \varphi$ s'il existe une preuve de $\varphi$ sous les hypothèses de $\mathcal{B}$.

La prochaine section va démontrer que ce système formel est correct pour $(\Delta LP, \models)$, la suivante qu'il est complet.

## A.2 Correction de $S_{\Delta H}$

### Théorème A.2.1 (Correction de $S_{\Delta H}$)

Soit $\mathcal{B}$ un ensemble de formules de $\Delta LP$, et $\varphi$ une formule de $\Delta LP$. Si $\mathcal{B} \vdash^\Delta \varphi$, alors $\mathcal{B} \models \varphi$. En particulier, si $\vdash^\Delta \varphi$, alors $\varphi$ est une tautologie.

**Preuve de (A.2.1).** Le schéma des preuves de correction suit souvent un plan classique : les schémas d'axiomes ne produisent que des tautologies, les règles d'inférence produisent des conclusions correctes si les prémisses le sont, et on termine par induction sur la taille d'une preuve.

(1) Si $\varphi$ est une formule dérivée d'un des trois premiers schémas d'axiomes (SA1), (SA2) ou (SA3), on utilise le résultat de transposition (A.7.2) pour démontrer que $\varphi$ est une tautologie.

(2) Si $v, w \in \mathcal{D}_0$ avec $v \neq w$, et si $a \in \mathcal{V}$, alors quelle que soit l'interprétation $\mathcal{IJ}$, si $\mathcal{IJ} \models a^v$, alors $\mathcal{IJ} \not\models a^w$. Donc $\models a^v \to \neg a^w$.

Si maintenant $\alpha \in LP$, le théorème de substitution A.6.2 permet d'écrire $\models (a^v \to a^w) [a \setminus \alpha]$, soit $\models \alpha^v \to \neg\alpha^w$.

(3) Si $a$ est une variable quelconque, on vérifie facilement que quelle que soit $\mathcal{IJ} \in \Delta\Omega$,

$$ \mathcal{IJ} \models a^{=f} \lor a^{=v} \lor a^{=} \lor a^{-} $$

ce qui permet d'écrire, en remplaçant $u \lor v$ par $\neg u \to v$, $4! = 24$ tautologies de la forme

$$ \neg a^v \to (\neg a^w \to (\neg a^x \to a^y)) $$

où $v, w, x$ et $y$ sont des éléments de $\mathcal{D}_0$ deux à deux distincts. Encore une fois, le théorème de substitution A.6.2 permet de conclure que toute formule issue de (SA5) est une tautologie.

(4) Soit maintenant $\varphi \in \Delta LP$, telle que $\mathcal{B} \vdash^\Delta \varphi$.

Notons $(\varphi_1, \dots, \varphi_n)$ une preuve de $\varphi$ sous hypothèse $\mathcal{B}$, et raisonnons par récurrence sur la longueur $n$ de cette preuve.

* Si $n = 1$, alors $\varphi = \varphi_n$ est nécessairement soit issue d'un schéma d'axiomes, et l'on vient de montrer que dans ce cas $\models \varphi$, d'où par monotonie (A.6.3) $\mathcal{B} \models \varphi$, soit une formule de $\mathcal{B}$, auquel cas on a encore (d'après A.7.3(i)) $\mathcal{B} \models \varphi$.

* Supposons avoir prouvé que si $(\psi_1, \dots, \psi_p)$ est une preuve de $\psi \in \Delta LP$ sous hypothèse $\mathcal{B}$, de longueur $p < n$, alors $\mathcal{B} \models \psi_p$.
▷ Si $\varphi_n$ est issue d'un schéma d'axiomes, alors $\models \varphi_n$, donc $\mathcal{B} \models \varphi_n = \varphi$.

▷ Si $\varphi_n \in \mathcal{B}$, alors évidemment $\mathcal{B} \models \varphi_n = \varphi$.

▷ Enfin, si $\varphi_n$ est obtenue par application du *modus ponens* à $\varphi_i$ et $\varphi_j = (\varphi_i \rightarrow \varphi_n)$, avec $i, j < n$, alors $(\varphi_1, \dots, \varphi_i)$ et $(\varphi_1, \dots, \varphi_j)$ sont des preuves respectives de $\varphi_i$ et $\varphi_j$ sous hypothèses $\mathcal{B}$, de longueurs strictement inférieures à $n$, donc $\mathcal{B} \models \varphi_i$ et $\mathcal{B} \models \varphi_j$ par hypothèse de récurrence.

D'après la propriété A.7.3(iii), on en déduit que $\mathcal{B} \models \varphi_n = \varphi$.

■

## A.3 Compléture de $S_{\Delta\mathcal{H}}$

Cette section est organisée pour donner en premier les résultats principaux et ensuite les lemmes sur lesquels ils s'appuient (avec une référence à ces lemmes).

**Théorème A.3.1 (compléture de $S_{\Delta\mathcal{H}}$) :** Soit $\mathcal{B}$ un ensemble de formules de $\Delta\mathcal{LP}$, et $\varphi$ une formule de $\Delta\mathcal{LP}$. Si $\mathcal{B} \models \varphi$, alors $\mathcal{B} \vdash^\Delta \varphi$.

En particulier, si $\varphi$ est une tautologie, alors $\vdash^\Delta \varphi$.

La preuve de compléture du système formel « à la Hilbert » repose sur l'équivalence entre la *cohérence* (i.e. la non-contradiction) et la *satisfiabilité*. Elle va s'articuler de la manière suivante :

(1) nous montrerons d'abord que tout ensemble cohérent de formules $\mathcal{B}$ peut être complété en un ensemble maximalement cohérent $\mathcal{B}'$,

(2) nous montrerons ensuite que $\mathcal{B}'$ est satisfiable, et donc que $\mathcal{B}$ l'est aussi,

(3) nous conclurons enfin à la compléture de $S_{\Delta\mathcal{H}}$.

Commençons par un peu de vocabulaire : si $\mathcal{B}$ permet de prouver une formule $\varphi$ et sa négation $\neg\varphi$, on dit que $\mathcal{B}$ est incohérent, et qu'il est cohérent dans le cas contraire. On dit aussi que $\mathcal{B}$ est maximalement cohérent (ou que $\mathcal{B}$ est clos pour la cohérence) si il est cohérent et si pour toute formule $\varphi$, soit $\mathcal{B} \cup \{\varphi\}$ est incohérent, soit $\mathcal{B} \vdash^\Delta \varphi$.

Commençons par l'implication facile « satisfiable $\rightarrow$ cohérent ».

**Proposition A.3.2 :** Si l'ensemble de formules $\mathcal{B}$ est satisfible alors il est cohérent.

**Preuve de (A.3.2).** Supposons que $\mathcal{B}$ soit contradictoire. Alors il existe une formule $\varphi$ telle que $\mathcal{B} \vdash^\Delta \varphi$ et $\mathcal{B} \vdash^\Delta \neg\varphi$. Par correction, on en déduit que $\mathcal{B} \models \varphi$ et $\mathcal{B} \models \neg\varphi$, ce qui entraîne immédiatement que $\mathcal{B}$ n'est pas satisfiable. Le résultat en découle en contraposant. ■

Montrons maintenant que si $\mathcal{B}$ est un ensemble de formules cohérent, alors on peut l'étendre en un ensemble $\mathcal{B}'$ de formules maximalement cohérent, au sens suivant : $\mathcal{B} \subseteq \mathcal{B}'$, et si $\mathcal{B}' \subsetneq \mathcal{B}''$, alors $\mathcal{B}''$ est contradictoire.

**Proposition A.3.3 (Extension maximalement cohérente d'un ensemble de formule $\mathcal{B}$)**

Soit $\mathcal{B}$ un ensemble de formules cohérent. Il existe un ensemble $\mathcal{B}'$ de formules maximalement cohérent contenant $\mathcal{B}$.

**Preuve de (A.3.3).**

On supposera ici que l'ensemble $\mathcal{V}$ est au plus *dénombrable*<fnref n="9" />. Cela permet d'introduire une numérotation des formules de $\Delta\mathcal{LP}$ sous forme d'une suite $(\varphi_i)_{i \in \mathbb{N}}$, avec $\varphi_0$, un axiome de $S_{\Delta\mathcal{H}}$.

<footnote n="9">9. Cette hypothèse est largement suffisante dans toutes les applications informatiques. Le théorème de compatité qui découle immédiatement de la preuve de compléture montrera en fait que ce résultat est valable pour un ensemble quelconque de variables.</footnote>
Posons $\mathcal{B}_0 = \mathcal{B}$, et posons, pour tout $n \in \mathbb{N}$ :

$$ \mathcal{B}_{n+1} = \begin{cases} \mathcal{B}_n & \text{si } \mathcal{B}_n \vdash^\Delta \neg \varphi_{n+1} \\ \mathcal{B}_n \cup \{\varphi_{n+1}\} & \text{sinon} \end{cases} $$

Montrons que chaque $\mathcal{B}_n$ est (i) cohérent, et (ii) vérifie $\mathcal{B}_n \vdash^\Delta \varphi_n$ ou $\mathcal{B}_n \vdash^\Delta \neg \varphi_n$.

* C'est vrai pour le cas de base, puisque $\mathcal{B}_0$ est supposé cohérent et que $\mathcal{B}_0 \vdash^\Delta \varphi_0$ ($\varphi_0$ étant un axiome).

* Supposons que $\mathcal{B}_n$ vérifie (i) et (ii). Deux cas peuvent se produire :

▷ si $\mathcal{B}_n \vdash^\Delta \neg \varphi_{n+1}$, alors $\mathcal{B}_{n+1} = \mathcal{B}_n$, donc $\mathcal{B}_{n+1}$ satisfait (i) et (ii), par hypothèse de récurrence;

▷ si $\mathcal{B}_n \nvdash^\Delta \neg \varphi_{n+1}$ alors $\mathcal{B}_{n+1} = \mathcal{B}_n \cup \{\varphi_{n+1}\}$ satisfait (ii) ; montrons que (i) est également satisfaite ;

supposons que $\mathcal{B}_{n+1}$ ne soit pas cohérent ; alors par le principe de contradiction (A.7.1), $\mathcal{B}_{n+1} \vdash^\Delta \neg \varphi_{n+1}$, ce qui se traduit par $\mathcal{B}_n \cup \{\varphi_{n+1}\} \vdash^\Delta \neg \varphi_{n+1}$, et donc par le théorème de déduction (A.6.1) que $\mathcal{B}_n \vdash^\Delta \varphi_{n+1} \rightarrow \neg \varphi_{n+1}$;

par contradiction (A.7.3(xi)), on en déduit que $\mathcal{B}_n \vdash^\Delta \neg \varphi_{n+1}$, en contradiction avec ce qu'on a supposé plus haut ; donc $\mathcal{B}_{n+1}$ est nécessairement cohérent.

Posons alors $\mathcal{B}' = \bigcup_{n \in \mathbb{N}} \mathcal{B}_n$, et montrons que $\mathcal{B}'$ est maximalement cohérent.

* Si $\mathcal{B}'$ n'était pas cohérent, alors il existerait une formule $\chi$ telle que $\mathcal{B}' \vdash^\Delta \chi$ et $\mathcal{B}' \vdash^\Delta \neg \chi$.

Les preuves étant des objets finis, les deux preuves de $\mathcal{B}' \vdash^\Delta \chi$ et $\mathcal{B}' \vdash^\Delta \neg \chi$ n'utilisent qu'un nombre fini de formules de $\mathcal{B}'$.

Il existe donc $n \in \mathbb{N}^*$ tel que $\mathcal{B}_n$ contient toutes les formules nécessaires à ces deux preuves. Et nous pouvons considérer ces deux preuves comme étant deux preuves dans $\mathcal{B}_n$, ce qui prouverait que $\mathcal{B}_n$ est incohérent, en contradiction avec sa construction.

* Supposons que $\mathcal{B}'$ ne soit pas maximal. Alors il existe une formule $\varphi_n$ telle que $\mathcal{B}' \nvdash^\Delta \varphi_n$ et $\mathcal{B}' \cup \{\varphi_n\}$ est cohérent.

Mais $\mathcal{B}_n \subseteq \mathcal{B}'$, et soit $\mathcal{B}_n \vdash^\Delta \varphi_n$, soit $\mathcal{B}_n \vdash^\Delta \neg \varphi_n$.

Si $\mathcal{B}_n \vdash^\Delta \varphi_n$, alors par monotonie (A.6.3), $\mathcal{B}' \vdash^\Delta \varphi_n$, en contradiction avec l'hypothèse. Donc $\mathcal{B}_n \vdash^\Delta \neg \varphi_n$.

Par monotonie toujours, $\mathcal{B}' \vdash^\Delta \neg \varphi_n$, donc

$$ \mathcal{B}' \cup \{\varphi_n\} \vdash^\Delta \neg \varphi_n \quad \text{et} \quad \mathcal{B}' \cup \{\varphi_n\} \vdash^\Delta \varphi_n $$

la deuxième affirmation étant évidente. Ainsi, $\mathcal{B}' \cup \{\varphi_n\}$ est incohérent, en contradiction avec l'hypothèse initiale.

<figure><img src="image_4.png" /></figure>

Nous allons maintenant prouver que l'ensemble de formule $\mathcal{B}'$ est syntaxiquement complet, ce qui signifie que pour toute formule $\varphi \in \Delta \mathcal{L} \mathcal{P}$, il existe une preuve de $\varphi$ ou de $\neg \varphi$ sous hypothèse $\mathcal{B}'$.

**Proposition A.3.4 :** $\mathcal{B}'$ est syntaxiquement complet : pour toute formule $\varphi \in \Delta \mathcal{L} \mathcal{P}$, soit $\mathcal{B}' \vdash^\Delta \varphi$, soit $\mathcal{B}' \vdash^\Delta \neg \varphi$.

**Preuve de (A.3.4).** Soit $\varphi \in \Delta \mathcal{L} \mathcal{P}$. Si $\varphi = \varphi_n$, $\mathcal{B}_n \subseteq \mathcal{B}'$, et par construction de $\mathcal{B}_n$, soit $\mathcal{B}_n \vdash^\Delta \varphi_n$, soit $\mathcal{B}_n \vdash^\Delta \neg \varphi_n$. Donc soit $\mathcal{B}' \vdash^\Delta \varphi$, soit $\mathcal{B}' \vdash^\Delta \neg \varphi$. ■

<figure><img src="image_5.png" /></figure>

Venons-en à la pièce maîtresse de la démonstration :

**Théorème A.3.5 (cohérent → satisfiable) :** Si $\mathcal{B}$ est cohérent, alors $\mathcal{B}$ est satisfiable.
**Preuve de (A.3.5).** Soit $\mathcal{B}$ un ensemble de formules cohérent, $\mathcal{B}'$ l'extension maximalement cohérente de $\mathcal{B}$ construite ci-dessus, et $\varphi \in \Delta\mathcal{LP}$.

Si $a \in \mathcal{V}$, considérons les quatre formules $a^{=f}$, $a^{=v}$, $a^{+}$ et $a^{-}$. Pour chacune, d'après la proposition A.3.4, soit elle peut être prouvée sous hypothèse $\mathcal{B}'$, soit sa négation peut l'être. Et les quatre négations ne peuvent simultanément être prouvées, à cause du schéma d'axiomes (SA5) et de la cohérence de $\mathcal{B}'$.

Ainsi, au moins une formule est prouvable, et à cause du schéma d'axiomes (SA4), au plus une l'est. Notons $\nu_a$ l'unique symbole de variation tel que $\mathcal{B}' \vdash^\Delta a^{\nu_a}$.

Considérons alors l'interprétation $\mathcal{IJ}$ définie sur chaque variable propositionnelle $a \in \mathcal{V}$ et chaque symbole de variation primitif $v$ par :

$$ \mathcal{IJ} \models a^v \quad \text{ssi} \quad v = \nu_a $$

Montrons alors que $\mathcal{B}' \vdash^\Delta \varphi$ si et seulement si $\mathcal{IJ} \models \varphi$. Raisonnons par induction structurelle sur $\varphi$.

* Cas de base : $\varphi = a^v$, avec $a \in \mathcal{V}$ et $v \in \mathcal{D}_0$

Par construction de $\mathcal{IJ}$, $\mathcal{IJ} \models \varphi = a^v$ si et seulement si $v = \nu_a$, donc $\mathcal{IJ} \models \varphi$ si et seulement si $\mathcal{B}' \vdash^\Delta \varphi$.

* Induction :

▷ Cas $\varphi = \neg\psi$

— Si $\mathcal{B}' \vdash^\Delta \varphi = \neg\psi$, alors par cohérence, $\mathcal{B}' \nvdash^\Delta \psi$, donc par hypothèse d'induction, $\mathcal{IJ} \nvDash \psi$, et $\mathcal{IJ} \models \neg\psi = \varphi$;

— et si $\mathcal{B}' \nvdash^\Delta \varphi = \neg\psi$, alors par complétude syntaxique, $\mathcal{B}' \vdash^\Delta \psi$, donc par hypothèse d'induction, $\mathcal{IJ} \models \psi$, et $\mathcal{IJ} \nvDash \neg\psi = \varphi$.

▷ Cas $\varphi = (\psi \to \theta)$

— Si $\mathcal{B}' \vdash^\Delta \varphi = (\psi \to \theta)$, alors par complétude syntaxique, $\mathcal{B}' \vdash^\Delta \psi$ ou $\mathcal{B}' \vdash^\Delta \neg\psi$.

Dans le premier cas, par application du *modus ponens*, $\mathcal{B}' \vdash^\Delta \theta$, donc $\mathcal{IJ} \models \theta$, et $\mathcal{IJ} \models \psi \to \theta = \varphi$.

Dans le second cas, $\mathcal{IJ} \nvDash \psi$, donc $\mathcal{IJ} \models \psi \to \theta = \varphi$.

— Si $\mathcal{B}' \nvdash^\Delta \varphi = (\psi \to \theta)$, alors par complétude syntaxique $\mathcal{B}' \vdash^\Delta \neg(\psi \to \theta)$. D'après (SA1), $\vdash^\Delta \theta \to (\psi \to \theta)$, donc nécessairement $\mathcal{B}' \nvdash^\Delta \theta$, et par hypothèse d'induction $\mathcal{IJ} \nvDash \theta$.

Supposons que $\mathcal{IJ} \models \varphi = \psi \to \theta$. Alors par négation de l'implication (A.7.3(xiii)), $\mathcal{IJ} \nvDash \psi$, donc par hypothèse d'induction $\mathcal{B}' \vdash^\Delta \neg\psi$.

D'après le principe de non cohérence (A.7.3(x)), $\neg\psi \to (\psi \to \theta)$, donc $\mathcal{B}' \vdash^\Delta (\psi \to \theta)$, contradiction.

Donc $\mathcal{IJ} \models \psi \to \theta = \varphi$.

■

## A.4 Preuve de la complétude de $\mathcal{S}_{\Delta\mathcal{H}}$

Il ne reste plus que quelques lignes de démonstration pour arriver à notre but : montrer que si $\mathcal{B} \models \varphi$, alors $\mathcal{B} \vdash^\Delta \varphi$ (ce qui achèvera la preuve du théorème de complétude A.3.1).

**Preuve de (A.3.1).** Soit $\varphi \in \Delta\mathcal{LP}$. Supposons que $\mathcal{B} \nvdash^\Delta \varphi$.

Alors, de la même façon que dans la preuve de la proposition A.3.3, $\mathcal{B} \cup \{\neg\varphi\}$ est cohérent, donc satisfiable d'après le théorème A.3.5, donc $\mathcal{B} \nvDash \varphi$.

L'énoncé du théorème s'en déduit par contraposition.

■

## A.5 Théorème de compactité

Après tous ces efforts, on prouve en quelques lignes supplémentaires le théorème de compactité, qui peut s'énoncer de deux manières différentes :
## Théorème A.5.1

* $\mathcal{B}$ est satisfiable si et seulement si tout sous-ensemble fini de $\mathcal{B}$ est satisfiable.

* $\mathcal{B}$ est contradictoire si et seulement si il existe un sous-ensemble fini de $\mathcal{B}$ qui l'est.

Ce résultat permet, il nous semble, de s'affranchir de l'hypothèse de dénombrabilité de l'ensemble $\mathcal{V}$.
**Preuve de (A.5.1).** La condition nécessaire est évidente. Montrons la condition suffisante par contraposition.

Supposons $\mathcal{B}$ non satisfiable. Alors d'après le théorème A.3.5, $\mathcal{B}$ est incohérent. Il existe donc une certaine formule $\varphi$ telle que $\mathcal{B} \vdash^\Delta \varphi$ et $\mathcal{B} \vdash^\Delta \neg\varphi$.

Les preuves étant des objets finis, il existe un sous-ensemble fini $\mathcal{B}^*$ de $\mathcal{B}$ tel que $\mathcal{B}^* \vdash^\Delta \varphi$ et $\mathcal{B}^* \vdash^\Delta \neg\varphi$.

Alors, par correction, $\mathcal{B}^* \models \varphi$ et $\mathcal{B}^* \models \neg\varphi$. Donc $\mathcal{B}^*$ n'est pas satisfiable.

■

## A.6 Les résultats utilisés dans ces preuves

Les preuves de correction et de complétude données plus haut utilisent un certain nombre de résultats qui sont rassemblés ci-dessous.

### A.6.1 Théorème de la déduction

#### Théorème A.6.1 (de la déduction)

Soit $\mathcal{B}$ un ensemble de formules, $\varphi$ et $\psi$ deux formules. $\mathcal{B} \cup \{\varphi\} \vdash^\Delta \psi$ si et seulement si $\mathcal{B} \vdash^\Delta \varphi \rightarrow \psi$.

**Preuve de (A.6.1).**

* ($\leftarrow$) $\mathcal{B} \subseteq \mathcal{B} \cup \{\varphi\}$, donc comme $\mathcal{B} \vdash^\Delta (\varphi \rightarrow \psi)$, $\mathcal{B} \cup \{\varphi\} \vdash^\Delta (\varphi \rightarrow \psi)$.

On a vu que $\mathcal{B} \cup \{\varphi\} \vdash^\Delta \varphi$, et on en déduit, par le *modus ponens*, que $\mathcal{B} \cup \{\varphi\} \vdash^\Delta \psi$.

* ($\rightarrow$) Soit $(\psi_1, \dots, \psi_n)$ une preuve de $\psi = \psi_n$ sous hypothèses $\mathcal{B} \cup \{\varphi\}$. Raisonnons par récurrence sur la longueur de cette preuve.

▷ Si $\psi_n$ est un axiome ou un élément de $\mathcal{B}$, alors la suite

<table><thead><tr><th>nom</th><th>formule</th><th>explications</th></tr></thead><tbody><tr><td>$\xi_1$</td><td>$\psi$</td><td>axiome ou élément de $\mathcal{B}$</td></tr><tr><td>$\xi_2$</td><td>$\psi \rightarrow (\varphi \rightarrow \psi)$</td><td>(SA1)</td></tr><tr><td>$\xi_3$</td><td>$\varphi \rightarrow \psi$</td><td>m.p. sur $\xi_1$ et $\xi_2$</td></tr></tbody></table>

est une preuve de $\varphi \rightarrow \psi$ sous hypothèse $\mathcal{B}$.

▷ Si $\psi = \varphi$, alors le lemme d'identité (A.7.3(v)) nous permet de déduire que $\vdash^\Delta \psi \rightarrow \psi$.

▷ Si $\psi_n = \psi$ est obtenue par application du *modus ponens* sur $\psi_i$ et $\psi_j = (\psi_i \rightarrow \psi_n)$, avec $i, j < n$, alors $(\psi_1, \dots, \psi_i)$ et $(\psi_1, \dots, \psi_j)$ sont des preuves respectives de $\psi_i$ et $\psi_j$ sous hypothèse $\mathcal{B} \cup \{\varphi\}$, de longueurs strictement inférieures à $n$.

Par hypothèse de récurrence,

$$ \mathcal{B} \vdash^\Delta (\varphi \rightarrow \psi_i) \quad \text{et} \quad \mathcal{B} \vdash^\Delta (\varphi \rightarrow \psi_j) = (\varphi \rightarrow (\psi_i \rightarrow \psi_j)) $$

On peut alors construire le schéma de preuve suivant pour $\varphi \rightarrow \psi$ :

<table><thead><tr><th>nom</th><th>formule</th><th>explications</th></tr></thead><tbody><tr><td>$\xi_1$</td><td>$\varphi \rightarrow \psi_i$</td><td>conséquence pour $\vdash^\Delta$ de $\mathcal{B}$</td></tr><tr><td>$\xi_2$</td><td>$\varphi \rightarrow (\psi_i \rightarrow \psi)$</td><td>conséquence pour $\vdash^\Delta$ de $\mathcal{B}$</td></tr><tr><td>$\xi_3$</td><td>$(\varphi \rightarrow (\psi_i \rightarrow \psi)) \rightarrow ((\varphi \rightarrow \psi_i) \rightarrow (\varphi \rightarrow \psi))$</td><td>(SA2)</td></tr><tr><td>$\xi_4$</td><td>$(\varphi \rightarrow \psi_i) \rightarrow (\varphi \rightarrow \psi)$</td><td>m.p. sur $\xi_1$ et $\xi_2$</td></tr><tr><td>$\xi_5$</td><td>$\varphi \rightarrow \psi$</td><td>m.p. sur $\xi_1$ et $\xi_4$</td></tr></tbody></table>
### A.6.2 Substitution d'une collection de formules de $\Delta\mathcal{L}\mathcal{P}$ dans une formule de $\mathcal{L}\mathcal{P}$

Soit $\alpha \in \mathcal{L}\mathcal{P}$ une formule de la logique propositionnelle, et $\chi$ une application de l'ensemble $\mathcal{V}(\alpha)$ des variables de $\alpha$ dans $\Delta\mathcal{L}\mathcal{P}$.

On note $\chi(\alpha)$ la formule obtenue en substituant dans $\alpha$ chaque occurrence de variable $a \in \mathcal{V}(\alpha)$ par $\chi(a)$. Nous appelons « transformée de $\alpha$ par $\chi$ » cette nouvelle formule.

De manière plus précise :

* si $\alpha = a$ avec $a \in \mathcal{V}$, alors $\chi(\alpha) = \chi(a)$,

* si $\alpha = \neg\beta$, avec $\beta \in \mathcal{L}\mathcal{P}$, alors $\chi(\alpha) = \neg\chi(\beta)$,

* si $\alpha = \beta \to \gamma$, avec $\beta$ et $\gamma$ dans $\mathcal{L}\mathcal{P}$, alors $\chi(\alpha) = \chi(\beta) \to \chi(\gamma)$.

On a le résultat suivant (qui est un deuxième théorème de substitution, le premier étant donné par (11), page 9) :

**Théorème A.6.2 (substitution 2) :** Soit $\alpha \in \mathcal{L}\mathcal{P}$ et $\chi : \mathcal{V}(\alpha) \to \Delta\mathcal{L}\mathcal{P}$. Si $\models \alpha$, alors $\models \chi(\alpha)$.

**Preuve de (A.6.2).** Cette preuve se place dans le cadre de la restriction aux connecteurs $\neg$ et $\to$ dans les deux logiques.

Soit $\mathcal{I}\mathcal{J} \in \Delta\Omega$, et $\chi : \mathcal{V}(\alpha) \to \Delta\mathcal{L}\mathcal{P}$.

Notons $\widehat{\mathcal{I}\mathcal{J}} \in \Omega$ définie de la manière suivante : $\widehat{\mathcal{I}\mathcal{J}} \models a$ ssi $\mathcal{I}\mathcal{J} \models \chi(a)$.

Nous allons montrer que $\mathcal{I}\mathcal{J} \models \chi(\alpha)$ ssi $\widehat{\mathcal{I}\mathcal{J}} \models \alpha$.

La preuve se fait par induction structurelle sur $\alpha$ :

* si $\alpha = a$, avec $a \in \mathcal{V}$, alors $\chi(\alpha) = \chi(a)$, et $\mathcal{I}\mathcal{J} \models \chi(a)$ ssi $\widehat{\mathcal{I}\mathcal{J}} \models a = \alpha$;

* si $\alpha = \neg\beta$, avec $\beta \in \mathcal{L}\mathcal{P}$, alors $\chi(\alpha) = \neg\chi(\beta)$, et

$$ 
\begin{array}{l}
\mathcal{I}\mathcal{J} \models \chi(\alpha) \quad \text{ssi } \mathcal{I}\mathcal{J} \nvDash \chi(\beta) \\
\qquad \quad \text{ssi } \widehat{\mathcal{I}\mathcal{J}} \nvDash \beta \qquad \text{(par hypothèse d'induction)} \\
\qquad \quad \text{ssi } \widehat{\mathcal{I}\mathcal{J}} \models \neg\beta = \alpha
\end{array}
$$

* enfin si $\alpha = \beta \to \gamma$, avec $\beta, \gamma \in \mathcal{L}\mathcal{P}$, alors $\chi(\alpha) = \chi(\beta) \to \chi(\gamma)$, et

$$ 
\begin{array}{l}
\mathcal{I}\mathcal{J} \nvDash \chi(\alpha) = \chi(\beta) \to \chi(\gamma) \quad \text{ssi } \mathcal{I}\mathcal{J} \models \chi(\beta) \text{ et } \mathcal{I}\mathcal{J} \nvDash \chi(\gamma) \\
\qquad \quad \text{ssi } \widehat{\mathcal{I}\mathcal{J}} \models \beta \text{ et } \widehat{\mathcal{I}\mathcal{J}} \nvDash \gamma \qquad \text{(par hypothèse d'induction)} \\
\qquad \quad \text{ssi } \widehat{\mathcal{I}\mathcal{J}} \nvDash \beta \to \gamma = \alpha
\end{array}
$$

La fin de la preuve est alors évidente : si $\alpha$ est une tautologie, alors quelle que soit $\mathcal{I}\mathcal{J} \in \Delta\Omega$, $\widehat{\mathcal{I}\mathcal{J}} \models \alpha$, donc $\widehat{\mathcal{I}\mathcal{J}} \models \chi(\alpha)$. Ainsi, $\chi(\alpha)$ est bien une tautologie (de $\Delta\mathcal{L}\mathcal{P}$).

### A.6.3 Monotonie

On note $\text{Th}(\mathcal{B})$ l'ensemble des formules que l'on peut déduire de $\mathcal{A}x \cup \mathcal{B}$ à l'aide du seul *modus ponens*.

**Proposition A.6.3 (monotonie) :**

* Si $\mathcal{B} \subseteq \mathcal{B}'$, alors $\text{Th}(\mathcal{B}) \subseteq \text{Th}(\mathcal{B}')$ (monotonie).

* Si $\mathcal{B} \vdash \Delta \mathcal{B}'$, alors $\text{Th}(\mathcal{B}') \subseteq \text{Th}(\mathcal{B})$ (monotonie forte).
**Preuve de (A.6.3).** Ces deux propriétés découlent directement de la définition de $\mathrm{Th}(\mathcal{B})$ :

* Si $\mathcal{B} \subseteq \mathcal{B}'$, alors toute preuve de $\varphi$ sous l'hypothèse $\mathcal{B}$ est encore une preuve de $\varphi$ sous l'hypothèse $\mathcal{B}'$.

* Si $\mathcal{B} \vdash^\Delta \mathcal{B}'$, alors $\mathcal{B}' \subseteq \mathrm{Th}(\mathcal{B})$, et par définition de la clôture, $\mathrm{Th}(\mathcal{B}') \subseteq \mathrm{Th}(\mathcal{B})$.

■

Ce résultat permet entre autre, dans les preuves, d’utiliser des « théorèmes » prouvés précédemment. Plus précisément :

**Proposition A.6.4**

Si $\mathcal{T}$ est un théorème du système formel $\mathcal{S} = (\mathcal{L}, \mathrm{Ax}, \mathrm{RI})$, alors, en notant $\mathcal{S}' = (\mathcal{L}, \mathrm{Ax} \cup \{\mathcal{T}\}, \mathrm{RI})$,

$$ \mathcal{B} \vdash_S \varphi \text{ si et seulement si } \mathcal{B} \vdash_{S'} \varphi $$

**Preuve de (A.6.4).** Dans un sens, c’est simplement une expression de la monotonie, dans l’autre, il suffit, dans une preuve de $\mathcal{B} \vdash_{S'} \varphi$, de remplacer toutes les utilisations de $\mathcal{T}$ par une preuve de $\mathcal{T}$ dans $\mathcal{S}$. ■

## A.7 Principe de contradiction

**Proposition A.7.1 (principe de contradiction)**

Si $\mathcal{B} \vdash^\Delta \varphi$ et $\mathcal{B} \vdash^\Delta \neg\varphi$, alors $\mathcal{B} \vdash^\Delta \psi$ pour toute formule $\psi$.

**Preuve de (A.7.1).** Par monotonie forte (A.6.3), puisque $\mathcal{B} \vdash^\Delta \varphi$ et $\mathcal{B} \vdash^\Delta \neg\varphi$, $\mathrm{Th}(\mathcal{B} \cup \{\varphi, \neg\varphi\}) \subseteq \mathrm{Th}(\mathcal{B})$. Il suffit donc de prouver que $\mathcal{B} \cup \{\varphi, \neg\varphi\} \vdash^\Delta \psi$.

<table><thead><tr><th>nom</th><th>formule</th><th>explications</th></tr></thead><tbody><tr><td>ξ<sub>1</sub></td><td>¬φ → (¬ψ → ¬φ)</td><td>(SA1)</td></tr><tr><td>ξ<sub>2</sub></td><td>¬φ</td><td>hypothèse</td></tr><tr><td>ξ<sub>3</sub></td><td>¬ψ → ¬φ</td><td>m.p. sur ξ<sub>1</sub> et ξ<sub>2</sub></td></tr><tr><td>ξ<sub>4</sub></td><td>(¬ψ → ¬φ) → (φ → ψ)</td><td>(SA3)</td></tr><tr><td>ξ<sub>5</sub></td><td>φ → ψ</td><td>m.p. sur ξ<sub>3</sub> et ξ<sub>4</sub></td></tr><tr><td>ξ<sub>6</sub></td><td>φ</td><td>hypothèse</td></tr><tr><td>ξ<sub>7</sub></td><td>ψ</td><td>m.p. sur ξ<sub>6</sub> et ξ<sub>5</sub></td></tr></tbody></table>

■

### A.7.1 Autres résultats importants

La plupart des preuves de ces résultats découlent de la proposition suivante, qui utilise le fait que le système de Hilbert est correct et complet pour la logique $(\mathcal{LP}, \models)$ :

**Proposition A.7.2 (transposition de preuve de $\mathcal{LP}$ dans $\Delta\mathcal{LP}$)**

Soit $\alpha \in \mathcal{LP}$, $V = \mathcal{V}(\alpha)$ et $\chi: V \to \Delta\mathcal{LP}$. On note $\chi(\alpha)$ la formule obtenue en substituant $a$ par $\chi(a)$ dans $\alpha$, pour toute $a \in V$. On a alors : si $\models \alpha$, alors $\vdash^\Delta \chi(\alpha)$.

**Preuve de (A.7.2).** Nous ne donnerons que le plan général, les détails sont laissés à la sagacité du lecteur.

Soit $\alpha \in \mathcal{LP}$ telle que $\models \alpha$. Par compléture de $S_H$ pour $(\mathcal{LP}, \models)$, $\vdash_H \alpha$ (où $\vdash_H$ est la relation de conséquence du système formel de Hilbert).
Soit $(\alpha_1, \dots, \alpha_p)$ une preuve de $\alpha$ dans $S_H$. On peut montrer, par récurrence sur la longueur de cette
preuve, que $(\chi(\alpha_1), \dots, \chi(\alpha_p))$ est une preuve $^{10}$ de $\chi(\alpha)$ dans $S_{\Delta H}$.

Cette proposition permet d'utiliser les preuves déjà connues pour ($\mathcal{LP}, \models$) de nombreux résultats pour les transposer dans ($\Delta\mathcal{LP}, \models$). Les résultats suivants sont ceux utilisés pour les preuves des résultats principaux, on trouve leurs démonstrations dans tout document apportant la preuve de la compléture du système formel de Hilbert pour la logique ($\mathcal{LP}, \models$) :

**Proposition A.7.3**

(i) $\{\varphi\} \vdash^{\Delta} \varphi$.

(ii) Si $\mathcal{B} \subseteq \mathcal{B}'$ et $\mathcal{B} \vdash^{\Delta} \varphi$, alors $\mathcal{B}' \vdash^{\Delta} \varphi$.

(iii) Si $\mathcal{B} \vdash^{\Delta} \varphi$ et $\mathcal{B} \vdash^{\Delta}(\varphi \to \psi)$, alors $\mathcal{B} \vdash^{\Delta} \psi$.

(iv) Si $(\varphi_1, \dots, \varphi_n)$ est une preuve de $\varphi = \varphi_n$ sous hypothèse $\mathcal{B}$, alors pour tout $k \in [1, n-1]$,
$(\varphi_1, \dots, \varphi_k)$ est une preuve de $\varphi_k$ sous hypothèse $\mathcal{B}$.

(v) $\vdash^{\Delta}(\varphi \rightarrow \varphi)$ (lemme d'identité).

(vi) $\vdash^{\Delta} \neg\neg\varphi \rightarrow \varphi$ (élimination de la double négation).

(vii) $\vdash^{\Delta} \varphi \rightarrow \neg\neg\varphi$ (introduction de la double négation).

(viii) $\{\varphi \to \psi, \psi \to \theta\} \vdash^{\Delta} \varphi \to \theta$ (syllogisme hypothétique).

(ix) $\vdash^{\Delta}(\varphi \rightarrow \psi) \rightarrow (\neg\psi \rightarrow \neg\varphi)$ (*modus tollens*).

(x) Pour tout $\theta \in \Delta\mathcal{LP}$, $\vdash^{\Delta} \neg\neg\varphi \rightarrow (\neg\varphi \rightarrow \theta)$.
Pour tout $\theta \in \Delta\mathcal{LP}$, $\vdash^{\Delta} \neg\varphi \rightarrow (\varphi \rightarrow \theta)$ (non cohérence).

(xi) $\vdash^{\Delta}(\varphi \rightarrow \neg\varphi) \rightarrow \neg\varphi$ (raisonnement par contradiction).

(xii) $\vdash^{\Delta}(\varphi \rightarrow \psi) \rightarrow ((\neg\varphi \rightarrow \psi) \rightarrow \psi)$ (raisonnement par disjonction).
Corollaire : si $\mathcal{B} \cup \{\varphi\} \vdash^{\Delta} \psi$ et $\mathcal{B} \cup \{\neg\varphi\} \vdash^{\Delta} \psi$, alors $\mathcal{B} \vdash^{\Delta} \psi$.

(xiii) $\vdash^{\Delta} \neg\varphi \rightarrow ((\psi \rightarrow \varphi) \rightarrow \neg\psi)$.
$\vdash^{\Delta} \varphi \rightarrow (\neg\psi \rightarrow \neg(\varphi \rightarrow \psi))$ (négation de l'implication).

B Un algorithme correct et complet selon la méthode des tableaux séman-
tiques pour ($\Delta\mathcal{LP}, \models$)

B.1 La méthode des tableaux sémantiques pour la logique ($\Delta\mathcal{LP}, \models$)

Soit $\varphi \in \Delta\mathcal{LP}$. Notons $T_0$ l'arbre composé d'une unique racine, étiquetée avec une forme normale sans négation de la formule $\psi = \neg\varphi$ (on rappelle qu'une forme normale sans négation de $\chi \in \Delta\mathcal{LP}$ est une formule $\chi'$ telle que $\chi \equiv \chi'$ et telle que les seuls connecteurs de $\chi'$ sont $\wedge$ et $\vee$ et les seules occurrences de $\alpha^v$ sont telles que $\alpha \in \mathcal{V}$ et $v \in \mathcal{D}_0$).

Si $\mathcal{T}$ est un arbre étiqueté avec des sous-formules de $\psi$, on peut créer un nouvel arbre $\mathcal{T}'$ en appliquant
l'une des deux règles suivantes :

règle (A) : si une formule $\varphi_{\alpha}$ de la forme $\eta_1 \wedge \dots \wedge \eta_p$ apparaît dans le chemin de $X$ à $Y$, on ajoute à la
suite de $Y$ une branche dont chaque nœud est une formule $\eta_i$ :

<footnote n="10">10. qui n'utilise d'ailleurs que les schémas d'axiomes communs aux systèmes formels $S_H$ et $S_{\Delta H}$, et le *modus ponens*.</footnote>
<figure><img src="image_6.png" /></figure>

**règle (B)** : si une formule $\varphi_\beta$ de la forme $\nu_1 \lor \dots \lor \nu_p$ apparaît dans le chemin de $X$ à $Y$, on ajoute à la suite de $Y$ une branche pour chacune des formules $\nu_i$ :

<figure><img src="image_7.png" /></figure>

Plus formellement, partant d'un tableau $T_1$, on dit que $T_2$ est une *extension directe* de $T_1$ si $T_2$ s'obtient à partir de $T_1$ par application d'une des deux règles (A) ou (B) ci-dessus.

Un arbre $\mathcal{T}$ est appelé *tableau sémantique pour la formule* $\varphi \in \Delta \mathcal{LP}$ si il existe une suite d'arbre $T_0, \dots, T_n$ telle que $T_0$ est défini comme précédemment, $T_n = \mathcal{T}$, et pour chaque $i \in [1, n]$, $T_i$ est une extension directe de $T_{i-1}$.

Deux remarques importantes :

(1) dans ce procédé, les tailles des sous-formules extraites par les opérations (A) et (B) sont strictement inférieures à la taille des formules dont sont tirés les nœuds engendrés;

(2) contrairement à ce qui se passe dans la logique du premier ordre <fnref n="11" />, une fois qu'une formule a subi une opération (A) ou (B) dans une branche, il est inutile de répéter cette opération <fnref n="12" />, puisqu'on ne ferait réapparaître que des sous-formules déjà présentes.

De ces deux remarques, on déduit que le procédé d'extension se termine après un nombre fini d'opérations, et conduit à un arbre possédant un nombre fini de branches, chaque branche étant de longueur finie.

Une branche d'un tableau (i.e. un chemin de la racine vers une feuille de l'arbre) est dite *close* si elle contient deux nœuds étiquetés par deux étiquettes $a^v$ et $a^w$, où $a \in \mathcal{V}$, $v, w \in D_0$ et $v \neq w$.

Un tableau est dit *clos* si toutes ses branches sont closes. On dit que *Tprouve* $\varphi$ si $\mathcal{T}$ est un tableau pour $\varphi$ et si $\mathcal{T}$ est clos.

<footnote n="11">11. pour laquelle le développement d'une formule de la forme $(\forall x) P(x)$ peut éventuellement être répété pour plusieurs valeurs particulières de $x$.</footnote>

<footnote n="12">12. et il ne faut donc surtout pas le faire, pour éviter des branches de longueur infinie et un processus de développement ne se terminant pas.</footnote>
D'autre part, une branche d'un tableau sera dite *complète* si

▷ pour toute formule $\varphi_\alpha = \eta_1 \wedge \dots \wedge \eta_p$ sur cette branche, toute les formules $\eta_i$ sont aussi sur cette branche (autrement dit toutes les règles de type (A) possibles ont été appliquées),

▷ pour toute formule $\varphi_\beta = \nu_1 \vee \dots \vee \nu_p$, au moins une formule $\nu_i$ est présente sur cette branche (autrement dit, toutes les règles de type (B) ont été appliquées sur cette branche).

Un tableau est dit *complet* si toutes ses branches sont soit closes, soit complètes. Pour un tel tableau, il n'y a aucune règle permettant d'obtenir une prolongation profitable, pouvant changer le résultat de la méthode.

Enfin, si une branche complète de $\mathcal{T}$ n'est pas close, nous dirons qu'elle est *ouverte*.

Pour résumer, un tableau $\mathcal{T}$ pour $\varphi$ est un arbre dont la racine est $\neg\varphi$, obtenu à partir du tableau $\mathcal{T}_0$ formé de l'unique racine étiquetée par $\neg\varphi$ en appliquant un certain nombre de fois l'une des deux règles (A) ou (B). Ce tableau peut être partiellement ou complètement développé. Il est clos si toutes ses branches contiennent un conflit, c'est-à-dire deux étiquettes de la forme $a^v$ incompatibles. Il n'a pas besoin d'être complètement développé dans la pratique, mais pour obtenir une information sur $\varphi$ (le fait que ce soit une tautologie ou non), il faudra qu'il soit complet, ce qui signifie que chaque branche est complète, ou contient un conflit.

## B.2 Correction de la méthode des tableaux sémantiques

**Théorème B.2.1 :** Si le tableau $\mathcal{T}$ pour la formule $\varphi$ est clos, alors $\varphi$ est une tautologie.

**Preuve de (B.2.1).** Soit $\mathcal{T}$ un tableau pour la formule $\varphi \in \Delta LP$, $\Theta$ une branche de $\mathcal{T}$ (i.e. un chemin de la racine de l'arbre à une feuille) et $IJ$ une interprétation. Nous dirons que $IJ$ satisfait la branche $\Theta$ si $IJ$ satisfait toutes les formules sur cette branche, et que $IJ$ satisfait $\mathcal{T}$ si $IJ$ satisfait au moins une des branches de $\mathcal{T}$.

Supposons alors que $\mathcal{T}'$ soit une extension de $\mathcal{T}$, obtenue en prolongeant une branche $\Theta$ de $\mathcal{T}$ par application d'une règle (A) ou (B). Supposons encore que l'interprétation $IJ$ satisfasse $\mathcal{T}$, et que $\Theta'$ soit une branche de $\mathcal{T}$ satisfaite par cette interprétation. Nous allons montrer que l'interprétation $IJ$ satisfait encore $\mathcal{T}'$.

Si $\Theta$ et $\Theta'$ sont distinctes, alors $\Theta'$ est encore une branche de $\mathcal{T}'$, et comme elle était satisfaite par $IJ$ dans $\mathcal{T}$, elle l'est encore dans $\mathcal{T}'$.

Si maintenant $\Theta = \Theta'$, de deux choses l'une.

▷ La branche $\Theta$ a été étendue en appliquant une règle (A) à l'une des formules $\varphi_\alpha$ étiquetant un de ses nœuds. $\varphi_\alpha$ était une conjonction de la forme $\varphi_\alpha = \eta_1 \wedge \dots \wedge \eta_p$, et on a prolongé la branche $\Theta$ en ajoutant l'un après l'autre les formules $\eta_1, \dots, \eta_p$.

Par hypothèse, l'interprétation $IJ$ satisfait $\varphi_\alpha$, ce qui signifie que $IJ$ satisfait chacune des formules $\eta_1, \dots, \eta_p$. La branche obtenue en étendant $\Theta$ ne comporte donc toujours que des formules satisfaites par $IJ$, et est donc encore satisfaite par $IJ$. Ainsi, l'interprétation $IJ$ satisfait une branche de $\mathcal{T}'$, et $IJ$ satisfait donc $\mathcal{T}'$.

▷ La branche $\Theta$ a été étendue en appliquant une règle (B) à l'une des formules $\varphi_\beta$ étiquetant un de ses nœuds. $\varphi_\beta$ était donc une disjonction, de la forme $\varphi_\beta = \nu_1 \vee \dots \vee \nu_p$, et on a ajouté au bout de $\Theta$ p fils étiquetés par ces p formules $\nu_i$.

Par hypothèse, l'interprétation $IJ$ satisfait $\Theta$, donc la formule $\varphi_\beta$, ce qui signifie que $IJ$ satisfait au moins une formule $\nu_j$.

Alors la branche de $\mathcal{T}'$ obtenue en prolongeant $\Theta$ par le nœud $\nu_j$ ne contient que des nœuds étiquetés par des formules satisfaites par l'interprétation $IJ$, cette branche, et par voie de conséquence le tableau $\mathcal{T}'$, sont donc encore satisfaits par l'interprétation $IJ$.

Ainsi, pour toute extension $\mathcal{T}'$ d'un tableau $\mathcal{T}$, et pour toute interprétation $IJ$, $IJ$ satisfait $\mathcal{T}$ entraîne $IJ$ satisfait $\mathcal{T}'$.
Par récurrence structurelle, si l'interprétation $\mathcal{IJ}$ satisfait la racine $\neg\varphi$ du tableau, elle satisfait toute suite de tableaux construits par extension.

Par contraposée, aucune interprétation ne satisfaisant un tableau clos, ce qui signifie que sa racine $\neg\varphi$ n'est satisfaite par aucune interprétation. Cette racine est donc insatisfiable, ce qui signifie que $\varphi$ est une tautologie, ce que nous voulions prouver. ■

## B.3 Compléture de la méthode des tableaux sémantiques

Pour prouver le résultat de cette section, suivant en cela la voie tracée par [15], nous aurons besoin de la définition suivante :

### Définition B.3.1

Soit $S$ un ensemble de formules de $\Delta LP$. On dira que $S$ est un ensemble de Hintikka si

(1) $S$ ne contient pas deux formules $a^v$ et $a^w$, avec $a \in \mathcal{V}$, $v, w \in \mathcal{D}_0$ et $v \neq w$,

(2) si $\varphi_\alpha = \eta_1 \wedge \dots \wedge \eta_p \in S$, alors pour tout $i$, $\eta_i \in S$,

(3) si $\varphi_\beta = \nu_1 \vee \dots \vee \nu_p \in S$, alors il existe $i$ tel que $\nu_i \in S$.

Intuitivement, un ensemble de Hintikka contient toutes les formules qu'on rencontre le long d'une branche complètement développée d'un tableau sémantique.

Nous utiliserons le résultat suivant<fnref n="13" /> :

**Lemme B.3.1 (Hintikka) :** Tout ensemble de Hintikka $S$ est satisfiable.

**Preuve de (B.3.1).** Pour cela, notons $\mathcal{IJ}_S$ l'interprétation définie comme suit<fnref n="14" /> :

* si $a \in \mathcal{V}$ est présente dans au moins une formule de $S$, sous la forme $a^v$ avec $v \in \mathcal{D}_0$, on pose $\mathcal{IJ}_S(a^v) = v$, et $\mathcal{IJ}_S(a^w) = f$ si $w \in \mathcal{D}_0$ et $w \neq v$,

* si $a \in \mathcal{V}$ est absente de toute formule de $S$, on donne la valeur $v$ à l'un quelconque des $\mathcal{IJ}(a^v)$, la valeur $f$ aux trois autres.

Notons que le premier point est possible parce que, par hypothèse, $S$ ne contient pas de formules contenant des atomes incompatibles.

Montrons alors que toute formule de $S$ est vrai sous l'interprétation $\mathcal{IJ}_S$, par récurrence sur la taille de ces formules.

▷ Tous les atomes présents dans $S$ sont satisfaits par l'interprétation $\mathcal{IJ}_S$, par construction de $\mathcal{IJ}_S$.

▷ Soit alors $\psi$ une formule de $S$ de taille $n$ strictement positive. Supposons que toute formule de $S$ de taille strictement inférieure à $n$ soit satisfaite par l'interprétation $\mathcal{IJ}_S$.

Comme $\psi$ est de taille strictement positive, deux cas peuvent se produire :

Cas 1 : $\psi = \eta_1 \wedge \dots \wedge \eta_p$ ; comme $S$ est un ensemble de Hintikka, $S$ contient toutes les formules $\eta_i$, qui sont de tailles strictement inférieures à $n$, donc satisfaites par l'interprétation $\mathcal{IJ}_S$, donc $\psi$ est satisfaite par cette interprétation ;

Cas 2 : $\psi = \nu_1 \vee \dots \vee \nu_p$ ; comme $S$ est un ensemble de Hintikka, $S$ contient au moins l'une des formules $\nu_i$, qui est de taille strictement inférieure à $n$, donc satisfaite par l'interprétation $\mathcal{IJ}_S$ par hypothèse ; $\psi$ est donc elle aussi satisfaite par cette interprétation.

On peut alors démontrer le résultat de cette section :

<footnote n="13">13. En fait, on peut se contenter ici d'un résultat plus faible en ne faisant la preuve que pour des ensembles de Hintikka *finis*, puisque l'arbre complètement développé ne comporte qu'un nombre fini de branches, toutes de longueur finie. Mais ça ne coûte rien de prouver le résultat plus général.</footnote>

<footnote n="14">14. On écrira parfois $\mathcal{IJ}_S(\varphi) = v$ pour signifier que $\mathcal{IJ}_S \models \varphi$.</footnote>
**Théorème B.3.2**

Si $\varphi$ est une tautologie, alors il existe $\mathcal{T}$ pour la formule $\varphi$ qui est clos.

Plus généralement, si $\varphi$ est une tautologie, alors tout tableau complet $\mathcal{T}$ pour $\varphi$ est clos.

**Preuve de (B.3.2).** Nous allons procéder par contraposée. Soit $\varphi$ une formule de $\Delta\mathcal{L}\mathcal{P}$, et $\mathcal{T}$ un tableau complet pour $\varphi$. Supposons que $\mathcal{T}$ ne soit pas clos, et montrons que $\neg\varphi$ est satisfiable.

Par hypothèse, il existe une branche $\Theta$ complète et ouverte. Notons $S$ l'ensemble des formules éti-
quetant les branches de $\Theta$. Alors, par complétude et non clôture, $S$ un ensemble de Hintikka. En effet,

(1) puisque $\Theta$ n'est pas close, $S$ ne peut pas contenir formules $a^v$ et $a^w$ incompatibles,

(2) par complétude du tableau et par définition de la règle de développement (A), si $\varphi_\alpha = \eta_1 \wedge \cdots \wedge \eta_p \in S$, alors pour tout $i$, $\eta_i \in S$,

(3) toujours par complétude du tableau, et par définition de la règle de développement (B), si $\varphi_\beta = \nu_1 \vee \cdots \vee \nu_p \in S$, alors il existe $i$ tel que $\nu_i \in S$.

Ceci montre le résultat suivant :

**Proposition B.3.3 :** Toute branche complète et ouverte d'un tableau est satisfiable.

On en déduit le résultat qui nous intéresse :

**Théorème B.3.4 :** Si $\varphi$ est une tautologie, alors tout tableau complet pour $\varphi$ est clos.

En effet, en contraposant, si $\mathcal{T}$ est un tableau ouvert pour $\varphi$, $\mathcal{T}$ contient au moins une branche satisfiable, qui contient en particulier la racine $\neg\varphi$. Cette dernière est donc satisfiable, ce qui signifie que $\varphi$ n'est pas une tautologie. ■

Enfin, comme toute formule $\varphi$ permet de construire au moins un tableau, on a encore le résultat suivant :

**Théorème B.3.5 (Complétude de la méthode des tableaux sémantiques)**

Toute tautologie est prouvable par la méthode des tableaux.

Références

[1] C. E. ALCHOURRÓN, P. GÄRDENFORS et D. MAKINSON : On the logic of theory change : partial meet functions for contraction and revision. *J. Symbolic Logic*, 50:510–530, 1985.

[2] F. BADRA et J. LIEBER : Une approche pour représenter les variations entre cas — Vers une application à l'extraction de connaissances d'adaptation. In A. CORDIER, éditeur : *15ème atelier sur le raisonnement à partir de cas*, pages 47–56, Grenoble, 2007.

[3] N. D. BELNAP : How a computer should think. *New essays on Belnap-Dunn logic*, pages 35–53, 2019.

[4] J. COJAN et J. LIEBER : Applying belief revision to case-based reasoning. In H. PRADE et G. RICHARD, éditeurs : *Computational Approaches to Analogical Reasoning : Current Trends*, volume 548 de *Studies in Computational Intelligence*, pages 133–161. Springer, 2014.

[5] A. CORDIER, V. DUFOUR-LUSSIER, J. LIEBER, E. NAUER, F. BADRA, J. COJAN, E. GAILLARD, L. INFANTE-BLANCO, P. MOLLI, A. NAPOLI et H. SKAF-MOLLI : Taaable : a Case-Based System for personalized Cooking. In S. MONTANI et L. C. JAIN, éditeurs : *Successful Case-based Reasoning Applications-2*, volume 494 de *Studies in Computational Intelligence*, pages 121–162. Springer, 2014.

[6] M. DALAL : Investigations into a theory of knowledge base revision : Preliminary report. In *Proceedings of the Seventh National Conference on Artificial Intelligence (AAAI)*, pages 475–479, 1988.
[7] M. D'AQUIN, F. BADRA, S. LAFROGNE, J. LIEBER, A. NAPOLI et L. SZATHMARY : Case base mining for adaptation knowledge acquisition. In M. M. VELOSO, éditeur : Proc. of the 20th Int. Joint Conf. on Artificial Intelligence (IJCAI'07), pages 750-755. Morgan Kaufmann, Inc., 2007.

[8] B. GANTER et R. WILLE : *Formal concept analysis : mathematical foundations*. Springer Science & Business Media, 2012.

[9] K. HANNEY et M. T. KEANE : Learning adaptation rules from a case-base. In I. SMITH et B. FALTINGS, éditeurs : *Advances in Case-Based Reasoning – Proc. of the Third Eur. Workshop, EWC-BR'96*, LNAI 1168, pages 179-192. Springer Verlag, Berlin, 1996.

[10] J. JARMULAK, S. CRAW et R. ROWE : Using case-base data to learn adaptation knowledge for design. In *Proc. of the 17th Int. Joint Conf. on Artificial Intelligence (IJCAI'01)*, pages 1011–1016. Morgan Kaufmann, Inc., 2001.

[11] H. KATSUNO et A. MENDELZON : Propositional knowledge base revision and minimal change. *Artificial Intelligence*, 52(3):263-294, 1991.

[12] D. LEAKE, X. YE et D. J CRANDALL : Supporting Case-Based Reasoning with Neural Networks : An Illustration for Case Adaptation. In AAAI Spring Symposium : *Combining Machine Learning with Knowledge Engineering*, volume 2, 2021.

[13] J. LIEBER et E. NAUER : Adaptation knowledge discovery using positive and negative cases. In *ICCBR 2021 - 29th International Conference on Case-Based Reasoning*, Salamanca (Virtual), Spain, 2021.

[14] C. K. RIESBECK et R. C. SCHANK : *Inside Case-Based Reasoning*. Lawrence Erlbaum Associates, Inc., Hillsdale, New Jersey, 1989. Available on line.

[15] R. M. SMULLYAN : *First-order logic*. Courier Corporation, 1995.

[16] A. THAYSE : *Boolean calculus of differences*. Springer, 1981.

[17] M. TIXIER, F. BADRA et J. LIEBER : Familles génératrices de règles d'adaptation pour assister leur acquisition semi-automatique. In *19èmes Journées Francophones d'Ingénierie des Connaissances (IC 2008)*, pages 225-236, Nancy, France, juin 2008.