Fixed-Domain Reasoning for Description Logics

Abstract

Description logics (DLs) are currently a de facto standard in logic-based knowledge representation thanks to the last two decades of research and their use as the underpinning of standardized and widely adopted web ontology language (OWL), which also comes with the advantage of existing user-friendly modeling tools. It has, however, been observed that OWL and description logics are utilized by logically less skilled practitioners as constraint languages adopting a closed-world assumption, contrary to the open world semantics imposed by the classical de nitions and the standards. Therefore, we came up with an alternative formal semantics re ecting this \o -label use" of these widely adopted formalisms. To that end, we introduce the xed-domain semantics and discuss that this semantics gives rise to the interesting new inferencing task of model enumeration. We describe how the new semantics can be axiomatized in very expressive DLs. We thoroughly investigate the complexities for standard reasoning as well as query answering for a wide range of DLs. We present an implementation of a xed-domain DL reasoner based on the translation into answer set programming (ASP) and provide rst results that this tool is superior to alternative approaches when used on constraint-satisfaction-type problems.

-

Preferred knowledge representation formalisms are often the ones which are standardized, widely adopted and come with elaborate modeling tool support. One outstanding example for this is certainly the Web Ontology Language OWL [ 32 ]. Ontology editors like Protege [ 16 ] provide user-friendly interfaces and combined with the natural-language-like Manchester syntax [ 12 ] possess perspicuous access to an arguably complex and involved formalism.

This gives rise to scenarios in which OWL is chosen over other formalisms, even if the application scenario does not match the typical usage of this language. For example, the modeled problem might be of a constraint-satisfaction type which does not go well with OWL's standard semantics allowing for models of arbitrary size. Consider the 3-coloring problem as a short but representative constraint-satisfaction problem, for which one can easily envision some OWL axioms imposing the conditions on valid colorings of a given graph. Then, asking for consistency of the problem description is a natural task for OWL reasoners, asking for colorability as such can be cast into a satis ability problem, but asking for concrete colorings already requires reasoning capabilities none of the OWL reasoners we are aware of is furnished with.

