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) [10.1007/3-540-45616-3_9].

Tableau calculi for the logics of finite k-ary trees

FIORINO, GUIDO GIUSEPPE
2002

Abstract

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.
paper
intermediate logics; hypertableau calculi
English
Automated Reasoning with Analytic Tableaux and Related Methods
2002
Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2002, Copenhagen, Denmark, July 30 - August 1, 2002, Proceedings
3-540-43929-3
2002
115
129
none
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) [10.1007/3-540-45616-3_9].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/3617
Citazioni
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
Social impact