Stable Model Semantics for Guarded Existential Rules and Description Logics

ABSTRACT. In this paper, we prove the decidability of stable model reasoning with guarded existential rules where rule bodies may contain negated atoms, as well as for reasoning using rules of the corresponding fragment of guarded Datalog+/-. In addition, we provide complexity results for these reasoning tasks (including conjunctive query answering) for a number of settings. Given that several lightweight description logics (in particular, DL-Lite, ELH, and OWL QL) can be directly translated to guardede Datalog+/-, we herewith obtain a direct stable model semantics for several description logics (DLs). This allows us to use negation (or complementation) directly in the axioms of a TBox, and to obtain a clear and natural semantics for such theories via their simple translation into an answer set program. We refer to this approach as to the "direct" stable model semantics in contrast to previous hybrid approaches that combine logic programming primitives with DL constructs, where the latter can be embedded into an answer set logic program, similar to generalized quantifiers (for example, the so-called dl-programs by Eiter et al. KR 2004; AIJ 2008).