Abstract
In recent work we have extended the description logic (DL) \(\mathcal {ALC\!Q}\) by means of more expressive number restrictions using numerical and set constraints stated in the quantifier-free fragment of Boolean Algebra with Presburger Arithmetic (QFBAPA). It has been shown that reasoning in the resulting DL, called \(\mathcal {ALCSCC}\), is PSpace-complete without a TBox and ExpTime-complete w.r.t. a general TBox. The semantics of \(\mathcal {ALCSCC}\) is defined in terms of finitely branching interpretations, that is, interpretations where every element has only finitely many role successors. This condition was needed since QFBAPA considers only finite sets. In this paper, we first introduce a variant of \(\mathcal {ALCSCC}\), called \(\mathcal {ALCSCC} ^\infty \), in which we lift this requirement (inexpressible in first-order logic) and show that the complexity results for \(\mathcal {ALCSCC}\) mentioned above are preserved. Nevertheless, like \(\mathcal {ALCSCC}\), \(\mathcal {ALCSCC} ^\infty \) is not a fragment of first-order logic. The main contribution of this paper is to give a characterization of the first-order fragment of \(\mathcal {ALCSCC} ^\infty \). The most important tool used in the proof of this result is a notion of bisimulation that characterizes this fragment.
Partially supported by the German Research Foundation (DFG) within the Research Unit 1513 (Hybris) and the Research Training Group 1763 (QuantLA).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The complement is defined w.r.t. \(\sigma (\mathcal {U})\), i.e., \(\sigma (s^c)= \sigma (\mathcal {U})\setminus \sigma (s)\).
- 2.
Note that we do not distinguish between different infinite cardinalities, such as countably infinite, uncountably infinite, etc.
- 3.
A more detailed definition of the semantics can be found in [5].
- 4.
Note that, by induction, the sets \(D^\mathcal {I}\) are well-defined.
References
Baader, F.: Description logic terminology. In: [4], pp. 485–495 (2003)
Baader, F.: A new description logic with set constraints and cardinality constraints on role successors. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 43–59. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66167-4_3
Baader, F.: Expressive cardinality constraints on \(\cal{ALCSCC}\) concepts. In: Proceedings of the 34th Annual ACM Symposium on Applied Computing (SAC 2019), pp. 1123–1131. ACM (2019)
Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2003)
De Bortoli, F.: Integrating reasoning services for description logics with cardinality constraints with numerical optimization techniques. EMCL Master’s thesis, Chair for Automata Theory, Faculty of Computer Science, TU Dresden (2019). https://tu-dresden.de/inf/lat/theses#DeBo-Mas-19
Eisenbrand, F., Shmonin, G.: Carathéodory bounds for integer cones. Oper. Res. Lett. 34(5), 564–568 (2006)
Finger, M., De Bona, G.: Algorithms for deciding counting quantifiers over unary predicates. In: Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence (AAAI 2017), pp. 3878–3884. AAAI Press (2017)
Hoehndorf, R., Schofield, P.N., Gkoutos, G.V.: The role of ontologies in biological and biomedical research: a functional perspective. Brief. Bioinform. 16(6), 1069–1080 (2015)
Hollunder, B., Baader, F.: Qualifying number restrictions in concept languages. In: Proceedings of the 2nd International Conference on the Principles of Knowledge Representation and Reasoning (KR 1991), pp. 335–346 (1991)
Kuncak, V., Piskac, R., Suter, P.: Ordered sets in the calculus of data structures. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 34–48. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15205-4_5
Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for Boolean algebra with Presburger arithmetic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 215–230. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73595-3_15
Kurtonina, N., de Rijke, M.: Expressiveness of concept expressions in first-order description logics. Artif. Intell. 107(2), 303–333 (1999)
Lutz, C., Piro, R., Wolter, F.: Description logic TBoxes: model-theoretic characterizations and rewritability. In: Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI 2011), IJCAI/AAAI, pp. 983–988 (2011)
Papadimitriou, C.H.: On the complexity of integer programming. J. ACM 28(4), 765–768 (1981)
Pratt-Hartmann, I.: On the computational complexity of the numerically definite syllogistic and related logics. Bull. Symb. Logic 14(1), 1–28 (2008)
Schild, K. A correspondence theory for terminological logics: preliminary report. In: Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI 1991), pp. 466–471 (1991)
Schmidt-Schauß, M., Smolka, G.: Attributive concept descriptions with complements. Artif. Intell. 48(1), 1–26 (1991)
Tobies, S.: A PSpace algorithm for graded modal logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 52–66. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48660-7_4
Tobies, S.: Complexity results and practical algorithms for logics in knowledge representation. PhD thesis, LuFG Theoretical Computer Science, RWTH-Aachen, Germany (2001). http://tu-dresden.de/inf/lat/theses/#Tobies-PhD-2001
van Benthem, J.: Modal Logic and Classical Logic. Bibliopolis, Napoli (1983)
Acknowledgment
The authors would like to thank Ulrike Baumann for helpful discussions regarding QFBAPA\(^\infty \). We should also like to point out that we have learned about the results regarding QFBAPA\(_\infty \) in [10] only a couple of days before the submission of the final version of this paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Baader, F., De Bortoli, F. (2019). On the Expressive Power of Description Logics with Cardinality Constraints on Finite and Infinite Sets. In: Herzig, A., Popescu, A. (eds) Frontiers of Combining Systems. FroCoS 2019. Lecture Notes in Computer Science(), vol 11715. Springer, Cham. https://doi.org/10.1007/978-3-030-29007-8_12
Download citation
DOI: https://doi.org/10.1007/978-3-030-29007-8_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-29006-1
Online ISBN: 978-3-030-29007-8
eBook Packages: Computer ScienceComputer Science (R0)