The strong completeness of the tableau method
ISSN: 0212-6192
Año de publicación: 1998
Número: 31-32
Páginas: 297-308
Tipo: Artículo
Otras publicaciones en: Contextos
Resumen
En este trabajo se describe una prueba directa (sin usar el teorema de compacidad) del hecho de que el metodo de arboles o tablas semanticas de primer orden es completo en el sentido fuerte, es decir: que si una formula . es una consecuencia de primer orden de un conjunto arbitrario de formulas �³ (no necesariamente contable), entonces existe un subconjunto finito �³0 de �³ tal que el conjunto �³0 �¾ { �Ê. } genera una tabla cerrada. Ademas, se hara una observacion incidental sobre un aspecto de la monotonia del metodo de tablas que ha dado lugar a algun error en la literatura publicada.