Rules of inference play a major role in knowledge representation and reasoning, e.g., for consequence-based deduction calculi in DLs. Highly scalable rule engines are available for the popular rule language Datalog [2,3,4,8,12,15], and the ExpTime (combined) reasoning complexity of this logic suggests that these engines could be exploited for reasoning in DLs. However, solving ExpTime-complete problems by translation to Datalog requires polynomially large predicate arities [13] or exponentially many rules [6], neither of which is feasible. To overcome this issue, we propose Datalog(S) { an extension of Datalog with terms that represent sets { and we show that it can be used to express common DL reasoning calculi by a simple translation of inference rules. Inspired by the approach in [9], we encode ontologies as facts, while the deductive calculus is a xed Datalog(S) rule set. This extends and generalises an approach of Ortiz et al. [13] by making sets data-dependent, leading to ExpTime data complexity. The main novelty of our work is the insight that Datalog(S)-reasoning can be encoded in theories of existential rules outside any known class, but for which the standard chase procedure is guaranteed to terminate, producing a nite model in exponential (i.e., worst-case optimal) time. This is surprising, as all previously known concrete rule languages for which the chase terminates feature PTime data complexity [5,11], which is strictly too weak for implementing DL reasoning in this way. Our insight enables us to use existing rule reasoners for Datalog(S), and therefore for DLs, and we show by empirical evaluation that this can lead to feasible practical implementations even without extensive optimisation. Datalog(S) is de ned as a logic with two sorts: an object sort for regular domain elements, and a set sort for sets over the elements of this domain. We impose certain syntactic restrictions that ensure nite object domains, and therefore nite (though exponentially larger) set domains. We provide built-in functions fg and U for constructing set terms, and built-in predicates 2 and that can be used in rule premises for accessing the contents of sets. For example, the Datalog(S) rules below de ne a unary predicate for all non-empty sets of books: book (x) ! bookSet (fxg)
bookSet (X) ^ bookSet (Y ) ! bookSet (X U Y ) The number of sets in a canonical model of these rules is exponential in the number of elements classi ed as books in the input data, and this is the source of the additional expressive power of Datalog(S).
We illustrate our approach by encoding the ExpTime-complete reasoning
task of classi cation for a Horn-ALC TBox into a Datalog(S) program. We
? The full version of this paper has been accepted for publication at IJCAI'19 [
n = 0, H active,> v C 2 T , or (Ru) fH v Aigin=1 : n = 1, A1 v C 2 T , or
H v C n = 2, A1 u A2 v C 2 T (R9+) HHvv9RA:B : A v 9R:B 2 T (R9 ) H v 9RH:Kv BK v A : 9R:A v B 2 T (R9?) H v 9RH:Kv ?K v ? (R8) H v 9R:K H v A
H v 9R:(K u B) : A v 8R:B 2 T
Act(H) ^ a 2 H ! Sc(H; a)
Act(H) ^ ax v(c>; c) ! Sc(H; c) Sc(H; a1) ^ ax v(a1; c) ! Sc(H; c) Sc(H; a1) ^ Sc(H; a2)
^ ax uv(a1; a2; c) ! Sc(H; c) Sc(H; a) ^ ax v9(a; r; b) ! Ex (H; r; fbg) Ex (H; r; K) ^ Sc(K; a)
^ ax 9v(a; r; b) ! Sc(H; b) Ex (H; r; K) ^ Sc(K; c?) ! Sc(H; c?)
Ex (H; r; K) ^ Sc(H; a) Ex (H; r; fbg U K)
^ ax v8(a; r; b) ! ^ Act(fbg U K)
de ne a Horn-ALC TBox T as a set of axioms in the following normal form:
> v C, A v C, A u B v C, A v 9R:C, 9R:A v C, A v ?, A v 8R:C,
where A; B; C are concept names, R is a role name, and >; ? are the top and
bottom concepts. Classi cation is the task of computing all axioms of the form
A v C that are entailed by T . We consider the consequence-driven classi cation
method for Horn-ALC proposed in [
This classi cation calculus can be encoded as a Datalog(S) program
consisting of the rule set R shown Figure 1 (right), and a set of facts F (T ) encoding
the axioms in the input TBox: for example, an axiom A1 u A2 v C 2 T will
be encoded as a fact ax uv(A1; A2; C). Each of the Datalog(S) rules in the right
of Figure 1 corresponds to the inference rule on its left, where conjunctions are
represented as sets, predicates Sc and Ex encode inferences, and predicate Act
signals active conjunctions. These can be initialised by adding cn(a) to F (T ) for
each concept name a in T , and adding the rule cn(a) ! Act (fag) to R. Rule
(R ) shows how adding a concept name B to a conjunction of concept names K
8
can be encoded as the set union fBg U K, which results in a new active set. The
semantics of Datalog(S) rule set R can be captured by a set of existential rules for
which a standard chase variant that prioritises non-generating rules [
In summary, our proposed language Datalog(S) can be used to translate algorithms of ExpTime-complete data complexity into programs with a xed set of existential rules. Besides providing an elegant, fully-declarative implementation for DL reasoning, our approach can take advantage of rule engines capabilities. Acknolwedgements. This work is supported by Deutsche Forschungsgemeinschaft in project number 389792660 (TRR 248, Center for Perspicuous Systems) and Emmy Noether grant KR 4381/1-1 (DIAMOND).