Méthode des tableaux

En théorie de la démonstration, les tableaux sémantiques sont une méthode de résolution du problème de la décision pour le calcul des propositions et les logiques apparentées, ainsi qu'une méthode de preuve pour la logique du premier ordre. La méthode des tableaux peut également déterminer la satisfiabilité des ensembles finis de formules de diverses logiques. C'est la méthode de preuve la plus populaire pour les logiques modales (Girle 2000). Elle fut inventée par le logicien hollandais Evert Willem Beth.

Représentation graphique d'un tableau propositionnel partiellement construit

Introduction

Pour les tableaux de réfutation, le but est de montrer que la négation d'une formule ne peut être satisfaite. Il existe des règles pour traiter chacun des connecteurs logiques. Dans certains cas, appliquer ces règles divise le sous-tableau en deux. Les quantificateurs sont instanciés. Si chaque branche du tableau mène à une contradiction évidente, la branche est fermée. Si toutes les branches sont fermées, la preuve est terminée et la formule d'origine est vraie.

Bien que l'idée fondamentale sous-jacente à la méthode des tableaux soit dérivée du théorème d'élimination des coupures de la théorie de la démonstration, les origines du calcul des tableaux se trouvent dans la sémantique des connecteurs logiques, le lien avec la théorie de la preuve ne s'étant effectué que dans les dernières décennies.

Plus spécifiquement, un calcul de tableaux consiste en une collection finie de règles, dont chacune spécifie comment déstructurer un connecteur logique en ses constituants. Les règles sont typiquement exprimées sous forme d'ensembles de formules, bien qu'il existe des logiques pour lesquelles des structures de données plus compliquées doivent être utilisées, telles que les multiensembles, les listes ou les arbres de formules. En conséquence, dans la suite, « ensemble » renverra indifféremment aux termes suivants : ensemble, liste, multiensemble, arbre.

S'il existe une règle pour chaque connecteur logique, la procédure finit par produire un ensemble composé uniquement de formules atomiques et de leurs négations. Un tel ensemble, dont aucun élément ne peut se voir appliquer de règle, est aisément reconnaissable comme satisfiable ou non satisfiable dans le cadre de la logique considérée. Les éléments d'un tableau sont donc disposés en un arbre, dont la racine est la formule de départ, et dont les branches sont créées et vérifiées de manière systématique. On obtient ainsi un algorithme de déduction et de raisonnement automatique.

Logique propositionnelle classique

Cette section présente une méthode des tableaux pour la logique propositionnelle classique.

Règles

Pour montrer qu'une formule $B$ est valide sous les hypothèses $A_{1},\ldots ,A_{n}$, on montre par réfutation que l'ensemble de formules $\{A_{1},\ldots ,A_{n},\neg B\}$ est insatisfiable. Pour cela, on place tout d'abord les formules sur une branche, et on applique un certain nombre de règles à ces formules ainsi qu'aux formules obtenues consécutivement.

Du fait des lois de De Morgan, les connecteurs ont des sémantiques reliées. Par conséquent on regroupe les formules entre deux catégories:

$\alpha (A,B)$	$A\wedge B$	$\neg (\neg A\vee \neg B)$	$\neg (A\rightarrow \neg B)$
$\beta (A,B)$	$A\vee B$	$\neg (\neg A\wedge \neg B)$	$(\neg A)\rightarrow B$

Quand une formule de type $\alpha (A,B)$ apparaît sur une branche, les deux formules $A$ et $B$ sont des conséquences logiques de cette formule. Par conséquent on les ajoute toutes deux sur la branche.

Si une formule de type $\beta (A,B)$ est vraie sur une branche, l'une au moins des deux formules $A$ et $B$ en découle. Par conséquent on crée deux nouvelles branches et on ajoute $A$ sur l'une et $B$ sur l'autre.

Une branche est fermée si une formule et sa négation (aux lois de De Morgan près) apparaissent dessus. Un tableau est fermé si toutes ses branches sont fermées. On peut montrer qu'un ensemble de formules est insatisfiable en logique classique propositionnelle ssi il existe un tableau fermé partant de celui-ci. On dit alors que la méthode des tableaux est correcte et complète pour cette logique.

Quand les règles ont été appliquées sur toutes les formules du tableau et qu'il n'est pas possible de le fermer, alors l'ensemble de formules de départ est satisfiable. En particulier, toutes les branches qu'il n'est pas possible de fermer forment un modèle pour l'ensemble de départ. Du point de vue de la réfutation, ces branches peuvent être vues comme des contre-exemples à la validité de la formule de départ.

Exemples

On veut montrer que $a$ est une conséquence de $(a\vee \neg b)\wedge b$ en logique classique propositionnelle. Par réfutation, il s'agit donc de montrer que $\{(a\vee \neg b)\wedge b,\neg a\}$ est insatisfiable. On démarre donc avec le tableau :

