Une technique de recherche de preuve et de test de satisfiabilité qui décompose progressivement des formules logiques en composants le long d'un arbre (le tableau ou arbre de vérité), ferme les branches contenant des contradictions et construit ainsi soit un contre‑modèle à partir d'une branche ouverte, soit établit la validité lorsque toutes les branches sont fermées.

Principe

Appliquer des règles de décomposition syntaxiques aux formules pour explorer les affectations ou modèles possibles : décomposer conjonctions, disjonctions, quantificateurs et opérateurs modaux selon un ensemble de règles, suivre les conditions de branche, et utiliser des règles de fermeture et des contrôles de boucle ou d'équité pour assurer la terminaison lorsque cela est applicable.

Démonstration

Pour la logique propositionnelle, commencer par la négation de la formule à prouver et construire un tableau : scinder les disjonctions en branches alternatives, ajouter les conjonctes à la même branche et marquer une branche fermée lorsqu'elle contient à la fois p et non p. Une branche ouverte saturée fournit une valuation satisfaisante ; l'insatisfiabilité est attestée lorsque toutes les branches sont fermées.

Mauvaise application

Exécuter un tableau du premier ordre naïf sans mécanismes de blocage, de vérification de boucle ou de gestion des branches infinies puis prétendre disposer d'une procédure décidable ; ou traiter incorrectement les conditions de fermeture (par ex. ignorer des contraintes globales dans les tableaux modaux), conduisant à des faux positifs ou négatifs.

Conséquence

Les méthodes tableaux fournissent des preuves constructives ou des contre‑modèles, s'adaptent facilement à de nombreuses logiques (modale, temporelle, logiques de description) et fondent de nombreux moteurs de preuve automatisés et vérificateurs de satisfiabilité ; les performances pratiques dépendent de l'ordre des règles et de la gestion des branches.

Inversion

Remplacer la recherche par tableau par un calcul de réfutation tel que la résolution ou les calculs de séquents modifie la structure de recherche d'une construction de modèle en arbre vers une manipulation de clauses ou une élimination de coupures pilotée par buts, échangeant souvent la facilité d'extraction de modèles contre d'autres comportements en complexité/espace.

Limite

S'applique aux logiques classiques et à beaucoup de logiques non classiques mais l'exhaustivité et la terminaison exigent des jeux de règles spécifiques à la logique et parfois le blocage ou des stratégies d'équité ; la méthode ne garantit pas à elle seule des ressources polynomiales et peut produire un nombre exponentiel de branches.

Tension sémantique

Les tableaux privilégient la décomposition locale syntaxique et la construction explicite de modèles, en tension avec des méthodes globales comme la résolution ou les solveurs SMT qui transforment et combinent des clauses ou contraintes ; la tension porte sur l'extraction de modèles versus l'efficacité inférentielle centrée sur les clauses.

Synthèse

La méthode du tableau est une recherche syntaxique systématique en arbre qui décompose les formules pour exhiber une affectation satisfaisante ou fermer toutes les possibilités ; son adaptabilité à plusieurs logiques et son caractère constructif en font un outil pratique de raisonnement automatisé, contrebalancé par des problèmes de terminaison et de complexité de ramification.