## [Método de Tableaux](/es/node/59201) Definición Una técnica de búsqueda de pruebas y de prueba de satisfacibilidad que descompone incrementalmente fórmulas lógicas en componentes a lo largo de un árbol (el tableau o árbol de verdad), cerrando ramas que contienen contradicciones y, de este modo, construyendo un contra‑modelo a partir de una rama abierta o estableciendo la validez cuando todas las ramas se cierran. ## Principio Principio Aplicar reglas de descomposición sintáctica a las fórmulas para explorar asignaciones o modelos posibles: descomponer conjunciones, disyunciones, cuantificadores y operadores modales según conjuntos de reglas, registrar condiciones por rama y usar reglas de cierre y controles de bucle o equidad para asegurar la terminación cuando sea aplicable. ## Demostración Demostración En lógica proposicional, comenzar con la negación de la fórmula a probar y construir un tableau: dividir disyunciones en ramas alternativas, añadir los conjunctos a la misma rama y marcar una rama como cerrada cuando contiene p y no p. Una rama abierta saturada proporciona una asignación satisfactoria; la insatisfacibilidad queda acreditada cuando todas las ramas se cierran. ## Aplicación incorrecta Aplicación incorrecta Ejecutar un tableau de primer orden ingenuo sin bloqueo, comprobación de bucles o mecanismos para tratar ramas infinitas y afirmar que se dispone de un procedimiento de decisión; o tratar incorrectamente las condiciones de cierre (por ejemplo, ignorar restricciones globales en tableaux modales) lo que conduce a falsos positivos o negativos. ## Consecuencia Consecuencia Los métodos de tableau proporcionan pruebas constructivas o contra‑modelos, se adaptan con facilidad a muchas lógicas (modal, temporal, lógicas de descripción) y fundamentan muchos demostradores automáticos y comprobadores de satisfacibilidad; el rendimiento práctico depende del orden de aplicación de reglas y de la gestión de ramas. ## Inversión Inversión Sustituir la búsqueda por tableau por un cálculo de refutación como la resolución o los cálculos de secuentes cambia la estructura de búsqueda de construcción de modelos en árbol a manipulación de cláusulas o eliminación de cortes dirigida por objetivos, intercambiando a menudo la facilidad de extracción de modelos por otros comportamientos en complejidad/espacio. ## Límite Límite Se aplica a las lógicas clásicas y a muchas no clásicas, pero la completitud y la terminación requieren conjuntos de reglas específicas de la lógica y a veces bloqueo o estrategias de equidad; por sí sola no garantiza recursos polinomiales y puede generar un número exponencial de ramas. ## Tensión semántica Tensión semántica Los tableaux enfatizan la descomposición sintáctica local y la construcción explícita de modelos, lo que compite con métodos globales como la resolución o los solve‑res SMT que transforman y combinan cláusulas o restricciones; la tensión está entre extracción de modelos y eficiencia inferencial centrada en cláusulas. ## Síntesis Síntesis El método de tableau es una búsqueda sintáctica sistemática en árbol que descompone fórmulas para exhibir una asignación satisfactoria o cerrar todas las posibilidades; su adaptabilidad a múltiples lógicas y su carácter constructivo lo convierten en una herramienta práctica de razonamiento automatizado, compensada por cuestiones de terminación y complejidad de ramificación.