Description Logics That Count, and What They Can and Cannot Count (Extended Abstract)?

Abstract

Simple counting quantifiers that can be used to compare the number of role successors of an individual or the cardinality of a concept with a fixed natural number have been employed in Description Logics (DLs) for more than two decades, under the respective names of number restrictions [8,13,12] and cardinality restrictions on concepts (CRs, CBoxes) [4,19]. The DL ALCQ [12] extends the basic DL ALC with so-called qualified number restrictions of the form ( n r:C) and ( n r:C), collecting individuals for which the number of r successors belonging to the concept C is bounded from below/above by the natural number n. The computational complexity of concept satisfiability in ALCQ [12] has been shown to be PSpace-complete without concept inclusions (CIs, TBoxes) and ExpTime-complete w.r.t. CIs, independently from the encoding (unary or binary) of the numbers occurring in the restrictions [18,20]. CRs are global constraints of the form ( n C) and ( n C), which state a lower/upper bound on how many elements of C a model may contain. By replacing CIs with CRs, the complexity of satisfiability increases to NExpTimecomplete if the numbers occurring in the CRs are assumed to be encoded in binary [19]. With unary coding of numbers, it stays ExpTime-complete even w.r.t. CRs [19]. It should be noted that both qualified number restrictions and CRs (which generalize CIs) can be expressed in C2, the two-variable fragment of first-order logic with counting quantifiers [11,16], whose satisfiability problem is known to be NExpTime-complete [17]. Qualified number restrictions cannot relate cardinalities of different sets of role successors to one another, but can only compare the number of role successors (satisfying certain properties) of an individual against a fixed natural number. To overcome this limitation, in [1] we extended ALCQ by enabling the statement of restrictions on role successors using the quantifier-free fragment of Boolean Algebra with Presburger Arithmetic (QFBAPA) [14], in which one can express Boolean combinations of set constraints and numerical constraints comparing the cardinalities of finite sets. The resulting logic, called ALCSCC, strictly extends the expressive power of ALCQ. In [1] it is shown that the ALCSCC concept description succ(jrj = jsj), which describes individuals having the same number of r-successors as s-successors, cannot be expressed in ALCQ. In addition, it has been shown in [5] that succ(jr \ Aj = jr \ :Aj), the ALCSCC concept ? Supported by DFG in TRR 248 (CPEC, grant 389792660) and RTG 1763 (QuantLA). Copyright © 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).

-

describing individuals whose number of r-successors belonging to A is the same as the number of r-successors not belonging to A, is not even expressible in firstorder logic. In spite of this considerable increase in expressive power, we were able to show in [ 1 ] that there is no increase in complexity: like for ALCQ, the complexity of the satisfiability problem in ALCSCC is PSpace-complete without CIs and ExpTime-complete w.r.t. CIs. The “in PSpace” result can also be derived from previous work [ 9 ] on modal logics with Presburger constraints, while the “in ExpTime” result is a novel contribution of [ 1 ].

Just like classical number restrictions, CRs can only relate the cardinality of a concept to a fixed number. In [ 7 ] we have introduced and investigated a generalization of CRs, which we called extended cardinality constraints (ECBoxes). The main idea was again to use QFBAPA to formulate and combine these constraints. It is shown in [ 7 ] that, in the DL ALC, the complexity of reasoning w.r.t. extended cardinality constraints (NExpTime for binary coding of numbers), is the same as for reasoning w.r.t. CRs. Moreover, we identified a special class of ECBoxes called restricted cardinality constraints (RCBoxes), which can express CIs but not CRs, and showed that the complexity of reasoning is lowered to ExpTime if ECBoxes are replaced with RCBoxes. The NExpTime upper bound for the extended case can actually be inferred from the NExpTime upper bound in [ 21 ] for a more expressive logic with n-ary relations and function symbols, but the ExpTime upper bound for the restricted case is a novel result.

