Resumen de Sistemas de tableau com unificação para lógicas modais
O método dos tableaux tem se mostrado bastante intuitivo embora ineficiente, em virtude da difficuldade em se controlar as instanciaçoes em lógicas de 1ª ordem. Estudos recentes comprovaram a eficiencia de provadores automáticos de teoremas baseados em tableau com a incorporação do algoritmo de unificação para a lógica clássica de 1ª ordem.
Neste artigo propomos um sistema de tableau para as lógicas modais K, T, D, K4 e S4 com a fórmula de Barcan utilizando o algoritmo de unificação no controle das instanciaçôes.
