Une technique sémantique et exhaustive pour les formules propositionnelles qui énumère toutes les attributions possibles de valeurs de vérité aux propositions atomiques et évalue la formule sous chaque attribution pour déterminer validité, satisfaisabilité ou équivalence.

Principe

Considérer de façon exhaustive chaque valuation des atomes propositionnels ; une formule est valide si elle est vraie sous toutes les valuations, satisfaisable si elle est vraie pour au moins une, et équivalente à une autre si leurs valeurs coïncident pour chaque valuation.

Démonstration

Pour montrer que A → B est une tautologie, construire une table listant toutes les combinaisons de valeurs pour A et B, calculer A → B ligne par ligne et vérifier que chaque entrée est vraie.

Mauvaise application

Employer les tables de vérité en logique avec domaines infinis ou non bornés (premier ordre avec quantificateurs) sans réduction finie, ou les appliquer à des formules avec trop d'atomes, mène à une computation irréalisable et à des conclusions erronées sur la faisabilité.

Conséquence

Les tables de vérité donnent des réponses décisives et indépendantes du modèle pour les problèmes propositionnels, sont simples à mettre en œuvre et à enseigner, et fournissent des contre-exemples clairs (lignes) attestant la non-validité ou la non-équivalence.

Inversion

L'approche inverse est symbolique ou proof-théorique : utiliser des calculs déductifs (résolution, tableaux, déduction naturelle) pour manipuler symboliquement les formules au lieu d'énumérer les valuations, échangeant décidabilité contre évolutivité.

Limite

Limitée à la logique propositionnelle ou à des fragments décidables où le nombre d'atomes propositionnels est réduit ; impraticable pour de grandes formules propositionnelles et non applicable directement à la logique du premier ordre sans hypothèses de finitude.

Tension sémantique

En tension avec des calculs algorithmiques comme la résolution : les tables sont exhaustives et simples mais subissent une explosion combinatoire, tandis que la résolution et les tableaux cherchent à éviter l'énumération complète par inférence symbolique et stratégies de recherche.

Synthèse

La méthode des tables de vérité est un test sémantique exhaustif pour les formules propositionnelles qui évalue chaque valuation pour produire des jugements définitifs sur validité, satisfaisabilité et équivalence, au prix d'une croissance exponentielle selon le nombre d'atomes.