Méthode des tableaux

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Représentation graphique d'un tableau propositionnel partiellement construit

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.

Introduction[modifier | modifier le code]

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 est 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 destructurer 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[modifier | modifier le code]

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

Règles[modifier | modifier le code]

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 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 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[modifier | modifier le code]

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 :

Prop-tableau-1.svg

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

Prop-tableau-2.svg

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

Prop-tableau-3.svg

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 :

Prop-tableau-4.svg

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 :

Non-closed propositional tableau.svg

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[modifier | modifier le code]

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

Première approche[modifier | modifier le code]

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.

First-order tableau.svg

Métavariables et unification[modifier | modifier le code]

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)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)))\}

First-order tableau with metavariables.svg

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

Stratégies[modifier | modifier le code]

Comme on le voit dans le tableau précédant, 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[modifier | modifier le code]

  • 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é ».