A hypersequent calculus with clusters for linear frames.

*(English)*Zbl 1418.03066
Bezhanishvili, Guram (ed.) et al., Advances in modal logic. Vol. 12. Proceedings of the 12th conference (AiML 2018), Bern, Switzerland, August 27–31, 2018. London: College Publications. 43-62 (2018).

Summary: The logic K\(_{\mathbf{t}}\)4.3 is the basic modal logic 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 K\( _{\mathbf{t}}\)4.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 K\(_{\mathbf{t}}\)4.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, and to the complexity of the two-variable fragment of first-order logic over total orders.

For the entire collection see [Zbl 1398.03005].

For the entire collection see [Zbl 1398.03005].