Display to Labeled Proofs and Back Again for Tense Logics
From MaRDI portal
Publication:5034228
DOI10.1145/3460492zbMATH Open1505.03047arXiv1911.02289OpenAlexW3175155954WikidataQ113772971 ScholiaQ113772971MaRDI QIDQ5034228
Revantha Ramanayake, Alwen Tiu, Agata Ciabattoni, Tim S. Lyon
Publication date: 24 February 2022
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Abstract: We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to a derivation in the associated display calculus. A key insight in this converse translation is a canonical representation of display sequents as labeled polytrees. Labeled polytrees, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics.
Full work available at URL: https://arxiv.org/abs/1911.02289
Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Temporal logic (03B44)
Related Items (1)
This page was built for publication: Display to Labeled Proofs and Back Again for Tense Logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5034228)
