We present tableau calculi for the logics $\gdj_k$ ($k\geq 2$) semantically characterized by the classes of Kripke models built on finite $k$-ary trees. Our tableau calculi use the signs $\T$ and $\F$, some tableau rules for Intuitionistic Logic and two rules formulated in a hypertableau fashion. We prove the Soundness and Completeness Theorems for our calculi. Finally, we use them to prove the main properties of the logics $\gdj_k$, in particular their constructivity and their decidability.
Ferrari, M., Fiorentini, C., & Fiorino, G. (2002). Tableau calculi for the logics of finite k-ary trees. In Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2002, Copenhagen, Denmark, July 30 - August 1, 2002, Proceedings (pp.115-129).
Citazione: | Ferrari, M., Fiorentini, C., & Fiorino, G. (2002). Tableau calculi for the logics of finite k-ary trees. In Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2002, Copenhagen, Denmark, July 30 - August 1, 2002, Proceedings (pp.115-129). |
Tipo: | paper |
Carattere della pubblicazione: | Scientifica |
Titolo: | Tableau calculi for the logics of finite k-ary trees |
Autori: | Ferrari, M; Fiorentini, C; Fiorino, G |
Autori: | |
Data di pubblicazione: | 2002 |
Lingua: | English |
Nome del convegno: | Automated Reasoning with Analytic Tableaux and Related Methods |
ISBN: | 3-540-43929-3 |
Appare nelle tipologie: | 02 - Intervento a convegno |