KR Conference 2012 Conference Paper
- Bernardo Cuenca Grau
- Ian Horrocks
- Markus Krötzsch
- Clemens Kupke
- Despoina Magka
- Boris Motik
- Zhe Wang
problem in both database and KR settings. This problem is undecidable (Beeri and Vardi 1981) in general, and it can be characterised using chase (Johnson and Klug 1984; Maier, Mendelzon, and Sagiv 1979), a technique closely related to the hypertableau calculus (Motik, Shearer, and Horrocks 2009). The chase extends in a forward-chaining manner the original set of facts by introducing facts implied by the rules. The result of the chase is called the universal model, and an arbitrary conjunctive query can be answered over the original set of facts and the rules by simply evaluating the query in the universal model. Rules with existentially quantified variables in the head— so-called generating rules—require the introduction of fresh individuals, and cyclic applications of generating rules may lead to non-termination; moreover, determining whether chase terminates on a set of rules and facts is undecidable. However, several decidable classes of existential rules have been identified, and the existing proposals can be classified into two main groups. In the first group, rules are restricted such that their (possibly infinite) universal models can be represented using finitary means. This group includes rules with universal models of bounded treewidth (Baget et al. 2011), guarded rules (Calı̀ et al. 2010), and ‘sticky’ rules (Calı̀, Gottlob, and Pieris 2011). In the second group, one uses a sufficient (but not necessary) acyclicity condition that ensures chase termination. Roughly speaking, acyclicity conditions analyse information flow between the rules to ensure that no cyclic applications of generating rules are possible. Weak acyclicity (WA) (Fagin et al. 2005) was one of the first such notions, and it was extended to safety (SF) (Meier, Schmidt, and Lausen 2009), stratification (ST) (Deutsch, Nash, and Remmel 2008), acyclicity of a graph of rule dependencies (aGRD) (Baget, Mugnier, and Thomazo 2011), joint acyclicity (JA) (Krötzsch and Rudolph 2011), and super-weak acyclicity (SWA) (Marnette 2009). Acyclicity conditions are relevant for at least two reasons. First, unlike guarded rules, acyclic rules can axiomatise structures of arbitrary shapes, as long as these structures are bounded in size. Second, the chase result for acyclic rules can be stored and manipulated as if it were a database. This is important in data exchange, where the goal is to materialise the transformed database. In this paper, we argue that acyclicity is also relevant for description logics (DLs), the KR formalisms underpin- Answering conjunctive queries (CQs) over a set of facts extended with existential rules is a key problem in knowledge representation and databases. This problem can be solved using the chase (aka materialisation) algorithm; however, CQ answering is undecidable for general existential rules, so the chase is not guaranteed to terminate. Several acyclicity conditions provide sufficient conditions for chase termination. In this paper, we present two novel such conditions—modelfaithful acyclicity (MFA) and model-summarising acyclicity (MSA)—that generalise many of the acyclicity conditions known so far in the literature. Materialisation provides the basis for several widely-used OWL 2 DL reasoners. In order to avoid termination problems, many of these systems handle only the OWL 2 RL profile of OWL 2 DL; furthermore, some systems go beyond OWL 2 RL, but they provide no termination guarantees. In this paper we investigate whether various acyclicity conditions can provide a principled and practical solution to these problems. On the theoretical side, we show that query answering for acyclic ontologies is of lower complexity than for general ontologies. On the practical side, we show that many of the commonly used OWL 2 DL ontologies are MSA, and that the facts obtained via materialisation are not too large. Thus, our results suggest that principled extensions to materialisationbased OWL 2 DL reasoners may be practically feasible.