From Display to Labelled Proofs for Tense Logics

  • Agata Ciabattoni
  • Tim LyonEmail author
  • Revantha Ramanayake
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10703)


We introduce an effective translation from proofs in the display calculus to proofs in the labelled calculus in the context of tense logics. We identify the labelled calculus proofs in the image of this translation as those built from labelled sequents whose underlying directed graph possesses certain properties. For the basic normal tense logic \(\textsf {Kt}\), the image is shown to be the set of all proofs in the labelled calculus \(\textsf {G3Kt}\).


Display calculus Labelled calculus Structural proof theory Tense logic Modal logic 



Work supported by the FWF projects: START Y544-N23 and I 2982.


  1. 1.
    Belnap Jr., N.D.: Display logic. J. Philos. Logic 11(4), 375–417 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press, Cambridge (2001)CrossRefzbMATHGoogle Scholar
  3. 3.
    Brünnler. K.: Deep sequent systems for modal logic. In: Advances in Modal Logic, vol. 6, pp. 107–119. College Publications, London (2006)Google Scholar
  4. 4.
    Chagrov, A., Zakharyashchev, M.: Modal companions of intermediate propositional logics. Stud. Logica. 51(1), 49–82 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Ciabattoni, A., Ramanayake, R.: Power and limits of structural display rules. ACM Trans. Comput. Logic 17(3), 1–39 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Dyckhoff, R., Negri, S.: Proof analysis in intermediate logics. Arch. Math. Log. 51(1–2), 71–92 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Dyckhoff, R., Negri, S.: Geometrization of first-order logic. Bull. Symbolic Logic 21, 123–163 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Fitting, M.: Proof Methods for Modal and Intuitionistic Logics. Synthese Library, vol. 169. D. Reidel Publishing Co., Dordrecht (1983)CrossRefzbMATHGoogle Scholar
  9. 9.
    Fitting, M.: Prefixed tableaus and nested sequents. Ann. Pure Appl. Logic 163(3), 291–313 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Goré, R., Postniece, L., Tiu, A.: On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Log. Methods Comput. Sci. 7(2), 1–38 (2011). (2:8)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Goré, R., Ramanayake, R.: Labelled tree sequents, tree hypersequents and nested (deep) sequents. In: Advances in Modal Logic, vol. 9. College Publications, London (2012)Google Scholar
  12. 12.
    Greco, G., Ma, M., Palmigiano, A., Tzimoulis, A., Zhao, Z.: Unified correspondence as a proof-theoretic tool. J. Logic Comput. (2016, to appear).
  13. 13.
    Kashima, R.: Cut-free sequent calculi for some tense logics. Stud. Logica. 53(1), 119–135 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Kracht, M.: Power and weakness of the modal display calculus. In: Proof Theory of Modal Logic (Hamburg, 1993) Applied Logic Series, vol. 2, pp. 93–121. Kluwer Academic Publishers, Dordrecht (1996)Google Scholar
  15. 15.
    Lemmon, E.J., Scott, D.S.: The ‘Lemmon Notes’: An Introduction to Modal Logic. Blackwell, Oxford (1977)zbMATHGoogle Scholar
  16. 16.
    Mints, G.: Indexed systems of sequents and cut-elimination. J. Philos. Logic 26(6), 671–696 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Negri, S.: Proof analysis in modal logic. J. Philos. Logic 34(5–6), 507–544 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Ramanayake, R.: Inducing syntactic cut-elimination for indexed nested sequents. In: Proceedings of IJCAR, pp. 416–432 (2016)Google Scholar
  19. 19.
    Restall, G.: Comparing modal sequent systems.
  20. 20.
    Restall, G., Poggiolesi, F.: Interpreting and applying proof theory for modal logic. In: Restall, G., Russell, G. (eds.) New Waves in Philosophical Logic, pp. 39–62 (2012)Google Scholar
  21. 21.
    Viganò, L.: Labelled Non-Classical Logics. Kluwer Academic Publishers, Dordrecht (2000). With a foreword by Dov M. GabbayCrossRefzbMATHGoogle Scholar
  22. 22.
    Wansing, H.: Displaying Modal Logic. Trends in Logic-Studia Logica Library, vol. 3. Kluwer Academic Publishers, Dordrecht (1998)zbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  • Agata Ciabattoni
    • 1
  • Tim Lyon
    • 1
    Email author
  • Revantha Ramanayake
    • 1
  1. 1.Institut für ComputersprachenTechnische Universität WienWienAustria

Personalised recommendations