In [ 2,3 ], we have combined the work in [ 1 ] and [ 7 ] by considering extended cardinality constraints in ALCSCC. This turned out to be non-trivial since the local cardinality constraints of ALCSCC may interact with the global ones in the extended cardinality constraints. Nevertheless, we were able to show that the complexity results (NExpTime-complete in general, and ExpTime-complete in the restricted case) hold not only for ALC, but also for ALCSCC.

The purpose of the paper [ 6 ], whose results this abstract summarizes, is twofold. On the one hand, after giving a compact representation of the known complexity results for the DLs with extended counting facilities mentioned above, we prove that those bounds are preserved in a setting where arbitrary rather than just finite models are considered. On the other hand, we investigate in detail the expressive power of these DLs over arbitrary models.

A first step in this direction had already been made in [ 5 ] for number restrictions over role successors. There, to ease the comparison with classical DLs such as ALCQ, where one usually employs a semantics based on arbitrary rather than finite models, we considered variants of QFBAPA and ALCSCC (called QFBAPA1 and ALCSCC1) that allow for possibly infinite sets and interpretations, respectively. After transferring the known complexity results for QFBAPA and ALCSCC to these variants, we examined their expressive power using appropriate bisimulation relations. Basically, we showed there that ALCSCC1 concepts can go beyond first-order logic (recall the concept description succ(jr \ Aj = jr \ :Aj) mentioned earlier) and determined a sub-logic of ALCSCC1, called ALCCQU , that corresponds to the first-order fragment of ALCSCC1. We also proved that ALCCQU is more expressive than ALCQ and ALCQ

