文章基本信息

标题：A Hypersequent Calculus with Clusters for Tense Logic over Ordinals
本地全文：下载
作者：David Baelde ; Anthony Lick ; Sylvain Schmitz 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：122
页码：1-19
DOI：10.4230/LIPIcs.FSTTCS.2018.15
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Prior's tense logic forms the core of linear temporal logic, with both past- and future-looking modalities. We present a sound and complete proof system for tense logic over ordinals. Technically, this is a hypersequent system, enriched with an ordering, clusters, and annotations. The system is designed with proof search algorithms in mind, and yields an optimal coNP complexity for the validity problem. It entails a small model property for tense logic over ordinals: every satisfiable formula has a model of order type at most omega^2. It also allows to answer the validity problem for ordinals below or exactly equal to a given one.
关键词：modal logic; proof system; hypersequent