Skip to main content
Springer Nature Link
Log in

A Tableau Calculus for Multimodal Logics and Some (Un)Decidability Results

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

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

  • 376 Accesses

Abstract

In this paper we present a prefixed analytic tableau calculus for a class of normal multimodal logics and we present some results about decidability and undecidability of this class. The class is characterized by axioms of the form [t 1] ... [t n]ϕ ⊃ [s 1] ... [s m]ϕ, called inclusion axioms, where the t i’s and s j’s are constants. This class of logics, called grammar logics, was introduced for the first time by Fariñas del Cerro and Penttonen to simulate the behaviour of grammars in modal logics, and includes some well-known modal systems. The prefixed tableau method is used to prove the undecidability of modal systems based on unrestricted, context sensitive, and context free grammars. Moreover, we show that the class of modal logics, based on right-regular grammars, are decidable by means of the filtration methods, by defining an extension of the Fischer-Ladner closure.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Y. Auffray and P. Enjalbert. Modal Theorem Proving: An equational viewpoint. Journal of Logic and Computation, 2(3):247–297, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  2. M. Baldoni. Normal Multimodal Logics: Automatic Deduction and Logic Programming Extension. PhD thesis, Dipartimento di Informatica, Università degli Studi di Torino, 1998.

    Google Scholar 

  3. M. Baldoni, L. Giordano, and A. Martelli. A Multimodal Logic to define Modules in Logic Programming. In Proc. of ILPS’93, pages 473–487. The MIT Press, 1993.

    Google Scholar 

  4. M. Baldoni, L. Giordano, and A. Martelli. A Framework for Modal Logic Programming. In Proc. of the JICSLP’96, pages 52–66. The MIT Press, 1996.

    Google Scholar 

  5. B. Beckert and R. Goré. Free Variable Tableaux for Propositional Modal Logics. In Proc. of TABLEAUX’97, volume 1227 of LNAI, pages 91–106. Springer-Verlag, 1997.

    Google Scholar 

  6. R. V. Book. Thue Systems as Rewriting Systems. Journal of Symbolic Computation, 3(1–2):39–68, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  7. L. Catach. Normal Multimodal Logics. In Proc. of the AAAI’ 88, pages 491–495. Morgan Kaufmann, 1988.

    Google Scholar 

  8. L. Catach. TABLEAUX: A General Theorem Prover for Modal Logics. Journal of Automated Reasoning, 7(4):489–510, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  9. G. De Giacomo and F. Massacci. Tableaux and Algorithms for Propositional Dynamic Logic with Converse. In Proc. of CADE-15, volume 1249 of LNAI, pages 613–627. Springer, 1996.

    Google Scholar 

  10. P. Enjalbert and L. Fariñas del Cerro. Modal Resolution in Clausal Form. Theoretical Computer Science, 65(1):1–33, 1989

    Article  MATH  MathSciNet  Google Scholar 

  11. L. Fariñas del Cerro and M. Penttonen. Grammar Logics. Logique et Analyse, 121–122:123–134, 1988.

    Google Scholar 

  12. M. J. Fischer and R. E. Ladner. Propositional Dynamic Logic of Regular Programs. Journal of Computer and System Sciences, 18(2):194–211, 1979.

    Article  MATH  MathSciNet  Google Scholar 

  13. M. Fisher and R. Owens. An Introduction to Executable Modal and Temporal Logics. In Proc. of the IJCAI’93 Workshop on Executable Modal and Temporal Logics, volume 897 of LNAI, pages 1–20. Springer-Verlag, 1993.

    Google Scholar 

  14. M. Fitting. Proof Methods for Modal and Intuitionistic Logics, volume 169 of Synthese library. D. Reidel, Dordrecht, Holland, 1983.

    MATH  Google Scholar 

  15. O. Gasquet. Optimization of deduction for multi-modal logics. In Applied Logic: How, What and Why? Kluwer Academic Publishers, 1993.

    Google Scholar 

  16. M. Genesereth and N. Nilsson. Logical Foundations of Artificial Intelligence. Morgan Kaufmann, 1987.

    Google Scholar 

  17. R. A. Goré. Tableaux Methods for Modal and Temporal Logics. Technical Report TR-ARP-16-95, Automated Reasoning Project, Australian Nat. Univ., 1995.

    Google Scholar 

  18. G. Governatori. Labelled Tableaux for Multi-Modal Logics. In Proc. of TABLEAUX’ 95, volume 918 of LNAI, pages 79–94. Springer-Verlag, 1995.

    Google Scholar 

  19. J. Y. Halpern and Y. Moses. A Guide to Completeness and Complexity for Modal Logics of Knowledge and Belief. Artificial Intelligence, 54:319–379, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  20. D. Harel, A. Pnueli, and J. Stavi. Propositional Dynamic Logic of Nonregular Programs. Journal of Computer and System Sciences, 26:222–243, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  21. J. E. Hopcroft and J. D. Ullman. Introduction to automata theory, languages, and computation. Addison-Wesley Publishing Company, 1979.

    Google Scholar 

  22. G. E. Hughes and M. J. Cresswell. A Companion to Modal Logic. Meuthuen, 1984.

    Google Scholar 

  23. G. E. Hughes and M. J. Cresswell. A New Introduciton to Modal Logic. Routledge, 1996.

    Google Scholar 

  24. M. Kracth. Highway to the Danger Zone. Journal of Logic and Computation, 5(1):93–109, 1995.

    Article  MathSciNet  Google Scholar 

  25. F. Massacci. Strongly Analytic Tableaux for Normal Modal Logics. In Proc. of the CADE’94, volume 814 of LNAI, pages 723–737. Springer-Verlag, 1994.

    Google Scholar 

  26. A. Nerode. Some Lectures on Modal Logic. In F. L. Bauer, editor, Logic, Algebra, and Computation, volume 79 of NATO ASI Series. Springer-Verlag, 1989.

    Google Scholar 

  27. A. Nonnengart. First-Order Modal Logic Theorem Proving and Functional Simulation. In Proc. of IJCAI’93, pages 80–85, 1993.

    Google Scholar 

  28. H. J. Ohlbach. Optimized Translation of Multi Modal Logic into Predicate Logic. In Proc. of the Logic Programming and Automated Reasoning, volume 822 of LNAI, pages 253–264. Springer-Verlag, 1993.

    Google Scholar 

  29. H. J. Ohlbach. Translation methods for non-classical logics: An overview. Bull. of the IGPL, 1(1):69–89, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  30. H.J. Ohlbach. Semantics-Based Translation Methods for Modal Logics. Journal of Logic and Computation, 1(5):691–746, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  31. M.A. Orgun and W. Ma. An overview of temporal and modal logic programming. In Proc. of the First International Conference on Temporal Logic, volume 827 of LNAI, pages 445–479. Springer-Verlag, 1994.

    Google Scholar 

  32. J. Pitt and J. Cunningham. Distributed Modal Theorem Proving with KE. In Proc. of the TABLEAUX’96, volume 1071 of LNAI, pages 160–176. Springer-Verlag, 1996.

    Google Scholar 

  33. M. Wooldridge and N. R. Jennings. Agent Theories, Architectures, and Languages: A survey. In Proc. of the ECAI-94 Workshop on Agent Theories, volume 890 of LNAI, pages 1–39. Springer-Verlag, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università degli Studi di Torino, Corso Svizzera, 185, I-10149, Torino, Italy

    Matteo Baldoni, Laura Giordano & Alberto Martelli

Authors
  1. Matteo Baldoni
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Laura Giordano
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alberto Martelli
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Philosophy, Tilburg University, P.O. Box 90153, 5000 LE, Tilburg, The Netherlands

    Harrie de Swart

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baldoni, M., Giordano, L., Martelli, A. (1998). A Tableau Calculus for Multimodal Logics and Some (Un)Decidability Results. In: de Swart, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1998. Lecture Notes in Computer Science(), vol 1397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-69778-0_13

Download citation

  • DOI: https://doi.org/10.1007/3-540-69778-0_13

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64406-4

  • Online ISBN: 978-3-540-69778-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics