Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

A Hypersequent Calculus with Clusters for Linear Frames

Abstract : The logic Kt4.3 is the basic modal language of linear frames. Along with its extensions, it is found at the core of linear-time temporal logics and logics on words. In this paper, we consider the problem of designing proof systems for these logics, in such a way that proof search yields decision procedures for validity with an optimal complexity—coNP in this case. In earlier work, Indrzejczak has proposed an ordered hypersequent calculus that is sound and complete for Kt4.3 but does not yield any decision procedure. We refine his approach, using a hypersequent structure that corresponds to weak rather than strict total orders, and using annotations that reflect the model-theoretic insights given by small models for Kt4.3. We obtain a sound and complete calculus with an associated coNP proof search algorithm. These results extend naturally to the cases of unbounded and dense frames.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/hal-01756126
Contributor : Sylvain Schmitz Connect in order to contact the contributor
Submitted on : Saturday, March 31, 2018 - 7:54:08 PM
Last modification on : Thursday, July 2, 2020 - 5:26:02 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01756126, version 1

Citation

David Baelde, Anthony Lick, Sylvain Schmitz. A Hypersequent Calculus with Clusters for Linear Frames. 2018. ⟨hal-01756126v1⟩

Share

Metrics

Record views

141

Files downloads

48