FOL (

DLs ALCQt = ALCCQU = ALCSCC1 \ FOL

ALCSCC1 equivalent to an extension of ALCQ, called ALCQt, where number restrictions range over (safe) role types rather than role names. Figure 1 gives an overview of the expressivity results contained in [ 5 ].

In [ 6 ], we recall these results, and then extend them to TBoxes, CBoxes, RCBoxes, and ECBoxes, by adapting methods and ideas from [ 15 ]. As in [ 5 ], we consider the semantic variants QFBAPA1 and ALCSCC1, rather than their finite counterparts, and derive the expressivity hierarchy depicted in Figure 2 using suited bisimulation relations and the 0-1 law for first-order sentences [ 10 ].

Detailed definitions of the aforementioned formalisms, as well as proofs of the expressivity results mentioned in this abstract, have been published in [ 6 ].

References

1. Franz Baader . A new description logic with set constraints and cardinality constraints on role successors . In Clare Dixon and Marcelo Finger , editors, Proc. of the 11th Int. Symposium on Frontiers of Combining Systems (FroCoS'17) , volume 10483 of Lecture Notes in Computer Science, pages 43 - 59 , Brasília, Brazil, 2017 . Springer-Verlag.

2. Franz Baader . Expressive cardinality constraints on ALCSCC concepts . In Proc. of the 34th ACM/SIGAPP Symposium On Applied Computing (SAC'19) . ACM, 2019 .

3. Franz Baader . Expressive cardinality restrictions on concepts in a description logic with expressive number restrictions . ACM SIGAPP Applied Computing Review , 19 : 5 - 17 , 2019 .

4. Franz Baader , Martin Buchheit , and Bernhard Hollunder . Cardinality restrictions on concepts . Artificial Intelligence , 88 ( 1-2 ): 195 - 213 , 1996 .

5. Franz Baader and Filippo De Bortoli. On the expressive power of description logics with cardinality constraints on finite and infinite sets . In Andreas Herzig and Andrei Popescu , editors, Proc. of the 12th Int. Symposium on Frontiers of Combining Systems (FroCoS'19) , volume 11715 of Lecture Notes in Computer Science. Springer-Verlag, 2019 .

6. Franz Baader and Filippo De Bortoli. Description logics that count, and what they can and cannot count . In Laura Kovacs, Konstantin Korovin, and Giles Reger, editors, ANDREI-60. Automated New-era Deductive Reasoning Event in Iberia , volume 68 of EPiC Series in Computing, pages 1 - 25 . EasyChair, 2020 .

7. Franz Baader and Andreas Ecke . Extending the description logic ALC with more expressive cardinality constraints on concepts . In Proc. of the 3rd Global Conf. on Artificial Intelligence (GCAI'17) , volume 50 of EPiC Series in Computing, pages 6 - 19 . EasyChair, 2017 .

8. Alexander Borgida , Ronald J. Brachman , Deborah L. McGuinness , and Lori Alperin Resnick . CLASSIC: A structural data model for objects . In Proc. of the ACM SIGMOD Int. Conf. on Management of Data , pages 59 - 67 , 1989 .

9. Stéphane Demri and Denis Lugiez . Complexity of modal logics with Presburger constraints . J. Applied Logic , 8 ( 3 ): 233 - 252 , 2010 .

10. Ronald Fagin . Probabilities on finite models . Journal of Symbolic Logic , 41 ( 1 ): 50 - 58 , 1976 .

11. Erich Grädel , Martin Otto , and Eric Rosen . Two-variable logic with counting is decidable . In Proc. of the 12th IEEE Symp. on Logic in Computer Science (LICS'97) , pages 306 - 317 . IEEE Computer Society Press, 1997 .

12. Bernhard Hollunder and Franz Baader . Qualifying number restrictions in concept languages . In Proc. of the 2nd Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR'91) , pages 335 - 346 , 1991 .

13. Bernhard Hollunder , Werner Nutt, and Manfred Schmidt-Schauß. Subsumption algorithms for concept description languages . In Proc. of the 9th Eur. Conf. on Artificial Intelligence (ECAI'90) , pages 348 - 353 , London (United Kingdom), 1990 . Pitman.

14. Viktor Kuncak and Martin Rinard . Towards efficient satisfiability checking for boolean algebra with presburger arithmetic . In Frank Pfenning, editor, Automated Deduction - CADE-21, Lecture Notes in Computer Science , pages 215 - 230 . Springer Berlin Heidelberg, 2007 .

15. Carsten Lutz , Robert Piro, and Frank Wolter . Description Logic TBoxes: ModelTheoretic Characterizations and Rewritability . In IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence , Barcelona, Catalonia, Spain, July 16-22 , 2011 , pages 983 - 988 , 2011 . Long version available at https://arxiv.org/pdf/1104.2844.pdf.

16. Leszek Pacholski , Wieslaw Szwast, and Lidia Tendera . Complexity of two-variable logic with counting . In Proc. of the 12th IEEE Symp. on Logic in Computer Science (LICS'97) , pages 318 - 327 . IEEE Computer Society Press, 1997 .

17. Ian Pratt-Hartmann. Complexity of the two-variable fragment with counting quantifiers . J. of Logic, Language and Information , 14 ( 3 ): 369 - 395 , 2005 .

18. Stephan Tobies . A PSPACE algorithm for graded modal logic . In Harald Ganzinger, editor, Proc. of the 16th Int. Conf. on Automated Deduction (CADE'99) , volume 1632 of Lecture Notes in Artificial Intelligence , pages 52 - 66 . Springer-Verlag, 1999 .

19. Stephan Tobies . The complexity of reasoning with cardinality restrictions and nominals in expressive description logics . J. of Artificial Intelligence Research , 12 : 199 - 217 , 2000 .

20. Stephan Tobies . Complexity Results and Practical Algorithms for Logics in Knowledge Representation . PhD thesis , LuFG Theoretical Computer Science, RWTHAachen, Germany, 2001 .

21. Kuat Yessenov , Ruzica Piskac, and Viktor Kuncak . Collections, cardinalities, and relations . In Gilles Barthe and Manuel V. Hermenegildo, editors, Proc. of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'10) , volume 5944 of Lecture Notes in Computer Science, pages 380 - 395 . Springer-Verlag, 2010 .