Tableaux Semánticos

Un procedimiento de prueba por refutación que descompone fórmulas lógicas en un árbol de componentes más simples (un tableau o árbol de verdad) para comprobar satisfacibilidad; un tableau cerrado (todas las ramas contradictorias) muestra la insatisfacibilidad de la fórmula raíz.