Display to Labeled Proofs and Back Again for Tense Logics

From International Center for Computational Logic

Toggle side column

Display to Labeled Proofs and Back Again for Tense Logics

Agata CiabattoniAgata Ciabattoni,  Tim LyonTim Lyon,  Revantha RamanayakeRevantha Ramanayake,  Alwen TiuAlwen Tiu
Display to Labeled Proofs and Back Again for Tense Logics


Agata Ciabattoni, Tim Lyon, Revantha Ramanayake, Alwen Tiu
Display to Labeled Proofs and Back Again for Tense Logics
ACM Transactions on Computational Logic, 22(3):1-31, August 2021
  • KurzfassungAbstract
    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. The latter, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics.
  • Weitere Informationen unter:Further Information: Link
  • Forschungsgruppe:Research Group: Computational LogicComputational Logic
@article{CLRT2021,
  author    = {Agata Ciabattoni and Tim Lyon and Revantha Ramanayake and Alwen
               Tiu},
  title     = {Display to Labeled Proofs and Back Again for Tense Logics},
  journal   = {ACM Transactions on Computational Logic},
  volume    = {22},
  number    = {3},
  publisher = {Association for Computing Machinery},
  year      = {2021},
  month     = {August},
  pages     = {1-31},
  doi       = {10.1145/3460492}
}