Méthode des tableaux

Pour montrer qu'une formule ${\displaystyle B}$ est valide sous les hypothèses ${\displaystyle A_{1},\ldots ,A_{n}}$, on montre par réfutation que l'ensemble de formules ${\displaystyle \{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:

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

Quand une formule de type ${\displaystyle \alpha (A,B)}$ apparaît sur une branche, les deux formules ${\displaystyle A}$ et ${\displaystyle 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 ${\displaystyle \beta (A,B)}$ est vraie sur une branche, l'une au moins des deux formules ${\displaystyle A}$ et ${\displaystyle B}$ en découle. Par conséquent on crée deux nouvelles branches et on ajoute ${\displaystyle A}$ sur l'une et ${\displaystyle 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.

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

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

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

Les deux branches sont fermées : en effet, la première contient ${\displaystyle a}$ et ${\displaystyle \neg a}$, et la seconde ${\displaystyle b}$ et ${\displaystyle \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 ${\displaystyle a}$ est une conséquence de ${\displaystyle (a\vee \neg b)\wedge b}$.

Si on part de l'ensemble de formules ${\displaystyle \{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ù ${\displaystyle a,b,c}$ sont interprétées par vrai, comme le montre la branche de droite qui ne peut être fermée.

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.

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

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

Pour les formules de type ${\displaystyle \delta }$, on utilise la skolémisation : on remplace ${\displaystyle x}$ par une constante fraîche ${\displaystyle c}$ dans ${\displaystyle 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 ${\displaystyle \gamma }$ plusieurs fois, en instanciant ${\displaystyle x}$ par des termes différents. Le tableau suivant montre que l'ensemble de formules ${\displaystyle \{\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.

Comme on le voit dans l'exemple précédent, il est nécessaire de deviner les termes qui instancient ${\displaystyle x}$ dans les règles ${\displaystyle \gamma }$ de façon à pouvoir fermer les branches. Du point de vue de la démonstration automatique, on ne peut évidemment pas instancier ${\displaystyle x}$ de façon exhaustive jusqu'à trouver les bons. À la place de cela, on remplace ${\displaystyle x}$ par ce que l'on va appeler une métavariable ${\displaystyle X}$, et c'est au moment où on cherchera à fermer les branches que l'on cherchera comment instancier ${\displaystyle 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 ${\displaystyle \delta }$, car en skolémisant, il faut prendre en compte les métavariables présentes. Par conséquent, on y instancie ${\displaystyle x}$ par ${\displaystyle f(Y_{1},\ldots ,Y_{n})}$ où ${\displaystyle 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 ${\displaystyle \{\forall x.~P(x),\exists x.~(\neg P(x)\vee \neg P(f(x)))\}}$

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

Comme on le voit dans le tableau précédent, il est parfois inutile d'appliquer une règle ${\displaystyle \gamma }$ (celle qui a produit ${\displaystyle P(X)}$). En général, il vaut mieux appliquer les règles ${\displaystyle \delta }$ avant, pour limiter le nombre de métavariables. De la même façon, il vaut mieux appliquer des règles autres que ${\displaystyle \beta }$ pour éviter de dupliquer le nombre de branches. Une stratégie possible est d'appliquer en priorité les règles ${\displaystyle \alpha }$, puis ${\displaystyle \delta }$, puis ${\displaystyle \beta }$ et enfin ${\displaystyle \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.