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.

Principio

Aplicar sistemáticamente reglas de descomposición que reflejen las condiciones semánticas de los conectivos y cuantificadores, expandiendo ramas hasta que se cierren por contradicción o permanezcan abiertas como testigos de satisfacción.

Demostración

Para evaluar ¬(A ∧ B), coloca su negación en la raíz, aplica la descomposición de negación y conjunción para producir ramas; si cada rama contiene una fórmula y su negación, el tableau se cierra y demuestra la validez del original.

Aplicación incorrecta

Interrumpir la expansión prematuramente, aplicar mal las reglas de división de ramas o no instanciar correctamente cuantificadores (especialmente universales) puede dejar ramas abiertas que sugieran erróneamente satisfacibilidad o cerrar indebidamente.

Consecuencia

Bien ejecutados, los tableaux proporcionan contraejemplos a partir de ramas abiertas y refutaciones compactas a partir de tableaux cerrados, siendo prácticos para razonamiento automatizado y extracción de contraejemplos diagnósticos.

Inversión

La perspectiva inversa es un sistema que construye derivaciones sintácticas (p. ej. Hilbert o deducción natural) en lugar de buscar contraejemplos semánticos; los tableaux enfatizan la búsqueda de modelos.

Límite

Más naturales para lógicas proposicionales y de primer orden; los tableaux de primer orden requieren estrategias con variables libres o skolemización para representar testigos, y sin restricciones la búsqueda puede no terminar.

Tensión semántica

Existe tensión con la resolución y los cálculos axiomáticos: los tableaux están orientados a la búsqueda de modelos y tienden a producir contraejemplos, mientras que la resolución se centra en la refutación de cláusulas mediante unificación y generación de resolventes.

Síntesis

Los tableaux semánticos son un método de búsqueda/decisión basado en árboles que descompone fórmulas por reglas semánticas; los patrones de cierre de ramas deciden la satisfacibilidad y ofrecen contraejemplos o refutaciones explícitas.