Coalgebraic Hybrid Logic

  • Rob Myers
  • Dirk Pattinson
  • Lutz Schröder
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5504)


We introduce a generic framework for hybrid logics, i.e. modal logics additionally featuring nominals and satisfaction operators, thus providing the necessary facilities for reasoning about individual states in a model. This framework, coalgebraic hybrid logic, works at the same level of generality as coalgebraic modal logic, and in particular subsumes, besides normal hybrid logics such as hybrid K, a wide variety of logics with non-normal modal operators such as probabilistic, graded, or coalitional modalities and non-monotonic conditionals. We prove a generic finite model property and an ensuing weak completeness result, and we give a semantic criterion for decidability in PSPACE. Moreover, we present a fully internalised PSPACE tableau calculus. These generic results are easily instantiated to particular hybrid logics and thus yield a wide range of new results, including e.g. decidability in PSPACE of probabilistic and graded hybrid logics.


Modal Logic Description Logic Sequent Calculus Kripke Structure Proof Tree 
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. 1.
    Areces, C., Blackburn, P., Marx, M.: A road-map on complexity for hybrid logics. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 307–321. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. 2.
    Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Wolter, F., van Benthem, J. (eds.) Handbook of Modal Logics. Elsevier, Amsterdam (2006)Google Scholar
  3. 3.
    Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook. Cambridge University Press, Cambridge (2003)zbMATHGoogle Scholar
  4. 4.
    Baader, F., Milicic, M., Lutz, C., Sattler, U., Wolter, F.: Integrating description logics and action formalisms for reasoning about web services. LTCS-Report LTCS-05-02, Dresden University of Technology (2005),
  5. 5.
    Bezhanishvili, N., ten Cate, B.: Transfer results for hybrid logic. Part 1: the case without satisfaction operators. J. Logic Comput. 16, 177–197 (2006)CrossRefzbMATHGoogle Scholar
  6. 6.
    Blackburn, P., Marx, M.: Tableaux for quantified hybrid logic. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 38–52. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  7. 7.
    Bolander, T., Blackburn, P.: Termination for hybrid tableaus. J. Logic Comput. 17, 517–554 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Bolander, T., Braüner, T.: Tableau-based decision procedures for hybrid logic. J. Log. Comput. 16(6), 737–763 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Book, R., Long, T., Selman, A.: Quantitative relativizations of complexity classes. SIAM J. Computing 13, 461–487 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Braüner, T.: Natural deduction for first-order hybrid logic. J. Logic, Language and Information 14, 173–198 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Calin, G., Myers, R., Pattinson, D., Schröder, L.: CoLoSS: The coalgebraic logic satisfiability solver (system description). In: Methods for Modalities, M4M-5. ENTCS. Elsevier, Amsterdam (to appear, 2008)Google Scholar
  12. 12.
    ten Cate, B.: Model theory for extended modal languages. PhD thesis, University of Amsterdam, ILLC Dissertation Series DS-2005-01 (2005)Google Scholar
  13. 13.
    Chandra, A., Stockmeyer, L.: Alternation. J. ACM 28, 114–133 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Chellas, B.: Modal Logic. Cambridge University Press, Cambridge (1980)CrossRefzbMATHGoogle Scholar
  15. 15.
    D’Agostino, G., Visser, A.: Finality regained: A coalgebraic study of Scott-sets and multisets. Arch. Math. Logic 41, 267–298 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Demri, S., Lugiez, D.: Presburger modal logic is PSPACE-complete. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 541–556. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  17. 17.
    Fagin, R., Halpern, J.Y.: Reasoning about knowledge and probability. J. ACM 41, 340–367 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Fine, K.: In so many possible worlds. Notre Dame J. Formal Logic 13, 516–520 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Haarslev, V., Möller, R., van der Straeten, R., Wessel, M.: Extended query facilities for racer and an application to software-engineering problems. In: Description Logics, DL 2004, pp. 148–157 (2004)Google Scholar
  20. 20.
    Heifetz, A., Mongin, P.: Probabilistic logic for type spaces. Games and Economic Behavior 35, 31–53 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Inform. Comput. 94, 1–28 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Mares, E.: Relevant Logic: A Philosophical Interpretation. Cambridge University Press, Cambridge (2004)CrossRefGoogle Scholar
  23. 23.
    Papadimitriou, C.: On the complexity of integer programming. J. ACM 28, 765–768 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Pattinson, D.: Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theoret. Comput. Sci. 309, 177–193 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Pattinson, D., Schröder, L.: Admissibility of cut in coalgebraic logics. In: Coalgebraic Methods in Computer Science, CMCS 2008. ENTCS, vol. 203, pp. 221–241. Elsevier, Amsterdam (2008)Google Scholar
  26. 26.
    Pauly, M.: A modal logic for coalitional power in games. J. Logic Comput. 12, 149–166 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Schröder, L.: A finite model construction for coalgebraic modal logic. J. Log. Algebr. Prog. 73, 97–110 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Schröder, L., Pattinson, D.: PSPACE reasoning for rank-1 modal logics. In: Logic in Computer Science, LICS 2006, pp. 231–240. IEEE, Los Alamitos (2006); Full version to appear in ACM TOCLGoogle Scholar
  29. 29.
    Schröder, L., Pattinson, D.: Shallow models for non-iterative modal logics. In: Dengel, A.R., Berns, K., Breuel, T.M., Bomarius, F., Roth-Berghofer, T.R. (eds.) KI 2008. LNCS (LNAI), vol. 5243, pp. 324–331. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  30. 30.
    Seligman, J.: Internalization: The case of hybrid logics. J. Logic Comput. 11, 671–689 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Sirin, E., Parsia, B., Grau, B.C., Kalyanpur, A., Katz, Y.: Pellet: A practical OWL-DL reasoner. J. Web Semantics (2006)Google Scholar
  32. 32.
    Troelstra, A., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, Cambridge (1996)zbMATHGoogle Scholar
  33. 33.
    Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: System description. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 292–297. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  34. 34.
    Tzakova, M.: Tableau calculi for hybrid logics. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS, vol. 1617, pp. 278–292. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  35. 35.
    Zolin, E.: The description logic complexity navigator (2007),

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Rob Myers
    • 1
  • Dirk Pattinson
    • 1
  • Lutz Schröder
    • 2
  1. 1.Department of ComputingImperial College LondonUK
  2. 2.DFKI Bremen and Department of Computer ScienceUniversität BremenGermany

Personalised recommendations