1. Carral, D., Dragoste, I., Krotzsch, M.: Restricted chase (non)termination for existential rules with disjunctions. In: Proceedings of IJCAI , Melbourne, Australia (2017), to appear (https://iccl.inf.tu-dresden.de/web/Inproceedings3140)
The restricted chase is a sound and complete algorithm that solves conjunctive query answering over expressive, non-deterministic DL ontologies. The algorithm branches on disjunctive choices and computes all the possible inferences that have not already been satis ed, risking non-termination.
For this reason, we develop new acyclicity conditions [1] that guarantee restricted chase termination of a TBox over any ABox, by extending known acyclicity notions to the restricted disjunctive case. We put forward restricted joint acyclicity and the more general restricted model-summarizing acyclicity (RMSA), both of which can be checked in polynomial time. An even more general notion is restricted model-faithful acyclicity (RMFA), but checking membership of a DL ontology is ExpTime-complete. Moreover, we show that the complexity of query answering over acyclic ontologies is coN2ExpTime-complete.
Acyclicity conditions are su cient, but not necessary for termination. Thus, we introduce the rst cyclicity notion for non-termination of the oblivious and the restricted chase, which imply that there exists some ABox for which some chase tree would be in nite. Checking this condition is 2ExpTime-complete.
We conducted experiments on a large corpus of real-world ontologies to evaluate the empirical generality of our notions. Indeed, our acyclicity notions improve the generality of existing ones by 4:2% for deterministic ontologies and 9:2% for non-deterministic ones, with RMSA signi cantly improving over MSA. Moreover, combining cyclicity and acylicity notions allows us to decide restricted chase termination of 96:3% ontologies in the deterministic case (from 72:4% using only MFA) and 42:4% in the non-deterministic one (from 25:2% with MFA), respectively. The high percentage of unclassi ed ontologies in the non-deterministic case can be explained by the loose approximation of disjunctive axioms consequences when determining facts necessarily entailed during the chase.
We present the rst systematic study about termination of the restricted chase on expressive, non-deterministic ontologies in which we characterize termination for a larger subset of real-world ontologies than in previous works. Moreover, we present a cyclicity notion that allows us to establish chase nontermination, thus assessing the space for improvement of acyclicity notions.
Our work also motivates and enables further research on e cient chase-based reasoning procedures for expressive, non-deterministic ontologies. Many tableaubased OWL reasoners already implement chase-like algorithms. We believe this is a highly promising direction in description logics and existential rules alike.