Método de Tableaux

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.