On the Decidability of Certain Semi-Lattice Based Modal Logics

摘要

Sequent calculi are proof systems that are exceptionally suitable for proving the decidability of a logic. Several relevance logics were proved decidable using a technique attributable to Curry and Kripke. Further enhancements led to a proof of the decidability of implicational ticket entailment by Bimbo and Dunn in [12,13]. This paper uses a different adaptation of the same core proof technique to prove a group of positive modal logics (with disjunction but no conjunction) decidable.