Abstract
We describe the Coalgebraic Ontology Logic solver Cool, a generic reasoner that decides the satisfiability of modal (and, more generally, hybrid) formulas with respect to a set of global assumptions – in Description Logic parlance, we support a general TBox and internalize a Boolean ABox. The level of generality is that of coalgebraic logic, a logical framework covering a wide range of modal logics, beyond relational semantics. The core of Cool is an efficient unlabelled tableaux search procedure using global caching. Concrete logics are added by implemening the corresponding (one-step) tableaux rules. The logics covered at the moment include standard relational examples as well as graded modal logic and Pauly’s Coalition Logic (the next-step fragment of Alternating-time Temporal Logic), plus every logic that arises as a fusion of the above. We compare the performance of Cool with state-of-the-art reasoners.
Work of the first, third, and fifth author supported by DFG grant GenMod2 (SCHR 1118/5-2).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672–713 (2002)
Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, pp. 821–868. Elsevier (2007)
Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook. Cambridge University Press (2003)
Calin, G., Myers, R., Pattinson, D., Schröder, L.: Coloss: The coalgebraic logic satisfiability solver. In: Methods for Modalities, M4M-5. ENTCS, vol. 231, pp. 41–54. Elsevier (2009)
Chellas, B.: Modal Logic. Cambridge University Press (1980)
Cîrstea, C., Kupke, C., Pattinson, D.: EXPTIME tableaux for the coalgebraic μ-calculus. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 179–193. Springer, Heidelberg (2009)
D’Agostino, G., Visser, A.: Finality regained: A coalgebraic study of Scott-sets and multisets. Arch. Math. Logic 41, 267–298 (2002)
David, A.: TATL: Implementation of ATL tableau-based decision procedure. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS, vol. 8123, pp. 97–103. Springer, Heidelberg (2013)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Fagin, R., Halpern, J.Y.: Reasoning about knowledge and probability. J. ACM 41, 340–367 (1994)
Fine, K.: In so many possible worlds. Notre Dame J. Formal Logic 13, 516–520 (1972)
Goré, R., Kupke, C., Pattinson, D.: Optimal tableau algorithms for coalgebraic logics. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 114–128. Springer, Heidelberg (2010)
Goré, R., Kupke, C., Pattinson, D., Schröder, L.: Global caching for coalgebraic description logics. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 46–60. Springer, Heidelberg (2010)
Goré, R., Nguyen, L.: EXPTIME tableaux for \(\mathcal{ALC}\) using sound global caching. In: Description Logics, DL 2007. CEUR Workshop Proceedings, vol. 250 (2007)
Goré, R.P., Postniece, L.: An experimental evaluation of global caching for \(\mathcal{ALC}\) (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 299–305. Springer, Heidelberg (2008)
Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabilities. In: Real-Time Systems, RTSS 1990, pp. 278–287. IEEE Computer Society (1990)
Pattinson, D.: Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theoret. Comput. Sci. 309, 177–193 (2003)
Pauly, M.: A modal logic for coalitional power in games. J. Log. Comput. 12, 149–166 (2002)
Schröder, L., Pattinson, D.: PSPACE bounds for rank-1 modal logics. ACM Trans. Comput. Log. 13, 1–13 (2009)
Segala, R.: Modelling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)
Snell, W., Pattinson, D., Widmann, F.: Solving graded/probabilistic modal logic via linear inequalities (system description). In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 383–390. Springer, Heidelberg (2012)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Gorín, D., Pattinson, D., Schröder, L., Widmann, F., Wißmann, T. (2014). Cool – A Generic Reasoner for Coalgebraic Hybrid Logics (System Description). In: Demri, S., Kapur, D., Weidenbach, C. (eds) Automated Reasoning. IJCAR 2014. Lecture Notes in Computer Science(), vol 8562. Springer, Cham. https://doi.org/10.1007/978-3-319-08587-6_31
Download citation
DOI: https://doi.org/10.1007/978-3-319-08587-6_31
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08586-9
Online ISBN: 978-3-319-08587-6
eBook Packages: Computer ScienceComputer Science (R0)