DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2018.15

A Hypersequent Calculus with Clusters for Tense Logic over Ordinals

Authors: David Baelde, Anthony Lick, and Sylvain Schmitz

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract

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.

Cite as

David Baelde, Anthony Lick, and Sylvain Schmitz. A Hypersequent Calculus with Clusters for Tense Logic over Ordinals. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{baelde_et_al:LIPIcs.FSTTCS.2018.15,
  author =	{Baelde, David and Lick, Anthony and Schmitz, Sylvain},
  title =	{{A Hypersequent Calculus with Clusters for Tense Logic over Ordinals}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{15:1--15:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.15},
  URN =		{urn:nbn:de:0030-drops-99143},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.15},
  annote =	{Keywords: modal logic, proof system, hypersequent}
}

Search Results

Documents authored by Lick, Anthony

A Hypersequent Calculus with Clusters for Tense Logic over Ordinals

Abstract

Cite as

Thanks for your feedback!

Could not send message