Tableaux Sémantiques

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.