Skip to main content
SpringerLink
Log in

Labelled Systems in Modal Logics

  • Chapter
  • First Online:
Natural Deduction, Hybrid Systems and Modal Logics

Part of the book series: Trends in Logic ((TREN,volume 30))

  • 1007 Accesses

Abstract

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.

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 189.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 249.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 249.99
Price excludes VAT (USA)
  • Durable hardcover 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

Notes

  1. 1.

    Cf. remarks in Section 7.2 on the lack of confluency in most of standard modal SC's.

  2. 2.

    One may mention also ND systems with strong labelling for other kinds of temporal logics not discussed in this book, like PLTL or CTL provided by Renteria and Hausler [230] or by Bolotov, Basukoski, Grigoriev and Shangin in [47, 48].

  3. 3.

    Massacci [186] provides a formal proof of this fact.

  4. 4.

    This feature makes Fitting's approach similar to Suppes’ format ND as compared to Jaśkowski format – cf. the Remarks in Section 2.4.3.

  5. 5.

    Although not always; for example Tapscott [271] is using essentially Fitting's labels in ND-system.

  6. 6.

    A justification for such rules may be found in [93].

  7. 7.

    This is essentially the solution of Fitting [93].

  8. 8.

    By the way, in regular logics we may even get rid of \((L\pi E^\prime)\) if we admit [LPOS] from Remark 8.3. as primitive, but we left the proof of this fact to the reader.

  9. 9.

    The former is in fact present in [93].

  10. 10.

    Except (LMB), since B-logics were not considered in [154] because of the lack of analytic formalization.

  11. 11.

    In fact, we may also use a static rule (LD) stated above for normal and regular logics instead of a transfer rule from the list.

  12. 12.

    A similar solution was applied in Mints [191] by addition of Fitting's labels to whole sequents in his version of (labelled) hipersequent calculi.

