On the Tree-Hypersequent Calculi

  • Francesca PoggiolesiEmail author
Part of the Trends in Logic book series (TREN, volume 32)


In the first part of the book we defined what it means for a sequent calculus to be good and we explained the reasons why it is important for a logic to have a good Gentzen calculus. In the second part of the book we set out the numerous attempts made at providing the main systems of modal logic with a proof calculus while showing their limits and their benefits. Our aim in this last part of the book is to present and deeply analyse a new method for generating good extensions of the sequent calculus for the SLH-systems plus GL.


  1. 3.
    A. Avron. A constructive analysis of RM. Journal of Symbolic Logic, 52:939–951, 1987.CrossRefGoogle Scholar
  2. 5.
    A. Avron. Using hypersequents in proof systems for non-classical logics. Annals of Mathematics and Artificial Intelligence, 4:225–248, 1991.CrossRefGoogle Scholar
  3. 7.
    M. Baaz and R. Zach. Hypersequents and cut elimination for intuitionistic fuzzy logic. In G. Peter and H. Schwichtenberg, editors, 14th International Workshop, CSL 2000. Fischbachau, Germany, August 21–26, 2000. Proceedings, pp. 187–201. Springer, Berlin, 2000.Google Scholar
  4. 15.
    K. Brünnler. Deep sequent systems for modal logic. In G. Governatori, I. Hodkinson, and Y. Venema, editors, Advances in Modal Logic, Vol 6, pp. 107–119. College Publications, London, 2006.Google Scholar
  5. 16.
    K. Brünnler and L. Strassburger. Modular sequent systems for modal logic. In M. Giese and A Waaler, editors, Proceeding of Tableaux 2009, LNAI 5607, pp. 152–166. Springer, Berlin-Heidelberg, 2009.Google Scholar
  6. 25.
    A. Ciabattoni. Hypersequent calculi for some intermediate logics with bounded Kripke models. Journal of Logic and Computation, 11:283–294, 2001.CrossRefGoogle Scholar
  7. 55.
    I. Hasuo and R. Kashima. Kripke completeness of first-order constructive logics with strong negation. Logic Journal of the IGPL, 11:615–646, 2003.CrossRefGoogle Scholar
  8. 60.
    B. Hill and F. Poggiolesi. A contraction-free and cut-free sequent calculus for propositional dynamic logic. Studia Logica, 94:68–94, 2010.CrossRefGoogle Scholar
  9. 66.
    R. Ishigaki and K. Kikuchi. Tree-sequent method for subintuitionistic predicate logics. Proceedings of the 16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, LNAI, 4548:149–164, 2007.CrossRefGoogle Scholar
  10. 68.
    R. Kashima. Cut-free sequent calculi for some tense logics. Studia Logica, 53:119–135, 1994.CrossRefGoogle Scholar
  11. 78.
    G. Metcalfe, N. Olivetti, and D. M. Gabbay. Sequent and hypersequent calculi for Abelian and Lukasiewicz logics. ACM Transaction on Computational Logic (TOCL), 1:691–746, 1991.Google Scholar
  12. 100.
    F. Poggiolesi. The method of tree-hypersequent for modal propositional logic. In D. Makinson, J. Malinowski, and H. Wansing, editors, Towards Mathematical Philosophy, pp. 31–51. Springer, Berlin, 2008.Google Scholar
  13. 102.
    F. Poggiolesi. Sequent Calculi for Modal Logic. Ph.D. Thesis, Florence/ Paris, 2008.Google Scholar
  14. 103.
    F. Poggiolesi. A purely syntactic and cut-free sequent calculus for the modal logic of provability. Review of Symbolic Logic, 2:593–611, 2009.CrossRefGoogle Scholar
  15. 105.
    F. Poggiolesi. Reflecting the semantic features of S5 at the syntactic level. In C. Sinigaglia and M. D’Agostino, editors, Proceedings of SILFS Conference. College Publications, London, forthcoming.Google Scholar
  16. 106.
    G. Pottinger. Uniform cut-free formulations of T, S4 and S5 (abstract). Journal of Symbolic Logic, 48:900, 901, 1983.Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2010

Authors and Affiliations


Personalised recommendations