ExpTime Tableaux with Global Caching for Hybrid PDL

  • Linh Anh NguyenEmail author


We present the first direct tableau decision procedure with the ExpTime complexity for HPDL (Hybrid Propositional Dynamic Logic). It checks whether a given ABox (a finite set of assertions) in HPDL is satisfiable. Technically, it combines global caching with checking fulfillment of eventualities and dealing with nominals. Our procedure contains enough details for direct implementation and has been implemented for the TGC2 (Tableaux with Global Caching) system. As HPDL can be used as a description logic for representing and reasoning about terminological knowledge, our procedure is useful for practical applications.


Modal logic Propositional dynamic logic Tableau-based decision procedures Global caching Complexity-optimal tableaux 



We would like to thank the anonymous reviewers for many comments and suggestions, which have helped us to improve the paper significantly.


  1. 1.
    Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Benthem, J.V., Wolter, F. (eds.) Handbook of Modal Logic, Studies in Logic and Practical Reasoning, vol. 3, pp. 821–868. Elsevier, New York (2007)Google Scholar
  2. 2.
    Baader, F., Sattler, U.: An overview of tableau algorithms for description logics. Studia Logica 69, 5–40 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Blackburn, P.: Internalizing labelled deduction. J. Log. Comput. 10(1), 137–168 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Blackburn, P., ten Cate, B.: Pure extensions, proof rules, and hybrid axiomatics. Studia Logica 84(2), 277–322 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Bolander, T., Blackburn, P.: Termination for hybrid tableaus. J. Log. Comput. 17(3), 517–554 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Bolander, T., Blackburn, P.: Terminating tableau calculi for hybrid logics extending K. Electr. Notes Theor. Comput. Sci. 231, 21–39 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Bolander, T., Braüner, T.: Tableau-based decision procedures for hybrid logic. J. Log. Comput. 16(6), 737–763 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Braüner, T.: Why does the proof-theory of hybrid logic work so well? J. Appl. Non-Class. Log. 17(4), 521–543 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Braüner, T.: Hybrid logic. In: Zalta, E. (ed.) The Stanford Encyclopedia of Philosophy, summer, 2017th edn. Stanford University, Metaphysics Research Lab (2017)Google Scholar
  10. 10.
    Calvanese, D., De Giacomo, G., Lenzerini, M., Nardi, D.: Reasoning in expressive description logics. In: Robinson, J.A., Voronkov, A. (eds) Handbook of Automated Reasoning, vol. 2, pp. 1581–1634. Elsevier and MIT Press (2001)Google Scholar
  11. 11.
    Cerrito, S., Mayer, M.C.: Nominal substitution at work with the global and converse modalities. In: Beklemishev, L.D., Goranko, V., Shehtman, V.B. (eds) Advances in Modal Logic 8, Papers from the Eighth Conference on Advances in Modal Logic held in Moscow, Russia, 24–27 August 2010, pp. 59–76. College Publications (2010)Google Scholar
  12. 12.
    Divroodi, A., Nguyen, L.: On bisimulations for description logics. Inf. Sci. 295, 465–493 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Donini, F., Massacci, F.: ExpTime tableaux for \(\cal{ALC}\). Art. Intell. 124, 87–138 (2000)CrossRefzbMATHGoogle Scholar
  14. 14.
    Dunin-Kȩplicz, B., Nguyen, L., Szałas, A.: Converse-PDL with regular inclusion axioms: a framework for MAS logics. J. Appl. Non-Class. Log. 21(1), 61–91 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Fischer, M., Ladner, R.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Giacomo, G.D., Lenzerini, M.: TBox and ABox reasoning in expressive description logics. In: Proceedings of KR’1996, pp. 316–327 (1996)Google Scholar
  17. 17.
    Goré, R.: And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL. In: Proceedings of IJCAR 2014, LNCS, vol. 8562, pp. 26–45. Springer (2014)Google Scholar
  18. 18.
    Goré, R., Nguyen, L.: Analytic cut-free tableaux for regular modal logics of agent beliefs. In: Proceedings of CLIMA VIII, LNCS, vol. 5056, pp. 274–289. Springer (2007)Google Scholar
  19. 19.
    Goré, R., Nguyen, L.: ExpTime tableaux for \(\cal{ALC}\) using sound global caching. J. Autom. Reason. 50(4), 355–381 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Goré, R., Postniece, L.: An experimental evaluation of global caching for \(\cal{ALC}\) (system description). In: Proceedings of IJCAR 2008, LNCS, vol. 5195, pp. 299–305. Springer (2008)Google Scholar
  21. 21.
    Goré, R., Widmann, F.: An optimal on-the-fly tableau-based decision procedure for PDL-satisfiability. In: R. Schmidt (ed.) Proceedings of CADE-22, LNAI 5663, pp. 437–452. Springer (2009)Google Scholar
  22. 22.
    Goré, R., Widmann, F.: Optimal and cut-free tableaux for propositional dynamic logic with converse. In: Proceedings of IJCAR 2010, LNCS, vol. 6173, pp. 225–239. Springer (2010)Google Scholar
  23. 23.
    Hansen, J.: Terminating tableaux for dynamic epistemic logics. Electr. Notes Theor. Comput. Sci. 262, 141–156 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, New York (2000)CrossRefzbMATHGoogle Scholar
  25. 25.
    Horrocks, I., Sattler, U.: A tableau decision procedure for \(\cal{SHOIQ}\). J. Autom. Reason. 39(3), 249–276 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Kaminski, M., Smolka, G.: A goal-directed decision procedure for Hybrid PDL. J. Autom. Reason. 52(4), 407–450 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Kritsimallis, A.: Tableaux with partial caching for Hybrid PDL with satisfaction statements. In: Proceedings of ICTAC 2017, LNCS, vol. 10580, pp. 229–247. Springer (2017)Google Scholar
  28. 28.
    Nguyen, L.: Cut-free ExpTime tableaux for Converse-PDL extended with regular inclusion axioms. In: Proc. of KES-AMSTA’2013, Frontiers in Artificial Intelligence and Applications, vol. 252, pp. 235–244. IOS Press (2013)Google Scholar
  29. 29.
    Nguyen, L.: ExpTime tableaux with global state caching for the description logic \(\cal{SHIO}\). Neurocomputing 146, 249–263 (2014)CrossRefGoogle Scholar
  30. 30.
    Nguyen, L.: Design of the tableau reasoner TGC2 for description logics. Int. J. Softw. Eng. Knowl. Eng. 26(8), 1315–1333 (2016)CrossRefGoogle Scholar
  31. 31.
    Nguyen, L.: ExpTime tableaux with global caching for graded propositional dynamic logic. Fundam. Inf. 147(2–3), 261–288 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    Nguyen, L., Golińska-Pilarek, J.: An ExpTime tableau method for dealing with nominals and qualified number restrictions in deciding the description logic \(\cal{SHOQ}\). Fundam. Inf. 135(4), 433–449 (2014)MathSciNetzbMATHGoogle Scholar
  33. 33.
    Nguyen, L., Szałas, A.: Checking consistency of an ABox w.r.t. global assumptions in PDL. Fundam. Inf. 102(1), 97–113 (2010)MathSciNetzbMATHGoogle Scholar
  34. 34.
    Pratt, V.: A near-optimal method for reasoning about action. J. Comput. Syst. Sci. 20(2), 231–254 (1980)MathSciNetCrossRefzbMATHGoogle Scholar
  35. 35.
    Sattler, U., Vardi, M.: The hybrid \(\mu \)-calculus. In: Proceedings of IJCAR 2001, LNCS, vol. 2083, pp. 76–91. Springer (2001)Google Scholar
  36. 36.
    Schild, K.: A correspondence theory for terminological logics: preliminary report. In: Proceedings of IJCAI’1991, pp. 466–471 (1991)Google Scholar
  37. 37.
    Seligman, J.: Internalization: The case of hybrid logics. J. Log. Comput. 11(5), 671–689 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  38. 38.
    Tzakova, M.: Tableau calculi for hybrid logics. In: Proceedings of TABLEAUX’99, LNCS, vol. 1617, pp. 278–292. Springer (1999)Google Scholar

Copyright information

© Springer Nature B.V. 2019

Authors and Affiliations

  1. 1.Division of Knowledge and System Engineering for ICT, Faculty of Information TechnologyTon Duc Thang UniversityHo Chi Minh CityVietnam
  2. 2.Institute of InformaticsUniversity of WarsawWarsawPoland

Personalised recommendations