References

  1. 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. 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.

    Article  Google Scholar 

  3. Zeman, J.J. 1973. Modal logic. Oxford: Oxford University Press.

    Google Scholar 

  4. Gabbay, D. 1996. LDS-labelled deductive systems. Oxford: Clarendon Press.

    Google Scholar 

  5. 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. Fitting, M. 1983. Proof methods for modal and intuitionistic logics. Dordrecht; Rei-del.

    Google Scholar 

  7. Mints, G. 1997. Indexed systems of sequents and cut-elimination. Journal of Philosophical Logic 26: 671–696.

    Article  Google Scholar 

  8. Aho, A.V., and J.D. Ullman. 1995. Foundations of computer science. New York: W.H. Freeman and CO.

    Google Scholar 

  9. 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. Vigano, L. 2000. Labelled non-classical logics. Dordrecht: Kluwer.

    Google Scholar 

  11. Blackburn, P. 2000. Representation, reasoning, and relational structures: A hybrid logic manifesto. Logic Journal of the IGPL 8(3): 339–365.

    Article  Google Scholar 

  12. Anderson, A., and N.D. Belnap, Jr. 1975. Entailment: The logic of relewance and necessity, vol I. Princeton: Princeton University Press.

    Google Scholar 

  13. Indrzejczak, A. 1996. Cut-free sequent calculus for S5. Bulletin of the Section of Logic 25(2): 95–102.

    Google Scholar 

  14. Avron, A., F. Honsell, M. Miculan, and C. Paravano. 1998. Encoding modal logics in logical frameworks. Studia Logica 60: 161–202.

    Article  Google Scholar 

  15. Basin, D., S. Matthews, and L. Vigano. 1998. Natural deduction for non-classical logics. Studia Logica 60: 119–160.

    Article  Google Scholar 

  16. 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. 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.

    Article  Google Scholar 

  18. Hähnle, R. 1994. Automated deduction in multiple-valued logics. Oxford: Oxford University Press.

    Google Scholar 

  19. Indrzejczak, A. 2007. Labelled tableau calculi for weak modal logics. Bulletin of the Section of logic 36(3–4): 159–173.

    Google Scholar 

  20. Rescher, N., and A. Urquhart. 1971. Temporal logic. New York: Springer-Verlag.

    Google Scholar 

  21. Renteria, C., and E. Hausler. 2002. Natural deduction for CTL. Bulletin of the section of logic 31(4): 231–240.

    Google Scholar 

  22. Indrzejczak, A. 2003. A labelled natural deduction system for linear temporal logic. Studia Logica 75(3): 345–376.

    Article  Google Scholar 

  23. Blackburn, P. 2000. Internalizing labelled deduction. Journal of Logic and Computation 10(1): 137–168.

    Article  Google Scholar 

  24. Indrzejczak, A. 2005. Sequent calculi for monotonic modal logics. Bulletin of the Section of logic 34(3): 151–164.

    Google Scholar 

  25. Carnielli, W.A. 1991. On sequents and tableaux for many-valued logics. Journal of Non-Classical Logic 8(1): 59–76.

    Google Scholar 

  26. Indrzejczak, A. 2000. Multiple sequent calculus for tense logics. Abstracts of AiML and ICTL 2000: 93–104, Leipzig.

    Google Scholar 

  27. Basin, D., S. Matthews, and L. Vigano. 1997. Labelled propositional modal logics: Theory and practice. Journal of Logic and Computation 7(6): 685–717.

    Article  Google Scholar 

  28. Wansing, H. 1998. Displaying modal logics. Dordrecht: Kluwer Academic Publishers.

    Google Scholar 

  29. Girle, R. 2000. Elementary modal logic. London: Acumen.

    Google Scholar 

  30. 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. Fitting, M. 1972. Tableau methods of proof for modal logics. Notre Dame Journal of Formal Logic 13(2): 237–247.

    Article  Google Scholar 

  32. Fitting, M., and R.L. Mendelsohn. 1998. First-order modal logic. Dordrecht: Kluwer.

    Google Scholar 

  33. Mouri, M. 2001. Theorem provers with countermodels and xpe. Bulletin of the Section of Logic 30(2): 79–86.

    Google Scholar 

  34. Fitch, F. 1966. Tree proofs in modal logic (abstract). The Journal of Symbolic Logic 31:152.

    Google Scholar 

  35. Russo, A. 1995. Modal labelled deductive systems. Dept. of Computing, Imperial College, London, Technical Report 95(7).

    Google Scholar 

  36. 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. 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.

    Article  Google Scholar 

  38. Fitting, M. 1990. Destructive modal resolution. Journal of Logic and Computation 1(1): 83–97.

    Article  Google Scholar 

  39. 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. 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.

    Article  Google Scholar 

  41. Kanger, S. 1957. Provability in Logic, Stockholm: Almqvist & Wiksell.

    Google Scholar 

  42. Indrzejczak, A. 1997. Generalised sequent calculus for propositional modal logics. Logica Trianguli 1: 15–31.

    Google Scholar 

  43. Priest, G. 2001. An introduction to non-classical logic. Cambridge: Cambridge University Press.

    Google Scholar 

  44. Tapscott, B.L. 1987. A simplified natural deduction approach to certain modal systems. Notre Dame Journal of Formal Logic 23(3): 371–384.

    Article  Google Scholar 

  45. Negri, S. 2005. Proof analysis in modal logic. Journal of Philosophical Logic 34: 507–544.

    Article  Google Scholar 

  46. 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. 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.

    Article  Google Scholar 

  48. Castellini, C. and A. Smaill. 2000. A systematic presentation of quantified modal logics. Logic Journal of the IGPL 10: 571–599.

    Article  Google Scholar 

  49. Castellini, C. 2005. Automated reasoning in quantified modal and temporal logic, PhD thesis, University of Edinburgh.

    Google Scholar 

  50. Baldoni, M. 1998. Normal multimodal logics: Automatic deduction and logic programming extension PhD thesis, Torino.

    Google Scholar 

  51. 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. 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. 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. Rousseau, G. 1967. Sequents in many valued logic. Fundamenta Mathematicae, LX 1: 22–23.

    Google Scholar 

  55. Curry, H.B. 1950. A theory of formal deducibility. Notre Dame: University of Notre Dame Press.

    Google Scholar 

  56. Curry, H.B. 1952. The elimination theorem when modality is present. Journal of Symbolic Logic 17: 249–265.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. Logic, University of Lódz, Kopcinskiego 16/18, 90-232, Lódz, Poland

    Dr. Andrzej Indrzejczak

Authors
  1. Dr. Andrzej Indrzejczak
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrzej Indrzejczak .

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer Science+Business Media B.V.

About this chapter

Cite this chapter

Indrzejczak, A. (2010). Labelled Systems in Modal Logics. In: Natural Deduction, Hybrid Systems and Modal Logics. Trends in Logic, vol 30. Springer, Dordrecht. https://doi.org/10.1007/978-90-481-8785-0_8

Download citation

Publish with us

Policies and ethics

Search

Navigation