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

  • Matteo Baldoni
  • Laura Giordano
  • Alberto Martelli
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)


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.


Multimodal logics Prefixed Tableaux methods Decidability Formal Grammars 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Y. Auffray and P. Enjalbert. Modal Theorem Proving: An equational viewpoint. Journal of Logic and Computation, 2(3):247–297, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 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. 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. 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. 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. 6.
    R. V. Book. Thue Systems as Rewriting Systems. Journal of Symbolic Computation, 3(1–2):39–68, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    L. Catach. Normal Multimodal Logics. In Proc. of the AAAI’ 88, pages 491–495. Morgan Kaufmann, 1988.Google Scholar
  8. 8.
    L. Catach. TABLEAUX: A General Theorem Prover for Modal Logics. Journal of Automated Reasoning, 7(4):489–510, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 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. 10.
    P. Enjalbert and L. Fariñas del Cerro. Modal Resolution in Clausal Form. Theoretical Computer Science, 65(1):1–33, 1989zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    L. Fariñas del Cerro and M. Penttonen. Grammar Logics. Logique et Analyse, 121–122:123–134, 1988.Google Scholar
  12. 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.zbMATHCrossRefMathSciNetGoogle Scholar
  13. 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. 14.
    M. Fitting. Proof Methods for Modal and Intuitionistic Logics, volume 169 of Synthese library. D. Reidel, Dordrecht, Holland, 1983.zbMATHGoogle Scholar
  15. 15.
    O. Gasquet. Optimization of deduction for multi-modal logics. In Applied Logic: How, What and Why? Kluwer Academic Publishers, 1993.Google Scholar
  16. 16.
    M. Genesereth and N. Nilsson. Logical Foundations of Artificial Intelligence. Morgan Kaufmann, 1987.Google Scholar
  17. 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. 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. 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.zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    D. Harel, A. Pnueli, and J. Stavi. Propositional Dynamic Logic of Nonregular Programs. Journal of Computer and System Sciences, 26:222–243, 1983.zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    J. E. Hopcroft and J. D. Ullman. Introduction to automata theory, languages, and computation. Addison-Wesley Publishing Company, 1979.Google Scholar
  22. 22.
    G. E. Hughes and M. J. Cresswell. A Companion to Modal Logic. Meuthuen, 1984.Google Scholar
  23. 23.
    G. E. Hughes and M. J. Cresswell. A New Introduciton to Modal Logic. Routledge, 1996.Google Scholar
  24. 24.
    M. Kracth. Highway to the Danger Zone. Journal of Logic and Computation, 5(1):93–109, 1995.CrossRefMathSciNetGoogle Scholar
  25. 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. 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. 27.
    A. Nonnengart. First-Order Modal Logic Theorem Proving and Functional Simulation. In Proc. of IJCAI’93, pages 80–85, 1993.Google Scholar
  28. 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. 29.
    H. J. Ohlbach. Translation methods for non-classical logics: An overview. Bull. of the IGPL, 1(1):69–89, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  30. 30.
    H.J. Ohlbach. Semantics-Based Translation Methods for Modal Logics. Journal of Logic and Computation, 1(5):691–746, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  31. 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. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Matteo Baldoni
    • 1
  • Laura Giordano
    • 1
  • Alberto Martelli
    • 1
  1. 1.Dipartimento di InformaticaUniversità degli Studi di TorinoTorinoItaly

Personalised recommendations