Une procédure de preuve par réfutation qui décompose des formules logiques en un arbre de composants plus simples (un tableau ou arbre de vérité) pour tester la satisfaisabilité ; un tableau fermé (toutes les branches contradictoires) montre l'insatisfaisabilité de la formule racine.

Principe

Appliquer systématiquement des règles de décomposition qui reflètent les conditions sémantiques des connecteurs et quantificateurs, en développant les branches jusqu'à ce qu'elles se ferment par contradiction ou restent ouvertes comme témoins de satisfaisabilité.

Démonstration

Pour tester ¬(A ∧ B), placer sa négation à la racine, appliquer la décomposition de la négation et de la conjonction pour produire des branches ; si chaque branche contient une formule et sa négation, le tableau se ferme, montrant que l'énoncé original est valide.

Mauvaise application

Arrêter le développement trop tôt, mal appliquer des règles de bifurcation ou ne pas instancier correctement les quantificateurs (surtout universels) peut laisser des branches ouvertes suggérant à tort la satisfaisabilité ou une fermeture non valable.

Conséquence

Exécutés correctement, les tableaux fournissent des contre-modèles à partir des branches ouvertes et des réfutations compactes à partir des tableaux fermés, ce qui les rend utiles en raisonnement automatique et pour extraire des contre-exemples diagnostiques.

Inversion

La perspective inverse est un système de preuve qui construit des dérivations syntaxiques (p. ex. Hilbert ou la déduction naturelle) plutôt que de chercher des contre-modèles sémantiques ; les tableaux privilégient la recherche de modèles.

Limite

Particulièrement adaptés aux logiques propositionnelle et du premier ordre ; les tableaux du premier ordre exigent des stratégies avec variables libres ou skolemisation pour représenter les témoins, et sans restrictions la recherche peut ne pas terminer.

Tension sémantique

Tension avec la résolution et les calculs axiomatiques : les tableaux sont orientés recherche de modèles et tendent à produire des contre-modèles, tandis que la résolution se concentre sur la réfutation par unification et génération de résolvantes.

Synthèse

Les tableaux sémantiques sont une méthode de décision/recherche en arbre qui décompose les formules par des règles sémantiques ; les motifs de fermeture des branches déterminent la satisfaisabilité et fournissent des contre-modèles ou des réfutations explicites.