Labelled Systems in Modal Logics

  • Andrzej IndrzejczakEmail author
Part of the Trends in Logic book series (TREN, volume 30)


One of the most important nonstandard approaches to formalization of modal logics is based on the application of labels. This technique is connected not only with modal logics but has a really wide scope of application in several branches of logic. In modal logic labels extend a language with a representation of states in a model. Their addition considerably increase the flexibility of expression.


Modal Logic Temporal Logic Inference Rule Deductive System Hybrid Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [186]
    Massacci, F. 1998. Single step tableaux for modal logics: Methodology, computations, algorithms. Technical Report TR-04, Dipartimento di Informatica e Sistemistica, Universita di Roma “La Sapienza”.Google Scholar
  2. [182]
    Marx, M., S. Mikulas, and S. Schlobach. 1999. Tableau calculus for local cubic modal logic and it’s implementation. Logic Journal of the IGPL 7(6): 755–778.CrossRefGoogle Scholar
  3. [288]
    Zeman, J.J. 1973. Modal logic. Oxford: Oxford University Press.Google Scholar
  4. [99]
    Gabbay, D. 1996. LDS-labelled deductive systems. Oxford: Clarendon Press.Google Scholar
  5. [117]
    Goré, R. 1999. Tableau methods for modal and temporal logics. In Handbook of tableau methods, eds. M. D’Agostino et al., 297–396. Dordrecht: Kluwer Academic Publishers.Google Scholar
  6. [93]
    Fitting, M. 1983. Proof methods for modal and intuitionistic logics. Dordrecht; Rei-del.Google Scholar
  7. [191]
    Mints, G. 1997. Indexed systems of sequents and cut-elimination. Journal of Philosophical Logic 26: 671–696.CrossRefGoogle Scholar
  8. [3]
    Aho, A.V., and J.D. Ullman. 1995. Foundations of computer science. New York: W.H. Freeman and CO.Google Scholar
  9. [183]
    Marx, M., S. Mikulas, and M. Reynolds. 2000. The mosaic method for temporal logics. In Automated reasoning with analytic tableaux and related methods, ed. R. Dyckhoff, Proc. of International Conference TABLEAUX 2000, Saint Andrews, Scotland, LNAI 1847, 324–340. New York: Springer.Google Scholar
  10. [287]
    Vigano, L. 2000. Labelled non-classical logics. Dordrecht: Kluwer.Google Scholar
  11. [33]
    Blackburn, P. 2000. Representation, reasoning, and relational structures: A hybrid logic manifesto. Logic Journal of the IGPL 8(3): 339–365.CrossRefGoogle Scholar
  12. [5]
    Anderson, A., and N.D. Belnap, Jr. 1975. Entailment: The logic of relewance and necessity, vol I. Princeton: Princeton University Press.Google Scholar
  13. [142]
    Indrzejczak, A. 1996. Cut-free sequent calculus for S5. Bulletin of the Section of Logic 25(2): 95–102.Google Scholar
  14. [17]
    Avron, A., F. Honsell, M. Miculan, and C. Paravano. 1998. Encoding modal logics in logical frameworks. Studia Logica 60: 161–202.CrossRefGoogle Scholar
  15. [22]
    Basin, D., S. Matthews, and L. Vigano. 1998. Natural deduction for non-classical logics. Studia Logica 60: 119–160.CrossRefGoogle Scholar
  16. [185]
    Massacci, F. 1994. Strongly analytic tableaux for normal modal logics. In Proc. CADE-12, ed. A. Bundy, LNAI 814: 723–737. New York: Springer.Google Scholar
  17. [42]
    Blamey, S., and L. Humberstone. 1991. A perspective on modal sequent logic. Publications of the Research Institute for Mathematical Sciences, Kyoto University 27: 763–782.CrossRefGoogle Scholar
  18. [119]
    Hähnle, R. 1994. Automated deduction in multiple-valued logics. Oxford: Oxford University Press.Google Scholar
  19. [154]
    Indrzejczak, A. 2007. Labelled tableau calculi for weak modal logics. Bulletin of the Section of logic 36(3–4): 159–173.Google Scholar
  20. [231]
    Rescher, N., and A. Urquhart. 1971. Temporal logic. New York: Springer-Verlag.Google Scholar
  21. [230]
    Renteria, C., and E. Hausler. 2002. Natural deduction for CTL. Bulletin of the section of logic 31(4): 231–240.Google Scholar
  22. [151]
    Indrzejczak, A. 2003. A labelled natural deduction system for linear temporal logic. Studia Logica 75(3): 345–376.CrossRefGoogle Scholar
  23. [32]
    Blackburn, P. 2000. Internalizing labelled deduction. Journal of Logic and Computation 10(1): 137–168.CrossRefGoogle Scholar
  24. [152]
    Indrzejczak, A. 2005. Sequent calculi for monotonic modal logics. Bulletin of the Section of logic 34(3): 151–164.Google Scholar
  25. [61]
    Carnielli, W.A. 1991. On sequents and tableaux for many-valued logics. Journal of Non-Classical Logic 8(1): 59–76.Google Scholar
  26. [146]
    Indrzejczak, A. 2000. Multiple sequent calculus for tense logics. Abstracts of AiML and ICTL 2000: 93–104, Leipzig.Google Scholar
  27. [21]
    Basin, D., S. Matthews, and L. Vigano. 1997. Labelled propositional modal logics: Theory and practice. Journal of Logic and Computation 7(6): 685–717.CrossRefGoogle Scholar
  28. [280]
    Wansing, H. 1998. Displaying modal logics. Dordrecht: Kluwer Academic Publishers.Google Scholar
  29. [111]
    Girle, R. 2000. Elementary modal logic. London: Acumen.Google Scholar
  30. [49]
    Bonette, N., and R. Goré. 1998. A labelled sequent system for tense logic Kt. In AI98: Proceedings of the Australian joint conference on artificial inteligence, LNAI Springer, 1502: 71–82.Google Scholar
  31. [92]
    Fitting, M. 1972. Tableau methods of proof for modal logics. Notre Dame Journal of Formal Logic 13(2): 237–247.CrossRefGoogle Scholar
  32. [96]
    Fitting, M., and R.L. Mendelsohn. 1998. First-order modal logic. Dordrecht: Kluwer.Google Scholar
  33. [192]
    Mouri, M. 2001. Theorem provers with countermodels and xpe. Bulletin of the Section of Logic 30(2): 79–86.Google Scholar
  34. [90]
    Fitch, F. 1966. Tree proofs in modal logic (abstract). The Journal of Symbolic Logic 31:152.Google Scholar
  35. [237]
    Russo, A. 1995. Modal labelled deductive systems. Dept. of Computing, Imperial College, London, Technical Report 95(7).Google Scholar
  36. [130]
    Heuerding, A., M. Seyfried, and H. Zimmermann. 1996. Efficient loop-check for backward proof search in some non-classical propositional logics. In Tableaux 96, LNCS 1071, eds. P. Miglioli et al., 210–225. Berlin: Springer.Google Scholar
  37. [240]
    Sato, M. 1977. A study of Kripke-type models for some modal logics by Gentzen’s sequential method. Publications of the Research Institute for Mathematical Sciences, Kyoto University 13: 381–468.CrossRefGoogle Scholar
  38. [94]
    Fitting, M. 1990. Destructive modal resolution. Journal of Logic and Computation 1(1): 83–97.CrossRefGoogle Scholar
  39. [97]
    Fitting, M. 2007. Modal proof theory. In Handbook of modal logic, eds. P. Blackburn, J.F.A.K van Benthem, and F. Wolter, 85–138. Amsterdam: Elsevier.Google Scholar
  40. [195]
    Nishimura, H. 1980. A study of some tense logics by Gentzen’s sequential method. Publications of the Research Institute for Mathematical Sciences, Kyoto University 16: 343–353.CrossRefGoogle Scholar
  41. [160]
    Kanger, S. 1957. Provability in Logic, Stockholm: Almqvist & Wiksell.Google Scholar
  42. [143]
    Indrzejczak, A. 1997. Generalised sequent calculus for propositional modal logics. Logica Trianguli 1: 15–31.Google Scholar
  43. [222]
    Priest, G. 2001. An introduction to non-classical logic. Cambridge: Cambridge University Press.Google Scholar
  44. [271]
    Tapscott, B.L. 1987. A simplified natural deduction approach to certain modal systems. Notre Dame Journal of Formal Logic 23(3): 371–384.CrossRefGoogle Scholar
  45. [194]
    Negri, S. 2005. Proof analysis in modal logic. Journal of Philosophical Logic 34: 507–544.CrossRefGoogle Scholar
  46. [16]
    Avron, A. 1996. The method of hypersequents in the proof theory of propositional non-classical logics. In Logic: From foundations to applications, eds. W. Hodges et al., 1–32. Oxford: Oxford Science Publication.Google Scholar
  47. [175]
    Leszczyńska, D. 2008. The method of Socratic proofs for modal propositional logics: K5, S4.2, S4.3, S4M, S4F, S4R anf G. Studia Logica 89(3): 365–399.CrossRefGoogle Scholar
  48. [63]
    Castellini, C. and A. Smaill. 2000. A systematic presentation of quantified modal logics. Logic Journal of the IGPL 10: 571–599.CrossRefGoogle Scholar
  49. [62]
    Castellini, C. 2005. Automated reasoning in quantified modal and temporal logic, PhD thesis, University of Edinburgh.Google Scholar
  50. [18]
    Baldoni, M. 1998. Normal multimodal logics: Automatic deduction and logic programming extension PhD thesis, Torino.Google Scholar
  51. [19]
    Baldoni, M. 2000. Normal multimodal logics with interaction axioms. In Labelled deduction vol 17 of Applied Logic Series, eds. D. Basin et al., 33–53. Dordrecht: Kluwer.Google Scholar
  52. [47]
    Bolotov, A., A. Basukoski, O. Grigoriev, and V. Shangin. 2006. Natural deduction calculus for linear-time temporal logic. Proceedings of jelia 2006. LNAI, Springer 4160.Google Scholar
  53. [48]
    Bolotov, A., O. Grigoriev, and V. Shangin. 2006. Natural deduction calculus for CTL. IEEE John Vincent Atanasoff Symposium on Modern Computing, 175–183.Google Scholar
  54. [236]
    Rousseau, G. 1967. Sequents in many valued logic. Fundamenta Mathematicae, LX 1: 22–23.Google Scholar
  55. [75]
    Curry, H.B. 1950. A theory of formal deducibility. Notre Dame: University of Notre Dame Press.Google Scholar
  56. [76]
    Curry, H.B. 1952. The elimination theorem when modality is present. Journal of Symbolic Logic 17: 249–265.CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media B.V. 2010

Authors and Affiliations

  1. 1.Dept. LogicUniversity of LódzLódzPoland

Personalised recommendations