We present tableau systems and sequent calculi for the intuitionistic analogues IK, ID, IT, IKB, IKDB, IB, IK4, IKD4, IS4, IKB4, IK5, IKD5, IK45, IKD45 and IS5 of the normal classical modal logics. We provide soundness and completeness theorems with respect to the models of intuitionistic logic enriched by a modal accessibility relation, as proposed by G. Fischer Servi. We then show the disjunction property for IK, ID, IT, IKB, IKDB, IB, IK4, IKD4, IS4, IKB4, IK5, IK45 and IS5. We also investigate the relationship of these logics with some other intuitionistic modal logics proposed in the literature. © 1994 Kluwer Academic Publishers.
A uniform tableau method for intuitionistic modal logics I / Gianni, Amati; PIRRI ARDIZZONE, Maria Fiora. - In: STUDIA LOGICA. - ISSN 0039-3215. - STAMPA. - 53:1(1994), pp. 29-60. [10.1007/bf01053021]
A uniform tableau method for intuitionistic modal logics I
PIRRI ARDIZZONE, Maria Fiora
1994
Abstract
We present tableau systems and sequent calculi for the intuitionistic analogues IK, ID, IT, IKB, IKDB, IB, IK4, IKD4, IS4, IKB4, IK5, IKD5, IK45, IKD45 and IS5 of the normal classical modal logics. We provide soundness and completeness theorems with respect to the models of intuitionistic logic enriched by a modal accessibility relation, as proposed by G. Fischer Servi. We then show the disjunction property for IK, ID, IT, IKB, IKDB, IB, IK4, IKD4, IS4, IKB4, IK5, IK45 and IS5. We also investigate the relationship of these logics with some other intuitionistic modal logics proposed in the literature. © 1994 Kluwer Academic Publishers.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.