In this extended abstract, we report on our work on xed-domain reasoning published at the 22nd European Conference on Arti cial Intelligence [6]. Introduction. The Web Ontology Language OWL [13] comes with comprehensive 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, problems 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 nd out if, in a given graph (V; E), a Hamiltonian path from vertex v to vertex v! exists. Using one individual name v for every vertex v 2 V , one might come up with the axioms (in description logic notation) noedge(v; v0) whenever (v; v0) 2= E, as well as > v 1edgeonpath:> u 1:edgeonpath :> and :fv gv9edgeonpath :> and :fv!gv9edgeonpath:>, 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 fv g v (9edgeonpath:)jV j 1fv!g expresses that there is an edgeonpath-path of length jV j 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 satis able 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 .
De nition 1 (Fixed-Domain Semantics). Given a non-empty nite set of individual names, called xed domain, an interpretation I = ( I ; I ) is said to be - xed (or just xed, if is clear from the context), if I = and aI = a for all a 2 . Accordingly, for a DL knowledge base K, we call an interpretation I a -model of K, if I is a - xed interpretation and I j= K. A knowledge base K is called -satis able if it has a -model.
Enumeration of -Models. As mentioned before, our approach aims at scenarios 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 xed 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, assuming = fa1; : : : ; ang, adding the DL axiom > v fa1; : : : ; ang 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 F D , we nd that K is -satis able i K [ F D is satis able under the classical DL semantics. Consequently, any o -the-shelf SROIQ reasoner can be used for xed-domain reasoning, at least when it comes to the classical reasoning tasks.
Complexity Analysis. We report on complexities of classical reasoning tasks under the xed-domain semantics. Note that, next to the size of the considered knowledge base the size of the domain j j 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 nite models [
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.
Theorem 1. Fixed-domain satis ability 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)
conjunctive 2-way regular path queries [
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.
Practical Fixed-Domain Reasoning. When axiomatizing the xed-domain
semantics, available OWL reasoners struggle with standard reasoning, and we
supported this statement with an evaluation. Thus, a more viable approach is
required for realizing xed-domain reasoning. To this end, we propose an encoding
of arbitrary SROIQ knowledge bases into answer set programming (ASP) [
We now brie y sketch how reasoning tasks w.r.t. the xed-domain semantics can be encoded by ASP. Intuitively, the set of all -interpretations de nes a search space, which can be traversed searching for -models, guided by appropriate 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 de nes all potential candidate interpretations using so-called guessing rules, and a constraining part chk(K) containing only integrity constraints (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 [
For satis ability checking, we conducted some preliminary tests, comparing
our tool to the popular HermiT and Konclude reasoners [
Among other experiments, we created a knowledge base modeling fully and correctly lled Sudokus, beginning with a 6 6 eld, consisting of 64 individuals, 13 concept names and 1 role name, then extending the size to a 9 9 eld featuring 108 named individuals. While HermiT & Konclude were still able to detect satis ability for the 6 6 case, invoking a satis ability test on the 9 9 case did not yield any answer within 30 minutes. In both cases Wolpertinger detected satis ability 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 e cient, i.e., it requires less than 5 minutes. Conclusion and Future Work. The xed-domain semantics allows to con ne 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 predicates 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 xed-domain reasoning problems into other formalisms are conceivable, 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 nonmonotonic logic programming formalism, rule-based extensions of OWL { monotonic 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.