Skip to main content
SpringerLink
Log in

Linear Nested Sequents, 2-Sequents and Hypersequents

  • Conference paper
  • First Online:
Book cover Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 9323))

Abstract

We introduce the framework of linear nested sequent calculi by restricting nested sequents to linear structures. We show the close connection between this framework and that of 2-sequents, and provide linear nested sequent calculi for a number of modal logics as well as for intuitionistic logic. Furthermore, we explore connections to backwards proof search for sequent calculi and to the hypersequent framework, including a reinterpretation of various hypersequent calculi for modal logic S5 in the linear nested sequent framework.

Supported by FWF project START Y544-N23 and the European Union’s Horizon 2020 programme under the Marie Skłodowska-Curie grant agreement No 660047.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Avron, A.: The method of hypersequents in the proof theory of propositional non-classical logics. In: Hodges, W., Hyland, M., Steinhorn, C., Truss, J. (eds.) Logic: From Foundations to Applications, Clarendon (1996)

    Google Scholar 

  2. Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press (2001)

    Google Scholar 

  3. Brünnler, K.: Deep sequent systems for modal logic. Arch. Math. Log. 48, 551–577 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  4. Ciabattoni, A., Gabbay, D.M., Olivetti, N.: Cut-free proof systems for logics of weak excluded middle. Soft Computing 2(4), 147–156 (1999)

    Article  Google Scholar 

  5. Ciabattoni, A., Ferrari, M.: Hypertableau and path-hypertableau calculi for some families of intermediate logics. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol. 1847, pp. 160–174. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  6. Fitting, M.: Prefixed tableaus and nested sequents. Ann. Pure Appl. Logic 163(3), 291–313 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  7. Fitting, M.: Nested sequents for intuitionistic logics. Notre Dame Journal of Formal Logic 55(1), 41–61 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  8. Goré, R., Ramanayake, R.: Labelled tree sequents, tree hypersequents and nested (deep) sequents. In: Bolander, T., Braüner, T., Ghilardi, S., Moss, L.S. (eds.) AiML 9, pp. 279–299. College Publications (2012)

    Google Scholar 

  9. Kleene, S.C.: Introduction to Metamathematics. North-Holland, Amsterdam (1952)

    MATH  Google Scholar 

  10. Kurokawa, H.: Hypersequent calculus for intuitionistic logic with classical atoms. In: Artemov, S., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 318–331. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  11. Lahav, O.: From frame properties to hypersequent rules in modal logics. In: LICS 2013 (2013)

    Google Scholar 

  12. Lellmann, B.: Axioms vs hypersequent rules with context restrictions: Theory and applications. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 307–321. Springer, Heidelberg (2014)

    Google Scholar 

  13. Marin, S., Straßburger, L.: Label-free modular systems for classical and intuitionistic modal logics. In: Goré, R., Kooi, B.P., Kurucz, A. (eds.) AiML 10, pp. 387–406. College Publications (2014)

    Google Scholar 

  14. Martini, S., Masini, A.: A computational interpretation of modal proofs. In: Wansing, H. (ed.) Proof Theory of Modal Logic, pp. 213–241. Kluwer (1996)

    Google Scholar 

  15. Masini, A.: 2-sequent calculus: a proof theory of modalities. Ann. Pure Aplied Logic 58, 229–246 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  16. Masini, A.: 2-sequent calculus: Intuitionism and natural deduction. J. Log. Comput. 3(5), 533–562 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  17. Mints, G.: Sistemy lyuisa i sistema T (Supplement to the Russian translation). In: Feys, R. (ed.) Modal Logic, pp. 422–509. Nauka, Moscow (1974)

    Google Scholar 

  18. Negri, S.: Proof analysis in modal logic. J. Philos. Logic 34, 507–544 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  19. Poggiolesi, F.: A cut-free simple sequent calculus for modal logic S5. Rev. Symb. Log. 1(1), 3–15 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  20. Poggiolesi, F.: The method of tree-hypersequents for modal propositional logic. In: Makinson, D., Malinkowski, J., Wansing, H. (eds.) Towards Mathematical Philosophy. Trends in Logic, vol. 28, pp. 31–51. Springer (2009)

    Google Scholar 

  21. Poggiolesi, F.: Gentzen Calculi for Modal Propositional Logic. Trends in Logic, vol. 32. Springer (2010)

    Google Scholar 

  22. Pottinger, G.: Uniform, cut-free formulations of T, S4 and S5 (abstract). J. Symb. Logic 48(3), 900 (1983)

    Google Scholar 

  23. Ramanayake, R.: Non-commutative classical arithmetical sequent calculi are intuitionistic (2015), accepted for publication in the Special issue of the Logic Journal of the IGPL: ISRALOG’14 post-proceedings

    Google Scholar 

  24. Restall, G.: Proofnets for S5: sequents and circuits for modal logic. In: Dimitracopoulos, C., Newelski, L., Normann, D. (eds.) Logic Colloquium 2005. Lecture Notes in Logic, vol. 28, pp. 151–172. Cambridge University Press (2007)

    Google Scholar 

  25. Tatsuta, M.: Non-commutative first-order sequent calculus. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 470–484. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  26. Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, vol. 43. Cambridge University Press (2000)

    Google Scholar 

  27. Wansing, H.: Sequent systems for modal logics. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol, vol. 8, Springer (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Languages, TU Wien, Vienna, Austria

    Björn Lellmann

Authors
  1. Björn Lellmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Uniwersytet Wrocławski, Wrocław, Poland

    Hans De Nivelle

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Lellmann, B. (2015). Linear Nested Sequents, 2-Sequents and Hypersequents. In: De Nivelle, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2015. Lecture Notes in Computer Science(), vol 9323. Springer, Cham. https://doi.org/10.1007/978-3-319-24312-2_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-24312-2_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-24311-5

  • Online ISBN: 978-3-319-24312-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation