A uniform tableau method for intuitionistic modal logics I |
| |
Authors: | Giambattista Amati Fiora Pirri |
| |
Institution: | (1) Fondazione Ugo Bordoni, via Baldassarre Castiglione 59, 00142 Roma, Italy;(2) Dip. di Informatica e Sistemistica, Università di Roma La Sapienza, via Salaria 113, 00198 Roma, Italy |
| |
Abstract: | We present tableau systems and sequent calculi for the intuitionistic analoguesIK, ID, IT, IKB, IKDB, IB, IK4, IKD4, IS4, IKB4, IK5, IKD5, IK45, IKD45 andIS5 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 forIK, ID, IT, IKB, IKDB, IB, IK4, IKD4, IS4, IKB4, IK5, IK45 andIS5. We also investigate the relationship of these logics with some other intuitionistic modal logics proposed in the literature.Work carried out in the framework of the agreement between the Italian PT Administration and the Fondazione Ugo Bordoni.Presented byDov Gabbay |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|