Méthode des tableaux

vignette|200px|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. 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.