zbMATH — the first resource for mathematics

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].

03B45 Modal logic (including the logic of norms)
03F03 Proof theory, general (including proof-theoretic semantics)
03F20 Complexity of proofs