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

#### 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.
##### Scheda breve Scheda completa Scheda completa (DC)
paper
intermediate logics; hypertableau calculi
English
Automated Reasoning with Analytic Tableaux and Related Methods
3-540-43929-3
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].
Ferrari, M; Fiorentini, C; Fiorino, G
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`
• 0
• ND