The strong completeness of the tableau method
ISSN: 0212-6192
Année de publication: 1998
Número: 31-32
Pages: 297-308
Type: Article
D'autres publications dans: Contextos
Résumé
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.