Practical Fixed-Domain Reasoning for Description Logics – Extended Abstract Sarah Alice Gaggl, Sebastian Rudolph, and Lukas Schweizer Technische Universität Dresden, Computational Logic Group firstname.lastname@tu-dresden.de In this extended abstract, we report on our work on fixed-domain reasoning published at the 22nd European Conference on Artificial Intelligence [6]. Introduction. The Web Ontology Language OWL [13] comes with comprehen- sive modeling tool support. This sometimes leads to situations where OWL is the modeling paradigm chosen over other formalisms, even if the application scenario does not match the typical usage of this language. For example, prob- lems of a constraint-satisfaction nature do not go well with OWL’s standard semantics which allows for models of arbitrary size. Example 1 Assume we want to find out if, in a given graph (V, E), a Hamil- tonian path from vertex vα to vertex vω exists. Using one individual name v for every vertex v ∈ V , one might come up with the axioms (in description logic no- tation) noedge(v, v 0 ) whenever (v, v 0 ) ∈ / E, as well as > v ≤1edgeonpath.> u ≤1.edgeonpath− .> and ¬{vα }v∃edgeonpath− .> and ¬{vω }v∃edgeonpath.>, requiring that all nodes have exactly one incoming and one outgoing edge that is on the Hamiltonian path, except for vα which just has an outgoing and vω which just has an incoming such edge. The axiom {vα } v (∃edgeonpath.)|V |−1 {vω } expresses that there is an edgeonpath-path of length |V | − 1 from vα to vω . The axiom Dis(edgeonpath, noedge) ensures that the path can never go along “no-edges”. Under the usual semantics, however, this set of axioms is always sat- isfiable since models may contain “anonymous” elements that do not correspond to any of the node individual names. The given formalisation is only appropriate if we restrict to models with domain V . To overcome these shortcomings, we propose fixed-domain reasoning for de- scription logics (DLs), imposing a non-standard model-theoretic semantics that restricts the domain to an explicitly given, fixed finite set. Models over Fixed Domains. In DLs, models can be of arbitrary cardinality. In many applications, however, the domain of interest is known to be finite. In fact, restricting reasoning to models of finite domain size (called finite model reasoning, a natural assumption in database theory), has already become the focus of intense studies in DLs [4, 11]. As opposed to assuming the domain to be merely finite (but of arbitrary, unknown size), we consider the case where the domain has an a priori known cardinality and use the term fixed domain. Definition 1 (Fixed-Domain Semantics). Given a non-empty finite set ∆ of individual names, called fixed domain, an interpretation I = (∆I , ·I ) is said to be ∆-fixed (or just fixed, if ∆ is clear from the context), if ∆I = ∆ and aI = a for all a ∈ ∆. Accordingly, for a DL knowledge base K, we call an interpretation I a ∆-model of K, if I is a ∆-fixed interpretation and I |= K. A knowledge base K is called ∆-satisfiable if it has a ∆-model. Enumeration of ∆-Models. As mentioned before, our approach aims at sce- narios like constraint satisfaction problems where a knowledge base is a formal problem description for which each model represents one solution; in particular the domain is part of the problem description and hence fixed a-priori. Then, retrieval of one, several, or all models is a natural task, as opposed to merely checking model existence. We let model enumeration denote the task of making the ∆-models of a knowledge base explicit. Axiomatization of ∆-Models. When introducing a new semantics for some logic, it is worthwhile to ask if existing reasoners can be used. Obviously, as- suming ∆ = {a1 , . . . , an }, adding the DL axiom > v {a1 , . . . , an } as well as the set of inequality axioms containing ai 6= aj with i < j to K will (up to isomorphism) rule out all models of K, not having ∆ as their domain. Denoting these additional axioms with FD∆ , we find that K is ∆-satisfiable iff K ∪ FD∆ is satisfiable under the classical DL semantics. Consequently, any off-the-shelf SROIQ reasoner can be used for fixed-domain reasoning, at least when it comes to the classical reasoning tasks. Complexity Analysis. We report on complexities of classical reasoning tasks under the fixed-domain semantics. Note that, next to the size of the considered knowledge base the size of the domain |∆| contributes to the input size of the reasoning problems considered. The combined complexity of standard reasoning in SROIQ is known to be N2ExpTime-complete, both for arbitrary models and finite models [9]. Restrict- ing to fixed domains leads to a drastic drop in complexity. Contrarily, imposing fixed domains on (allegedly) inexpressive fragments such as DL-Litecore , turns reasoning into a harder problem. Let DLmin be a minimalistic description logic that merely allows TBox axioms of the form A v ¬B, with A, B ∈ NC . Moreover, only atomic assertions of the form A(a) and r(a, b) are admitted. Theorem 1. Fixed-domain satisfiability checking in any language between DLmin and SROIQ is NP-complete. We next consider the complexity of query entailment for DLs. Again, we will notice a very uniform behavior over a wide range of DLs and query types. Bounded-arity Datalog queries over DLs are rather expressive, they subsume many of the prominent query classes in knowledge representation and databases, including (unions of) conjunctive queries, positive queries, (unions of) conjunc- tive 2-way regular path queries [5], positive 2-way regular path queries, (unions of) conjunctive nested 2-way regular path queries [1], and regular queries as defined in [10]. We obtain the following theorem. Theorem 2. For any class of queries subsuming conjunctive queries and sub- sumed by bounded-arity Datalog queries and any DL subsuming DLmin and sub- sumed by SROIQ, the combined complexity of fixed-domain query entailment is ΠP2 -complete. Practical Fixed-Domain Reasoning. When axiomatizing the fixed-domain semantics, available OWL reasoners struggle with standard reasoning, and we supported this statement with an evaluation. Thus, a more viable approach is re- quired for realizing fixed-domain reasoning. To this end, we propose an encoding of arbitrary SROIQ knowledge bases into answer set programming (ASP) [2]. This allows us to use existing ASP machinery to perform both standard reason- ing as well as the non-standard tasks model enumeration and query entailment quite elegantly. We now briefly sketch how reasoning tasks w.r.t. the fixed-domain seman- tics can be encoded by ASP. Intuitively, the set of all ∆-interpretations defines a search space, which can be traversed searching for ∆-models, guided by ap- propriate constraints. We thus propose a translation Π(K, ∆) for any SROIQ knowledge base K; i.e. Π(K, ∆) = Πgen (∆) ∪ Πchk (K), consisting of a generating part Πgen (∆) that defines all potential candidate interpretations using so-called guessing rules, and a constraining part Πchk (K) containing only integrity con- straints (i.e., rules with empty heads) that rules out interpretations violating axioms in K. We implemented our translation based approach as an open-source tool – named Wolpertinger.1 The obtained logic programs can be evaluated with most modern ASP solvers. However, the evaluation was conducted using Clingo [7] for grounding and solving, since it is currently the most prominent solver leading the latest competitions [3]. For satisfiability checking, we conducted some preliminary tests, comparing our tool to the popular HermiT and Konclude reasoners [8, 12]. Both are full OWL 2 DL reasoners and are leading the latest competitions. We are aware that these reasoners are designed for and optimized toward open-world scenarios, the conducted tests shall merely show the feasibility of our approach in comparison to standard DL reasoners using the previously discussed axiomatization. Among other experiments, we created a knowledge base modeling fully and correctly filled Sudokus, beginning with a 6×6 field, consisting of 64 individuals, 13 concept names and 1 role name, then extending the size to a 9 × 9 field featuring 108 named individuals. While HermiT & Konclude were still able to detect satisfiability for the 6×6 case, invoking a satisfiability test on the 9×9 case did not yield any answer within 30 minutes. In both cases Wolpertinger detected satisfiability with reasonable runtimes of below 10 seconds. For model enumeration, we used the knowledge base for the 9×9 Sudoku and turned the task into generating new Sudoku instances. We observed that, besides 1 https://github.com/wolpertinger-reasoner/Wolpertinger a constant time of around 6 seconds required for grounding, even requesting 106 models is reasonably efficient, i.e., it requires less than 5 minutes. Conclusion and Future Work. The fixed-domain semantics allows to confine modelhood of interpretations to models of the right form, for OWL ontologies which represent constraint-type problems. Although OWL still imposes some restrictions regarding expressivity (e.g., by restricting the arity of the used pred- icates to 1 and 2), we argue that quite large and involved problem scenarios can be modeled by OWL ontologies. Clearly, more comprehensive evaluations of our system with respect to such ontologies remain as imperative issue. Moreover, translations of fixed-domain reasoning problems into other formalisms are con- ceivable, including pure CSP languages or even SAT, which would have to be implemented and compared against the ASP approach. Another interesting strand of research would be to consider extensions of the source formalism, e.g. by non-monotonic features. As ASP itself is a non- monotonic logic programming formalism, rule-based extensions of OWL – mono- tonic or non-monotonic – should be straightforward to accommodate. Finally, we plan to incorporate typical ontology engineering tasks such as explanation and axiom pinpointing into our ASP-based framework. References 1. M. Bienvenu, D. Calvanese, M. Ortiz, and M. Simkus, ‘Nested regular path queries in description logics’, in Proc. KR (2014). 2. Gerhard Brewka, Thomas Eiter, and Miroslaw Truszczyński, ‘Answer set program- ming at a glance’, Commun. ACM, 54(12), 92–103, (2011). 3. F. Calimeri, M. Gebser, M. Maratea, and F. Ricca, ‘Design and results of the 5th answer set programming competition’, Artif. Intell., 231, 151–181, (2016). 4. D. Calvanese, ‘Finite model reasoning in description logics’, in Proc. DL (1996). 5. D. Calvanese, T. Eiter, and M. Ortiz, ‘Regular path queries in expressive descrip- tion logics with nominals’, in Proc. IJCAI (2009). 6. S. A. Gaggl, S. Rudolph, and L. Schweizer, ‘Fixed-domain reasoning for description logics’, in Proc. ECAI (2016). 7. M. Gebser, B. Kaufmann, R. Kaminski, M. Ostrowski, T. Schaub, and M. T. Schneider, ‘Potassco: The Potsdam Answer Set Solving Collection’, AI Communi- cations, 24(2), 107–124, (2011). 8. B. Glimm, I. Horrocks, B. Motik, G. Stoilos, and Z. Wang, ‘HermiT: an OWL 2 reasoner’, Journal of Automated Reasoning, 53(3), 245–269, (2014). 9. Y. Kazakov, ‘RIQ and SROIQ are harder than SHOIQ’, in Proc. KR (2008). 10. J. L. Reutter, M. Romero, and M. Y. Vardi, ‘Regular Queries on Graph Databases’, in Proc. ICDT (2015). 11. S. Rudolph, ‘Undecidability results for database-inspired reasoning problems in very expressive description logics’, in Proc. KR (2016). 12. A. Steigmiller, T. Liebig, and B. Glimm, ‘Konclude: System description’, Journal of Web Semantics, 27, 78–85, (2014). 13. W3C OWL Working Group, OWL 2 Web Ontology Language: Document Overview, W3C Recommendation, 2009.