La première formule est de type $\alpha$, on ajoute donc $a\vee \neg b$ et $b$ sur la branche pour obtenir le tableau :

$a\vee \neg b$ est de type $\beta$, il faut donc créer deux branches, l'une contenant $a$, l'autre $\neg b$ :

Les deux branches sont fermées : en effet, la première contient $a$ et $\neg a$, et la seconde $b$ et $\neg b$. On peut représenter ces fermetures de la façon suivante :

Par conséquent le tableau est fermé, l'ensemble de formule de départ est insatisfiable et $a$ est une conséquence de $(a\vee \neg b)\wedge b$.

Si on part de l'ensemble de formules $\{a\wedge c,\neg a\vee b\}$, on obtient finalement le tableau suivant :

Ce tableau ne peut être fermé, donc l'ensemble de départ est satisfiable. En particulier, il est satisfait dans le modèle où $a,b,c$ sont interprétées par vrai, comme le montre la branche de droite qui ne peut être fermée.

Logique classique du premier ordre

Dans cette section, on étend la méthode présentée à la section précédente à la logique du premier ordre.

Première approche

Pour pouvoir traiter les quantificateurs, on ajoute deux nouvelles règles, en regroupant une nouvelle fois les quantificateurs grâce à la dualité de la logique classique.

$\gamma x.~A(x)$	$\forall x.~A(x)$	$\neg (\exists x.~\neg A(x))$
$\delta x.~A(x)$	$\exists x.~A(x)$	$\neg (\forall x.~\neg A(x))$

Pour les formules de type $\gamma$, on instancie $x$ par un certain terme $t$ dans $A(x)$ et on l'ajoute à la branche.

Pour les formules de type $\delta$, on utilise la skolémisation : on remplace $x$ par une constante fraîche $c$ dans $A(x)$ et on l'ajoute à la branche.

Pour que la méthode soit complète, il est parfois nécessaire d'appliquer la règle $\gamma$ plusieurs fois, en instanciant $x$ par des termes différents. Le tableau suivant montre que l'ensemble de formules $\{\forall x.~P(x),\exists x.~(\neg P(x)\vee \neg P(f(x)))\}$ est insatisfiable. Dans la colonne de droite sont indiqués le numéro de la formule et le connecteur décomposés pour obtenir les formules au niveau correspondant.

Métavariables et unification

Comme on le voit dans l'exemple précédent, il est nécessaire de deviner les termes qui instancient $x$ dans les règles $\gamma$ de façon à pouvoir fermer les branches. Du point de vue de la démonstration automatique, on ne peut évidemment pas instancier $x$ de façon exhaustive jusqu'à trouver les bons. À la place de cela, on remplace $x$ par ce que l'on va appeler une métavariable $X$, et c'est au moment où on cherchera à fermer les branches que l'on cherchera comment instancier $X$. Pour cela, on va chercher à unifier (à négation près) deux formules de la branches. Néanmoins, il ne suffit pas de pouvoir trouver un telle unification pour chacune des branches : il faut trouver une substitution qui permette de fermer toutes les branches à la fois. On parle dans ce cas d'unification rigide. Il faut également modifier la règle $\delta$, car en skolémisant, il faut prendre en compte les métavariables présentes. Par conséquent, on y instancie $x$ par $f(Y_{1},\ldots ,Y_{n})$ où $Y_{1},\ldots ,Y_{n}$ sont les méta-variables présentes sur la branche où se situe la formule décomposée.

La figure suivante représente un tableau avec métavariables et unification pour l'ensemble de formules $\{\forall x.~P(x),\exists x.~(\neg P(x)\vee \neg P(f(x)))\}$

Le problème d'unification $\{X'=c(X),X''=f(c(X))\}$ est soluble, il est donc possible de fermer le tableau.

Stratégies

Comme on le voit dans le tableau précédent, il est parfois inutile d'appliquer une règle $\gamma$ (celle qui a produit $P(X)$). En général, il vaut mieux appliquer les règles $\delta$ avant, pour limiter le nombre de métavariables. De la même façon, il vaut mieux appliquer des règles autres que $\beta$ pour éviter de dupliquer le nombre de branches. Une stratégie possible est d'appliquer en priorité les règles $\alpha$, puis $\delta$, puis $\beta$ et enfin $\gamma$. On peut montrer que cette stratégie reste complète, c'est-à-dire qu'un tableau fermé sera trouvé si l'ensemble de formules de départ est insatisfiable.

Bibliographie

• Girle, Rod, 2000. Modal Logics and Philosophy. Teddington UK: Acumen.
• François Rivenc, Introduction à la Logique, où cette méthode est appelée « méthode des arbres de vérité ».