Hypersequent rules with restricted contexts for propositional modal logics

详细信息    查看全文

• 作者：Bjö ; rn Lellmann ^{lellmann@logic.at}
• 关键词：Structural proof theory ; Hypersequents ; Modal logic ; Hilbert axioms ; Cut elimination ; Decidability
• 刊名：Theoretical Computer Science
• 出版年：2016
• 出版时间：20 December 2016
• 年：2016
• 卷：656
• 期：part_PA
• 页码：76-105
• 全文大小：853 K
• 卷排序：656

文摘

As part of a general research programme into the expressive power of different generalisations of the sequent framework we investigate hypersequent calculi given by rules of the newly introduced format of hypersequent rules with context restrictions. The introduced rule format is used to prove uniform syntactic cut elimination, decidability and complexity results. We also introduce transformations between hypersequent rules of this format and Hilbert axioms, entailing a result about the limits of such rules. As case studies, we apply our methods to several modal logics and obtain e.g. a complexity-optimal decision procedure for the logic S5S5 and new calculi for the logic K4.2K4.2 as well as combinations of modal logics in the form of simply dependent bimodal logics.