From Frame Properties to Hypersequent Rules in Modal Logics

Author

Lahav, Orly

Author_Institution

Sch. of Comput. Sci., Tel Aviv Univ., Tel Aviv, Israel

fYear

2013

fDate

25-28 June 2013

Firstpage

408

Lastpage

417

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Logic in Computer Science (LICS), 2013 28th Annual IEEE/ACM Symposium on

Conference_Location

New Orleans, LA

ISSN

1043-6871

Print_ISBN

978-1-4799-0413-6

Type

conf

DOI

10.1109/LICS.2013.47

Filename

6571573