To overcome these shortcomings, we propose xed-domain reasoning for description logics { a family of logics providing the logical underpinning of OWL and its sublanguages. By this intuitive and simple approach, we consider DLs under a non-standard model-theoretic semantics, modifying the modelhood condition by restricting the domain to an explicitly given xed nite set. We investigate the combined complexity of reasoning in the presence of a given xed domain for a wide range of description logics, for which we establish tight bounds for standard reasoning tasks as well as query answering for various query notions. While satis ability checking in OWL under the classical semantics is N2ExpTime-complete [ 15 ] and query answering is not even known to be decidable, we show that these problems under the xed-domain semantics are merely NP-complete and 2P-complete, respectively.

We note that the xed-domain condition can be axiomatized in OWL. Still, employing the axiomatization, existing OWL reasoners struggle on xed-domain reasoning, due to the heavy combinatorics involved. Therefore, we propose a di erent approach and de ne a translation of SROIQ knowledge bases (the logical counterparts to OWL ontologies) into answer set programming (ASP) [ 4 ], such that the set of ( xed-domain) models coincides with the set of answer-sets of the obtained program. This allows us to use existing ASP solvers (see [ 5 ] for an overview) for xed-domain reasoning { including standard as well as nonstandard tasks. For the proposed translation, we provide an implementation and present preliminary evaluations on typical constraint-satisfaction-type problems. This not only demonstrates feasibility, but also suggests signi cant improvement compared to the axiomatized approach using highly optimized OWL reasoners. 2

Preliminaries

We assume the reader to be familiar with the basics of description logics (DLs) [ 2, 26 ]. Nevertheless, we recall some basics of the description logic SROIQ as well as the class of queries we consider in this work.

OWL 2 DL, the version of the Web Ontology Language we focus on, is de ned based on the description logic SROIQ (for details see [ 13 ]). Let NI , NC , and NR be nite, disjoint sets called individual names, concept names and role names respectively. These atomic entities can be used to form complex ones. A SROIQ knowledge base is a tuple (A; T ; R) where A is a SROIQ ABox, T is a SROIQ TBox and R is a SROIQ RBox, and we will refer to each TBox axiom as general concept inclusion (GCI). The semantics of SROIQ is de ned via interpretations I = ( I ; I ) composed of a non-empty set I called the domain of I and a function I mapping individual names to elements of I , concept names to subsets of I and role names to subsets of I I . This mapping is extended to complex role and concept expressions and nally used to de ne satisfaction of axioms (for details see [ 13 ]). We say that I satis es a knowledge base K = (A; T ; R) (or I is a model of K, written: I j= K), if it satis es all axioms of A, T , and R. We say that a knowledge base K entails an axiom (written K j= ) if all models of K are models of .

Boolean Datalog Queries Here we brie y introduce syntax and semantics of Datalog queries over description logic knowledge bases. A term can be a variable from a countably in nite set V of variables, or an element of NI . An atom has the form p(t1; : : : ; tn) where t1; : : : ; tn are terms and p is a predicate of arity n from a set of predicates containing NC (arity 1) and NR (arity 2) and containing a special predicate goal of arity 0. A Boolean Datalog query is a set of rst order logic Horn rules of the form 8X:a1 ^ : : : ^ ak ! a where a1; : : : ; an; a are atoms, but the predicate of a is not from NC or NR. X V denotes the set of variables occurring in the atoms. Given a DL interpretation I, and a Boolean Datalog query Q, an extended model for I and Q is a rst-order interpretation J over

I that coincides with I on the interpretation of NC and NR and satis es all the rules from Q. We say that Q matches I and write I j= Q if J j= goal for every extended model J for I and Q. For a DL knowledge base K, we say K entails Q i I j= Q for every model I of K. Bounded arity Datalog queries are classes of queries where the arity of the used predicates is bounded by some constant. A Boolean conjunctive query is a Boolean Datalog query with just one rule where a1; : : : ; an use only predicates from NC [ NR and a = goal . In that case, such a query can be equivalently written as the rst-order formula 9X:a1 ^ : : : ^ ak. 3

Models over Fixed Domains

In DLs, models can be of arbitrary cardinality. In many applications, however, the domain of interest is known to be nite. In fact, restricting reasoning to models of nite domain size (called nite model reasoning, a natural assumption in database theory), has already become the focus of intense studies in DLs [ 17, 6, 25, 27 ]. As opposed to assuming the domain to be merely nite (but of arbitrary, unknown size), we consider the case where the domain has an a priori known cardinality and use the term xed domain. We refer to such models as xed-domain models and argue that in many applications, this modi cation of the standard DL semantics represents a more intuitive de nition of what is considered and expected as a model of some knowledge base.

De nition 1 (Fixed-Domain Semantics). Given a DL knowledge base K and a non-empty nite set K NI , called xed domain, an interpretation I = ( I ; I ) is said to be K- xed (or just xed, if K is clear from the context), if I = K and aI = a for all a 2 K. Accordingly, we call an interpretation I a K-model of K, if I is a K- xed interpretation and I j= K. A knowledge base K is called K-satis able if it has a model over K. We say K K-entails an axiom (K j=fd ) if every K-model of K is also a model of .

Note that, under the xed-domain semantics, there is a one-to-one correspondence between K-interpretations and sets of ground facts. That is, for every K-interpretation I = ( I ; I ), we nd exactly one ABox AI with atomic concept assertions and role assertions de ned by AI := fr(a; b) j (a; b) 2 rI g [ fA(a) j a 2 AI g [ fIndc(a) j c 2 NI (K) n K and cI = ag and likewise, every such ABox A gives rise to a corresponding interpretation IA.1 This allows us to use ABoxes as convenient representations of models. Example 1. We brie y demonstrate the e ects of the xed-domain semantics as opposed to the nite-model semantics (with entailment j= n) and the classical semantics. Let K = (A; T ; R) and K = fa; bg with A = fA(a); A(b); s(a; b)g, T = f> v 9r:B; > v 61 r :>g, and R = fDis(s; r)g. First we note that K has a Kmodel I representable as AI = fA(a); A(b); B(a); B(b); s(a; b); r(a; a); r(b; b)g, thus K is satis able under all three semantics. Then = > v 9r:9r:B holds in all models of K, therefore K j= , K j= n , and K j=fd . Opposed to this, = > v B merely holds in all nite models, whence K j= n and K j=fd , but K 6j= . Finally, = > v 9r:Self only holds in all K-models, thus K j=fd , but K 6j= n and K 6j= .

Extraction & Enumeration of K-Models When performing knowledge base satis ability checking in DLs (the primary reasoning task usually considered), a model constructed by a reasoner merely serves as witness to claim satis ability, rather than as an accessible artifact. However, as mentioned before, our approach aims at scenarios 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. Then, retrieval of one, several, or all models is a natural task, as opposed to merely checking model existence. With model extraction we denote the task of materializing an identi ed model in order to be able to work with it, i.e. to inspect it in full detail and reuse it in downstream processes. The natural continuation of model extraction is to make all models explicit, performing model enumeration. Conveniently, for both tasks, we can use the introduced model representation via ABoxes. Most existing DL reasoning algorithms attempt to successively construct a model representation of a given knowledge base. However, most of the existing tableaux reasoners do not reveal the constructed model, besides the fact that models might end up being in nite such that an explicit representation is impossible. Regarding enumeration, we state that this task is not supported { not even implicitly { by any state-of-the-art DL reasoner, also due to the reason that in the standard case, the number of models is typically in nite and often even uncountable. We will use the notions of model extraction and enumeration as their meaning should be quite intuitive. Related thereto, the term model expansion is used in the general rst-order case, e.g. in the work of Mitchell and Ternovska [ 18 ]. There, an initial (partial) interpretation representing a problem instance is expanded to ultimately nd a model of the given theory. 1 For the other direction, I = fa; b j A(a) 2 AI or r(a; b) 2 AI g, and an individual c not occurring in I , we let cI = a, if Indc(a) 2 AI .

Example 2. We consider the 3-coloring problem for an undirected graph G = (V; E), encoded in K1 = (A1; T 1; R1), with T 1 = fN v Nr t Ng t Nb; Nr v 8edge:(Ng tNb); Ng v 8edge:(Nb tNr); Nb v 8edge:(Nr tNg); Nr v :Ng; Nr v :Nb; Ng v :Nbg. A1 = fN (vi) j 8vi 2 V = fv1; : : : ; vngg [ fedge(v; v0) j 8(v; v0) 2 Eg [ f:edge(v; v0) j 8(v; v0) 2 V V n Eg, and R1 = fSym(edge)g. Let K1 = fv1; : : : ; vng be the imposed xed domain. It is not hard to see, that there is a one-to-one correspondence between the K1 -models of K1 and the colorings of G.

Axiomatization of K-Models When introducing a new semantics for some logic, it is worthwhile to ask if existing reasoners can be used. Indeed, it is easy to see that, assuming K = fa1; : : : ; ang, adding the GCI > v fa1; : : : ; ang as well as the set of inequality axioms containing ai 6 aj with i < j to K will rule out all models of K, not having K as their domain. Denoting these additional axioms with F D, we then nd that K is K-satis able i K [ F D is satis able under the classical DL semantics and, likewise, K j=fd i K [ F D j= for any axiom . Consequently, any o -the-shelf SROIQ reasoner can be used for xed-domain reasoning, at least when it comes to the classical reasoning tasks.

However, the fact that the currently available DL reasoners are not optimized towards reasoning with axioms of the prescribed type (featuring disjunctions over potentially large sets of individuals) and that available reasoners do not support model extraction and model enumeration led us to develop an alternative computational approach based on ASP. 4

Complexity Analysis

The combined complexity of standard reasoning in SROIQ is known to be N2ExpTime-complete, both for arbitrary models and nite models [ 15 ]. Restricting to xed domains leads to a drastic drop in complexity. Contrarily, imposing xed domains on (allegedly) inexpressive fragments such as DL-Litecore, turns reasoning into a hard problem.

Therefore, let DLmin be a minimalistic description logic that merely allows TBox axioms of the form A v :B, with A; B 2 NC . Moreover, only atomic assertions of the form A(a) and r(a; b) are admitted. We rst demonstrate that satis ability checking in DLmin is NP-hard, allowing us to bequeath hardness up to more expressive DLs such as SROIQ. Subsequently, we demonstrate that xed-domain satis ability checking in SROIQ is in NP, and thus obtaining NP-completeness for all languages between DLmin and SROIQ. Proposition 1. The combined complexity of checking xed-domain satis ability of a DLmin knowledge base K = (A; T ) is NP-hard.

Proof. (Sketch) We obtain hardness by reducing the 3-colorability problem to the following DLmin axioms. Let G = (V; E) be the input graph. Then, for each node vi 2 V = fv1; : : : ; vng we introduce a concept name Vi, and encode the edges as disjointness axioms, such that T = fVi v :Vj j (vi; vj ) 2 E; 8i; j 2 f1; : : : ; ngg. The ABox A consists of the assertions Vi(ai) for each Vi 2 fV1; : : : ; Vng. Now let K = fr; g; bg, such that under any K- xed interpretation I, necessarily aiI 2 fr; g; bg, 1 i n. Consequently, G has a 3-coloring, i K = (A; T ) is

K-satis able. The reduction is linear in the size of G.

Proposition 2. The combined complexity of checking xed-domain satis ability of SROIQ knowledge bases is in NP.

Proof. (Sketch) Let K be a SROIQ knowledge base and K be the xed domain. To show membership, we note that after guessing a K- xed interpretation I, modelhood can be checked in polynomial time. For this we let C contain all the concept expressions occurring in K (including subexpressions). Furthermore, let R contain all role expressions and role chains (including subchains) occurring in K. Obviously, C and R are of polynomial size. Then, in a bottom-up fashion, we can compute the extension CI of every element C of C and the extension rI of every element r of R along the de ned semantics. Obviously, each such computation step requires only polynomial time. Finally, based on the computed extensions, every axiom of K can be checked { again in polynomial time. Combining these propositions yields the following theorem.

Theorem 1. Fixed-domain satis ability checking in any language between DLmin and SROIQ is NP-complete.

Note that this nding contrasts with the observation that xed-domain reasoning in rst-order logic is PSpace-complete. We omit the full proof here, just noting that membership and hardness can be easily shown based on the fact that checking modelhood in FOL is known to be PSpace-complete [ 31 ] and, for the membership part, keeping in mind that NPSpace = PSpace thanks to Savitch's Theorem [ 28 ]. This emphasizes the fact that, while the xed-domain restriction turns reasoning in FOL decidable, restricting to SROIQ still gives a further advantage in terms of complexity (assuming NP 6= PSpace). Query Entailment 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. We will start by showing a hardness result for a very minimalistic setting. Proposition 3. The combined complexity of junctive queries from a DLmin knowledge base is xed-domain entailment of con2P-hard.

Proof. We show hardness by providing a polynomial reduction from evaluation of quanti ed Boolean formulae of the form = 8p1; : : : ; p`9q1; : : : ; qm' such that ' is a Boolean formula where the propositional symbols are from the set fp1; : : : ; p`; q1; : : : ; qmg. Note that w.l.o.g. we can assume ' to be in conjunctive normal form, i.e. it has the shape W L1 ^ : : : ^ W Ln where the Li are sets of negated or unnegated propositional symbols.

Given such a formula , we now construct a DLmin knowledge base K, a domain K, and a conjunctive query Q (all of polynomial size) such that K

K-entails Q if and only if evaluates to true. We let K consist of elements dtrue and dfalse for all t 2 fp1; : : : ; p`; q1; : : : ; qmg, and K consist of the axioms: t t { InClauseL(dttrue) whenever t 2 L and InClauseL(dftalse) whenever :t 2 L { compatible(dttrue; dturue) and compatible(dftalse; dfalse) u for all ft; ug

fp1; : : : ; p`; q1; : : : ; qmg { compatible(dftalse; dtrue) and compatible(dttrue; dfualse)

u for all ft; ug fp1; : : : ; p`; q1; : : : ; qmg with t 6= u { Select (dt), Ct(dt) for all t 2 fp1; : : : ; p`g { Select (dttrue) and Select (dftalse) for all t 2 fq1; : : : ; qmg { Ct(dttrue), Ct(dftalse) for all t 2 fp1; : : : ; p`; q1; : : : ; qmg { Ct u Cu v ? for all ft; ug 2 fp1; : : : ; p`; q1; : : : ; qmg with t 6= u Finally, we let Q be the conjunctive query using the variables xL1 ; : : : ; xLn and consisting of the atoms InClauseL(xL), Select (xL) for all L 2 fL1; : : : ; Lng as well as compatible(xL; xL0 ) for all fL; L0g 2 fL1; : : : ; Lng.

We now sketch the argument why the above claimed correspondence holds. By construction, the minimal K-models I for every i 2 f1; : : : ; mg are exactly those where (next to the explicitly stated concept and role memberships) either dtpriue 2 Select I or dfpailse 2 Select I holds. Consequently Q is entailed, i for each of these models (representing all possible truth assignments to p1; : : : ; p`), one literal from every clause Li can be selected such that (a) this selection is consistent (i.e., no contradicting literals are selected) and (b) whenever a literal w.r.t. p1; : : : ; p` is selected, it must be the one corresponding with the model's prede ned truth assignment for these propositional symbols. However, this is the case exactly if is valid.

We continue by showing that even for very expressive DLs and query languages, query entailment under the xed domain semantics is still in the second level of the polynomial hierarchy.

Proposition 4. The combined complexity of the xed-domain entailment of bounded-arity Datalog queries from a SROIQ knowledge base is in 2P. Proof. Satisfaction of a bounded-arity Datalog query in a database (or nite interpretation) is in NP: there are only polynomially many ground atoms that can be derived, hence, whenever the query is entailed, there is a ground proof tree of polynomial size which can be veri ed in polynomial time. Consequently, xeddomain non-entailment of such a query Q from a SROIQ knowledge base K can be realized by (a) guessing an interpretation I (b) verifying I j= K in polynomial time (cf. the proof of Proposition 2) and (c) using an NP oracle to verify I 6j= Q. Consequently, checking xed-domain entailment is in coNPNP = 2P.

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) conjunctive 2-way regular path queries [ 7 ], positive 2-way regular path queries, (unions of) conjunctive nested 2-way regular path queries [ 3 ] and regular queries as dened in [ 24 ]. Combining the two propositions, we obtain the following theorem. Theorem 2. For any class of queries subsuming conjunctive queries and subsumed by bounded-arity Datalog queries and any DL subsuming DLmin and subsumed by SROIQ, the combined complexity of xed-domain query entailment is 2P-complete. 5

Practical Fixed-Domain Reasoning

In Section 3 we already claimed that available reasoners perform poorly on knowledge bases when axiomatizing the xed-domain semantics, and we support this statement with an evaluation in the sequel (cf. Section 5.3). Thus, a more viable approach is required when considering practical reasoning. To this end, we propose an encoding of arbitrary SROIQ knowledge bases into answer set programs. This allows us to use existing ASP machinery to perform both standard reasoning as well as the non-standard tasks model extraction & enumeration and query entailment quite elegantly.

We review the basic notions of answer set programming [ 22 ] under the stable model semantics [ 10 ], for further details we refer to [ 4 ]. We consider atoms, predicates and terms as de ned in Section 2. Each term is either a variable or a constant from a domain U . An atom is ground if it is free of variables. BU denotes the set of all ground atoms over U . A (disjunctive) rule is of the form a1 _ _ an

b1; : : : ; bk; not bk+1; : : : ; not bm, with n 0; m k 0, n + m > 0, where a1; : : : ; an, b1; : : : ; bm are atoms, and \not " stands for default negation. The head of is the set H( ) = fa1; : : : ; ang and the body of is B( ) = fb1; : : : ; bk; not bk+1; : : : ; not bmg. Furthermore, B+( ) = fb1; : : : ; bkg and B ( ) = fbk+1; : : : ; bmg. An interpretation I BU satis es a ground rule i H( ) \ I 6= ; whenever B+( ) I, B ( ) \ I = ;. I satis es a ground program , if each 2 is satis ed by I. A non-ground rule (resp., a program ) is satis ed by an interpretation I i I satis es all groundings of (resp., Gr ( )). I BU is an answer-set of i it is a subset-minimal set satisfying the reduct I = fH( ) B+( ) j I \ B ( ) = ;; 2 Gr ( )g. For a program , we denote the set of its answer-sets by AS( ). 5.1

ASP Encodings of DL Knowledge Bases Due to the identi ed complexity results, our ASP based approach suits perfectly for all involved reasoning tasks [ 4 ]. Intuitively, the set of all K-interpretations de nes a search space, which can be traversed searching for K-models, guided by appropriate constraints. We thus propose a translation (K) for any SROIQ knowledge base K; i.e. (K) = gen(K) [ chk(K), consisting of a generating part gen(K) that de nes all potential candidate interpretations, and a constraining part chk(K) that rules out interpretations violating axioms in K. However, we can only sketch the translation and refer to [ 8 ], where we introduced the main idea of the translation already.

The knowledge base is required to be in normalized form, obtained by a modi ed structural transformation (K), based on the one proposed in [ 21 ]. A GCI is normalized, if it is of the form > v Fin=1 Ci, where Ci is of the form B, fag, 8r:B, 9r:Self , :9r:Self , n r:B, or n r:B, for B a literal concept, r a role, and n a positive integer. A normalized knowledge base (K) is a modelconservative extension of K, i.e. every ( K-) model of (K) is a ( K-) model of K and every ( K-) model of K can be turned into a ( K-) model of (K) by nding appropriate interpretations for the concepts and roles introduced by . Thereby it is straightforward to extract a model for K, given a model of (K). Candidate Generation Following the generate & test paradigm, we let gen(K) be the program that generates (all) possible interpretations over K; i.e. for each concept name A, role name r, and individual a all possible extensions over K are generated. Thus, an answer-set A of gen(K) directly induces an interpretation IA of K over the xed-domain K. We denote the set of all interpretations of K over K with BK.

Proposition 5. Let K be a SROIQ knowledge base and gen(K) the obtained logic program. Then, it holds that BK coincides with the set of all answer-sets of gen(K).

Axiom Encoding For the test part, we turn each axiom 2 T [ R into a constraint, ultimately ruling out those candidate interpretations not satisfying , whence chk(K) = chk(T ) [ chk(R). Since each 2 T is of the form > v Fin=1 Ci, we simply turn it into a negative constraint of the form din=1 :Ci v ?, and add its direct translation to chk(T ). Role assertions and role inclusion axioms are also turned into constraints, and we add their direct translation to chk(R).

Theorem 3. For any normalized SROIQ knowledge base K = (A; T ; R) and its translation (K), it holds AS( (K)) = fB j B 2 BK and IB j= Kg.

With this theorem in place, we bene t from the translation in many aspects. Most notably, in addition to the standard DL reasoning tasks, model extraction and model enumeration can be carried out without additional e orts, since both are natural tasks for answer set solvers. Moreover, all mentioned query formalisms can be straightforwardly expressed in a rule-based way, whence integration in our framework is immediate.

Example 3. We reconsider K1 from Example 2. The axioms (a) N v Nr tNg tNb and (b) Nr v 8edge:(Ng t Nb), yield the following constraints:

N (X); not Nr(X); not Ng(X); not Nb(X):

Nr(X); edge(X; Y ); not ANgtNb (Y ):

ANgtNb (X); not Ng(X); not Nb(X):

(1) (2) (3) Due to normalization, (b) results in constraints (2) & (3), ensuring that if there is an edge from some red node X to Y , necessarily Y is either green or blue. We implemented our translation based approach as an open-source tool { named Wolpertinger.2 The obtained logic programs can be evaluated with most modern ASP solvers. However, the evaluation was conducted using Clingo [ 9 ] for grounding and solving, since it currently is the most prominent solver leading the latest competitions [ 5 ]. We present preliminary evaluation results based on simple ontologies, encoding constraint-satisfaction-type combinatorial problems. Existing OWL ontologies typically used for benchmarking, e.g. SNOMED or GALEN [ 29, 23 ], do not t our purpose, since they are modeled with the classical semantics in mind and often have little or no ABox information.

Our tests provide runtimes compared to the popular HermiT reasoner [ 11 ] and Konclude[ 30 ]. Whereas a direct comparison would not be fair, the conducted tests shall merely show the feasibility of our approach in comparison to standard DL reasoners using the axiomatization. In particular we focus on model enumeration, for which we can not conduct any comparison with existing DL reasoners. The evaluation itself is conducted on a standard desktop machine (Unix operating system, 2:7 Ghz Intel Core i5 Processor, 8 GB memory and standard Java-VM settings). Unsatis ability We construct an unsatis able knowledge base Kn = (An; T n; ;), with T n = fA1 v 9r:A2; : : : ; An v 9r:An+1; Ai u Aj v ? j 1 i < j n + 1g and An = fA1(a1); >(a1); : : : ; >(an)g, together with the xed-domain

K = fa1; : : : ; ang. Inspired by common pigeonhole-type problems, we have Kn enforce an r-chain of length n + 1 without repeating elements, yet, having xed

K to n elements such a model cannot exist. Table 1 depicts the runtimes for detecting unsatis ability of Kn, for increasing n. The durations correspond to the pure solving time as stated by the tools (including grounding in the case of Clingo), and neglecting pre-processing time. As the gures suggest, Kn is a potential worst-case scenario, where any of the tools is doomed to test all combinations. Whereas Wolpertinger is faster in claiming inconsistency in all cases up to K10, HermiT is slightly faster up from K11 { both leaving Konclude behind. However, K12 is already beyond a feasible time bound for all reasoners. Model Extraction and Enumeration With Table 2, we next provide some gures for model extraction and partial enumeration (retrieving a given number of K models). To this end, we created a knowledge base modeling fully and correctly lled Sudokus, featuring 108 named individuals, 13 concept names and 1 role name. When invoking a satis ability test on this knowledge base (axiomatized) using HermiT & Konclude, no answer was given within 15 minutes. On average, a solution for a given Sudoku instance is provided in around 7 seconds, of which more than 6 seconds are needed for grounding, while the actual solving is done in 2 https://github.com/wolpertinger-reasoner/Wolpertinger less than 0:1 seconds. For model enumeration, we used the knowledge base but removed information concerning pre- lled cells, turning the task into generating new Sudoku instances. The size of the grounded program is 20 MB, which takes around 6 seconds to obtain, as re ected in Table 2. 6

Conclusion

For OWL ontologies which represent constraint-type problems, the xed-domain semantics allows to con ne modelhood of interpretations towards more intuitional models. Although modeling features are limited, we argue that quite large and involved problem scenarios can be modeled in OWL ontologies. Clearly, evaluations of our system with respect to such ontologies remain as imperative issue. Moreover, we will consider translations into other formalisms, such as pure CSP languages, or even SAT, as future work. While remaining in monotonic waters, prospective considerations are in the direction of non-monotonic semantics. As such, rule-based extensions of OWL { monotonic [ 14, 20 ] or nonmonotonic [ 19, 1 ] { should be straightforward to accommodate. Moreover, we plan to incorporate typical ontology engineering tasks such as explanation and axiom pinpointing into our ASP-based framework.

Acknowledgements

We are grateful for all the valuable feedback from our colleagues and the anonymous workshop reviewers, which helped greatly to improve this work.

References

1. Alferes , J.J. , Knorr , M. , Swift , T. : Query-Driven Procedures for Hybrid MKNF Knowledge Bases . ACM Transactions on Computational Logic 14 ( 2 ), 16 :1{ 16 : 43 ( 2013 )

2. Baader , F. , Calvanese , D. , McGuinness , D. , Nardi , D. , Patel-Schneider , P. : The Description Logic Handbook: Theory, Implementation, and Applications . Cambridge University Press, second edn. ( 2007 )

3. Bienvenu , M. , Calvanese , D. , Ortiz , M. , Simkus , M. : Nested regular path queries in description logics . In: Baral, C. , Giacomo , G.D. , Eiter , T. (eds.) Proc. of the 14th Conference on Principles of Knowledge Representation and Reasoning (KR 2014 ). AAAI Press ( 2014 )

4. Brewka , G. , Eiter , T. , Truszczynski , M. : Answer set programming at a glance . Commun. ACM 54 ( 12 ), 92 { 103 ( 2011 )

5. Calimeri , F. , Gebser , M. , Maratea , M. , Ricca , F. : Design and results of the 5th answer set programming competition . Artif. Intell . 231 , 151 { 181 ( 2016 )

6. Calvanese , D. : Finite model reasoning in description logics . In: Padgham, L. , Franconi , E. , Gehrke , M. , McGuinness , D.L. , Patel-Schneider , P.F . (eds.) Proc. of the International Workshop on Description Logics (DL 1996 ). AAAI Technical Report , vol. WS-96-05 , pp. 25 { 36 . AAAI Press ( 1996 )

7. Calvanese , D. , Eiter , T. , Ortiz , M. : Regular path queries in expressive description logics with nominals . In: Boutilier, C . (ed.) Proc. of the 21st International Joint Conference on Arti cial Intelligence (IJCAI 2009 ). pp. 714 { 720 ( 2009 )

8. Gaggl , S.A. , Rudolph , S. , Schweizer , L. : Bound Your Models! How to Make OWL an ASP Modeling Language . In: Ellmauthaler, S. , Schulz , C. (eds.) Proc. of the International Workshop on User-Oriented Logic Programming (IULP 2015 ).

9. Gebser , M. , Roland Kaminski , B.K. , Schaub , M.O.T. , Schneider , M.T.: Potassco: The Potsdam Answer Set Solving Collection . AI Communications 24 ( 2 ), 107 { 124 ( 2011 )

10. Gelfond , M. , Lifschitz , V. : Classical negation in logic programs and disjunctive databases. New Generation Comput . 9 ( 3 /4), 365 { 386 ( 1991 )

11. Glimm , B. , Horrocks , I. , Motik , B. , Stoilos , G. , Wang , Z. : HermiT: an OWL 2 reasoner . Journal of Automated Reasoning 53 ( 3 ), 245 { 269 ( 2014 )

12. Horridge , M. , Patel-Schneider , P.F. : OWL 2 Web Ontology Language Manchester Syntax ( 2012 )

13. Horrocks , I. , Kutz , O. , Sattler , U. : The Even More Irresistible SROIQ . In: Doherty, P. , Mylopoulos , J. , Welty , C.A . (eds.) Proc. of the 10th International Conference on Principles of Knowledge Representation and Reasoning (KR 2006 ). pp. 57 { 67 . AAAI Press ( 2006 )

14. Horrocks , I. , Patel-Schneider , P.F. , Boley , H. , Tabet , S. , Grosof , B.N. , Dean , M.: SWRL: A Semantic Web Rule Language . W3C Member Submission (21 May 2004 )

15. Kazakov , Y. : RIQ and SROIQ are harder than SHOIQ . In: Brewka, G. , Lang , J . (eds.) Proc. of the 11th International Conference on Principles of Knowledge Representation and Reasoning (KR 2008 ). pp. 274 { 284 . AAAI Press ( 2008 )

16. Knublauch , H. , Musen , M.A. , Rector , A.L. : Editing Description Logic Ontologies with the Protege OWL Plugin . In: Haarslev, V. , Moller, R. (eds.) Proc. of the International Workshop on Description Logics (DL 2004 ). CEUR Workshop Proceedings , vol. 104 . CEUR-WS.org ( 2004 )

17. Lutz , C. , Sattler , U. , Tendera , L. : The complexity of nite model reasoning in description logics . Information and Computation 199 ( 1-2 ), 132 {171 (May 2005 )

18. Mitchell, D.G. , Ternovska , E.: A framework for representing and solving NP search problems . In: Veloso, M.M. , Kambhampati , S. (eds.) Proc. of the 20th National Conference on Arti cial Intelligence and the 17th Innovative Applications of Articial Intelligence Conference (AAAI 2005 ). pp. 430 { 435 . AAAI Press / The MIT Press ( 2005 )

19. Motik , B. , Rosati , R.: Reconciling description logics and rules . Journal of the ACM 57 ( 5 ) ( 2010 )

20. Motik , B. , Sattler , U. , Studer , R.: Query Answering for OWL DL with Rules . Journal of Web Semantics 3 ( 1 ), 41 { 60 ( 2005 )

21. Motik , B. , Shearer , R. , Horrocks , I. : Hypertableau Reasoning for Description Logics . Arti cial Intelligence Research 36 , 165 { 228 ( 2009 )

22. Niemela, I. : Logic programs with stable model semantics as a constraint programming paradigm . Ann. Math. Artif. Intell . 25 ( 3-4 ), 241 { 273 ( 1999 )

23. Rector , A. , Horrocks , I. : Experience building a large, re-usable medical ontology using a description logic with transitivity and concept inclusions . In: Proc. of the Workshop on Ontological Engineering ( 1997 )

24. Reutter , J.L. , Romero , M. , Vardi , M.Y.: Regular Queries on Graph Databases . In: Arenas, M. , Ugarte , M. (eds.) Proc. of the 18th International Conference on Database Theory (ICDT 2015 ). LIPIcs , vol. 31 , pp. 177 { 194 . Schloss Dagstuhl{ Leibniz-Zentrum fuer Informatik ( 2015 )

25. Rosati , R.: Finite Model Reasoning in DL-Lite . In: Bechhofer, S. , Hauswirth , M. , Ho mann , J., Koubarakis , M. (eds.) Proc. of the 5th European Semantic Web Conference (ESWC 2008 ). LNCS, vol. 5021 , p. 215 . Springer ( 2008 )

26. Rudolph , S. : Foundations of Description Logics . In: Polleres, A. , d'Amato , C. , Arenas , M. , Handschuh , S. , Kroner , P. , Ossowski , S. , Patel-Schneider , P.F. (eds.) Reasoning Web . 7th International Summer School 2011 , Tutorial Lectures . LNCS, vol. 6848 , pp. 76 { 136 . Springer ( 2011 )

27. Rudolph , S. : Undecidability Results for Database-Inspired Reasoning Problems in Very Expressive Description Logics . In: Baral, C. , Delgrande , J. , Wolter , F . (eds.) Proc. of the 15th International Conference on Principles of Knowledge Representation and Reasoning (KR 2016 ), AAAI Press ( 2016 ).

28. Savitch , W.J.: Relationships Between Nondeterministic and Deterministic Tape Complexities . J. Comput. Syst. Sci. 4 ( 2 ), 177 {192 (Apr 1970 )

29. Spackman , K.A. , Campbell , K.E. , Co^te, R.A.: SNOMED RT: a reference terminology for health care . In: AMIA 1997 , American Medical Informatics Association Annual Symposium . AMIA ( 1997 )

30. Steigmiller , A. , Liebig , T. , Glimm , B. : Konclude: System description . Journal of Web Semantics 27 , 78 { 85 ( 2014 )

31. Stockmeyer , L.J.: The Complexity of Decision Problems in Automata Theory and Logic . Ph.D. thesis , Massachusetts Institute of Technology ( 1974 )

32. W3C OWL Working Group: OWL 2 Web Ontology Language: Document Overview . W3C Recommendation ( 2009 )