Author_Institution :
Sch. of Comput. Sci., Tel Aviv Univ., Tel Aviv, Israel
Abstract :
We provide a general method for generating cutfree and/or analytic hypersequent Gentzen-type calculi for a variety of normal modal logics. The method applies to all modal logics characterized by Kripke frames, transitive Kripke frames, or symmetric Kripke frames satisfying some properties, given by first-order formulas of a certain simple form. This includes the logics KT, KD, S4, S5, K4D, K4.2, K4.3, KBD, KBT, and other modal logics, for some of which no Gentzen calculi was presented before. Cut-admissibility (or analyticity in the case of symmetric Kripke frames) is proved semantically in a uniform way for all constructed calculi. The decidability of each modal logic in this class immediately follows.
Keywords :
calculus; decidability; theorem proving; Gentzen calculi; K4.2 modal logic; K4.3 modal logic; K4D modal logic; KBD modal logic; KBT modal logic; KD modal logic; KT modal logic; S4 modal logic; S5 modal logic; analytic hypersequent Gentzen-type calculi; constructed calculi; cut-admissibility; cutfree hypersequent Gentzen-type calculi; decidability; first-order formulas; frame property; hypersequent rules; normal modal logics; symmetric Kripke frames; transitive Kripke frames; Calculus; Computer science; Context; Educational institutions; Semantics; Standards; Syntactics; cut-admissibility; frame properties; hypersequent calculi; modal logic; proof theory;
