We present tableau calculi for the logics D k (k≥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 D k, in particular their constructivity and their decidability.
Tableau calculi for the logics of finite k-ary trees / M. Ferrari, C. Fiorentini, G. Fiorino - In: Automated reasoning with analytic tableaux and related methods : international conference, TABLEAUX 2002 : Copenhagen, Denmark, july 30-august 1, 2002 : proceedings / [a cura di] U. Egly, C.G. Fermüller. - Berlin : Springer, 2002. - ISBN 3540439293. - pp. 115-129 (( convegno International Conference on Automated Reasoning with Analytic Tableaux and Related Methods tenutosi a Copenhagen nel 2002 [10.1007/3-540-45616-3_9].
Tableau calculi for the logics of finite k-ary trees
C. Fiorentini;
2002
Abstract
We present tableau calculi for the logics D k (k≥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 D k, in particular their constructivity and their decidability.
| File | Dimensione | Formato | |
|---|---|---|---|
|
2002_tableaux.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
262.49 kB
Formato
Adobe PDF
|
262.49 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
