The strong completeness of the tableau method

- Statement of Responsibility:
-
Fernández Díez, Gustavo
- Hlavní autor:
- Formát:
-
Journal article
- Jazyk:
-
English
- Forma / Žánr:
-
text (article)
- Vydáno:
-
Universidad de León: Servicio de Publicaciones 1998
- V:
-
Contextos ISSN 0212-6192 Nº 31-32, 1998, pags. 297-308
- Předmětová hesla:
- Annotation:
-
for the predicate calculus as to obtain a direct proof (without using compactness) of the fact that the most user-friendly formal method of deduction, the Beth-Smullyan method of first-order tableaux, is similarly complete, in the sense that if a formula . is a first-order consequence of an arbitrary set �³ of formulas, there is a finite subset �³0 of �³ such that the set �³0 �¾ { �Ê. } generates a closed tableau. Also, an incidental remark will be made concerning the monotony of the method of tableaux, on a problem which has led to a technical mistake in some of the published literature.