=Paper=
{{Paper
|id=Vol-1350/paper-28
|storemode=property
|title=Nonmonotonic
Nominal Schemas Revisited
|pdfUrl=https://ceur-ws.org/Vol-1350/paper-28.pdf
|volume=Vol-1350
|dblpUrl=https://dblp.org/rec/conf/dlog/Knorr15
}}
==Nonmonotonic
Nominal Schemas Revisited==
https://ceur-ws.org/Vol-1350/paper-28.pdf
Nonmonotonic Nominal Schemas Revisited
Matthias Knorr
NOVA LINCS, Departamento de Informática, Faculdade de Ciências e Tecnologia,
Universidade Nova de Lisboa
Abstract. Recently, a very general description logic (DL) that extends SROIQ
(the DL underlying OWL 2 DL) at the same time with nominal schemas and epis-
temic modal operators has been proposed, which encompasses some of the most
prominent monotonic and non-monotonic rule languages, including Datalog un-
der the answer set semantics. A decidable fragment is also presented, but the
restricted language does not fully cover all formalisms encompassed by the com-
plete language. In this paper, we aim to remedy that by studying an alternative set
of restrictions to achieve decidability, and we show that the existing embeddings
of the formalisms covered by the full language can be adjusted accordingly.
1 Introduction
Extending Description Logics (DLs) with modeling features admitting non-monotonic
reasoning has been frequently requested in many application domains (see, e.g., [14]
for semantic matchmaking on annotations at electronic online marketplaces). In fact,
the vast amount of work dedicated to the topic may serve as a witness in its own right.
DLs have been extended, for example, with defaults [2], with notions of circumscription
[4,33], and epistemic reasoning provided by the inclusion of modal1 operators within
the language [8] or only in queries [29]. In addition, a plethora of approaches combine
DLs with (often non-monotonic) rules (see, e.g., [9,30,19] and references in their sec-
tions on related work). As these approaches are commonly of different expressivity and
based on quite advanced different formal grounds, a uniform overarching formalism
allowing the integration of possibly all the various modeling features is an extremely
complicated problem.
In [20], a very general DL language is introduced that extends the expressive DL
underlying OWL 2, SROIQ, with nominal schemas [24] and epistemic operators as
defined in [8] with the aim of integrating the W3C standards OWL [15] and (non-
monotonic) RIF [18] and their underlying formalisms, DLs and rule languages respec-
tively, thus contributing towards the goal of a unifying logic for the Semantic Web (as
foreseen in the well-known Semantic Web stack). The full language is in fact very ex-
pressive, capturing a variety of different formalisms, among them two based on MKNF
logics [27] that had been considered of different expressivity so far – MKNF DLs [8],
i.e., the epistemic extension of DLs, and Hybrid MKNF, one very expressive combi-
nation of DLs and non-monotonic rules. Though not the full language of the latter is
1
In the remainder of the paper, we use the terms modal and epistemic operator interchangeably
to refer to the same notion.
considered, coverage of Answer Set Programming [11] is ensured, arguably the most
widely used non-monotonic reasoning rule formalism.
A decidable fragment of the full language is also considered in [20], which is
strongly related to the one presented in [8]. In fact, the restrictions are such that the
tableau algorithm presented in [8] can in principle be re-used. As it turns out, how-
ever, the decidable language does not encompass all the formalisms for which coverage
within the full language is shown. While this does not invalidate the approach as such, in
particular, if one views such a unifying formalism mainly as a conceptual underpinning,
it is certainly undesired if one rather wants to use it for modeling and reasoning.
In this paper, we aim to solve this problem, i.e., we consider a different set of re-
strictions, for which we show that reasoning is decidable and that, at the same time,
encompasses all the formalisms discussed in [20] with only minor adjustments to the
previously presented embeddings. The principal idea builds on the usage of nominals
and nominal schemas, which are necessarily present in the language by design anyway,
to limit the applicability of concept inclusions containing modal operators. As an addi-
tional result, we believe that the new restrictions are more succinct and that the resulting
adaptation of the procedure for verifying the existence of models becomes less compli-
cated. To further simplify notation, here we do not consider the full language presented
in [20], which is based on SROIQ, but rather a language based on ALC with only the
minimally necessary extensions and we term this language eALCOV (see Sect. 2 for a
detailed explanation on the name). As we can show, such language is already expressive
enough to cover the desired non-monotonic modeling features.
The remainder of the paper proceeds as follows. In Sect. 2, we recall the syntax and
semantics of the DL eALCOV we consider here. We then introduce the new alterna-
tive conditions of so-called safe eALCOV KBs in Sect. 3 and we subsequently show
that these do ensure decidability of reasoning, i.e., checking (MKNF-)satisfiability. In
Sect. 4, we show that, with minor adaptations, the applied changes do now permit
coverage of the discussed formalisms in [20] within the decidable fragment (of safe
eALCOV KBs), before we conclude and discuss future work in Sect. 5.
2 Epistemic DLs
In this section, we recall the syntax and semantics of epistemic description logics (DLs)
from [20]. Here, we focus on a subset of the language considered in [20] to make the
presentation more concise and to ease the reading. Namely, we consider the epistemic
DL ALCKN F [8], which is ALC enhanced with epistemic operators, extended by nom-
inals, nominal schemas [24], and the universal role. Nominal schemas represent vari-
able nominals that can only be bound to known individuals, and the universal role can
be represented using role hierarchies and negation on roles [23], but as we want to keep
the presentation simple, we leave this implicit. Since the name of the resulting language
ALCOVKN F (or even ALCHOV(¬)KN F for the implicit encoding of the universal
role) following standard and historic patterns would be quite cumbersome, we propose
using the name eALCOV instead, which stands for epistemic ALCOV (including the
universal role). The term epistemic originates from the two epistemic/modal operators
K and A, where K is interpreted in terms of minimal knowledge, while A is interpreted
Table 1. Syntax and semantics of eALCOV
Name Syntax Semantics
concept name A AI ⊆ ∆
role name V VI ⊆∆×∆
individual name a aI ∈ ∆
variable x Z(x) ∈ ∆
top > ∆
bottom ⊥ ∅
nominal (schema) {t} {a | [a]≈ ≈ t(I,M,N ),Z }
concept complement ¬C ∆ \ C (I,M,N ),Z
concept conjunction C u D C (I,M,N ),Z ∩ D(I,M,N ),Z
concept disjunction C t D C (I,M,N ),Z ∪ D(I,M,N ),Z
existential restriction ∃R.C {δ ∈ ∆ | ∃ with (δ, ) ∈ R(I,M,N ),Z and ∈ C (I,M,N ),Z }
universal restriction ∀R.C {δ ∈ ∆ | (δ, ) ∈ R(I,M,N ),Z implies ∈ C (I,M,N ),Z }
C (J ,M,N ),Z
T
knowledge concept KC
TJ ∈M (J ,M,N ),Z
assumption concept AC J ∈N C
universal role U ∆×∆
V (J ,M,N ),Z
T
knowledge role KV
TJ ∈M (J ,M,N ),Z
assumption role AV J ∈N V
concept assertion C(a) aI ∈ C (I,M,N ),Z
role assertion V (a, b) (aI , bI ) ∈ V (I,M,N ),Z
TBox axiom C v D C (I,M,N ),Z ⊆ D(I,M,N ),Z
Interpretation I; MKNF structure (I, M, N ); variable assignment Z; A ∈ NC ; C, D ∈ C;
V ∈ NR ; R ∈ R; a, b ∈ NI ; x ∈ NV , and t ∈ NV ∪ NI .
as autoepistemic assumption and corresponds to ¬not, i.e., the classical negation of the
negation as failure operator not used in [27] instead of A.
We consider a signature Σ = hNI , NC , NR , NV i where NI , NC , NR , and NV are
pairwise disjoint and finite sets of individual names, concept names, role names, and
variables. In the following, we assume that Σ has been fixed. We define concepts and
roles in eALCOV by the following grammar.
R ::=V | U | KV | AV
C ::=> | ⊥ | A | {i} | {x} | ¬C | C u C | C t C | ∃R.C | ∀R.C | KC | AC
where V ∈ NR , A ∈ NC , i ∈ NI , and x ∈ NV . The names of the individual concepts
and roles can be found in Table 1. Epistemic concepts are knowledge and assumption
concepts, while epistemic roles are knowledge and assumption roles.
As usual, a TBox axiom (or general concept inclusion (GCI)) is an expression C v
D where C, D ∈ C. An ABox axiom is of the form C(a) or V (a, b) where C ∈ C,
V ∈ NR , and a, b ∈ NI . An eALCOV axiom is any ABox or TBox axiom, and an
eALCOV knowledge base (KB) is a finite set of eALCOV axioms.
The semantics of eALCOV as recalled from [20] is an adaptation from [24] and
[8]. As common, an interpretation I = (∆I , ·I ) consists of a domain ∆I 6= ∅ and a
function ·I that maps elements in NI , NC , and NR to elements, sets, and relations of
∆I respectively. Additionally, nominal schemas require a variable assignment Z for
an interpretation I, which is a function Z : NV → ∆I such that, for each v ∈ NV ,
Z(v) = aI for some a ∈ NI .
As common in MKNF-related semantics used to combine DLs with non-monotonic
reasoning (see [8,17,19,30]), specific restrictions on interpretations are introduced to
ensure that certain unintended logical consequences can be avoided (see, e.g., [30]).
Here, we adopt the standard name assumption from [20]. An interpretation I (over Σ
to which ≈ is added) employs the standard name assumption if
(1) NI∗ extends NI with a countably infinite set of individuals that cannot be used in
variable assignments, and ∆I = NI∗ ;
(2) for each i in NI∗ , iI = i; and
(3) equality ≈ is interpreted in I as a congruence relation – that is, ≈ is reflexive,
symmetric, transitive, and allows for the replacement of equals by equals [10].
The first condition fixes the (infinite) universe, but limits the application of variable
assignments to a finite subset, the second condition defines I as a bijective function,
while the third ensures that we still can identify elements of the domain. As an immedi-
ate side-effect, the variable assignment is no longer tied to a specific interpretation and
we can simplify notation by using ∆ without reference to a concrete interpretation.
Now, the first-order semantics is lifted to satisfaction in MKNF structures that
treat the modal operators w.r.t. sets of interpretations. An MKNF structure is a triple
(I, M, N ) where I is an interpretation, M and N are sets of interpretations, and
I and all interpretations in M and N are defined over ∆. For any such (I, M, N )
and assignment Z, the function ·(I,M,N ),Z is defined for arbitrary eALCOV expres-
sions as shown in Table 1. (I, M, N ) and Z satisfy an eALCOV axiom α, written
(I, M, N ), Z |= α, if the corresponding condition in Table 1 holds. (I, M, N ) satis-
fies α, written (I, M, N ) |= α, if (I, M, N ), Z |= α for all variable assignments Z. A
(non-empty) set of interpretations M satisfies α, written M |= α, if (I, M, M) |= α
holds for all I ∈ M, and M satisfies an eALCOV knowledge base KB, written
M |= KB, if M |= α for all axioms α ∈ KB. Note the small deviation of the se-
mantics of {t} in Table 1 compared to that in [24], which is necessary to ensure that the
semantics works as intended under standard name assumption.
It can be verified that the two sets of interpretations are each used to interpret
one of the modal operators, but in the monotonic semantics above, they simply coin-
cide. This changes with the non-monotonic MKNF model defined in the usual fashion
[8,17,19,30]: M is fixed to interpret A, and supersets M0 of M are used to test whether
the knowledge derived from M (via K) is indeed minimal.
Definition 1. Given an eALCOV knowledge base KB, a (non-empty) set of interpre-
tations M is an MKNF model of KB if (1) M |= KB, and (2) for each M0 with
M ⊂ M0 , (I 0 , M0 , M) 6|= KB for some I 0 ∈ M0 . KB is MKNF-satisfiable if an
MKNF model of KB exists. An axiom α is MKNF-entailed by KB, written KB |=K α,
if all MKNF models M of KB satisfy α.
As noted in [8], since M |= KB is defined w.r.t. (I, M, M), the operators K and
A are interpreted in the same way, and so we can restrict instance checking KB |=K
C(a) and subsumption KB |=K C v D to C and D without occurrences of the
operator A. Also, in absence of modal operators in the eALCOV KB, there is a unique
MKNF model which simply contains all standard (first-order) models of KB as usual.
3 Reasoning in eALCOV
In [20], reasoning in eSROIQ2 is discussed following [8] for reasoning in ALCKN F .
The problem with this approach is that it is undecidable in general, so, as in [8], restric-
tions are applied in [20] to regain decidability, which in certain cases prevent coverage
of the formalisms encompassed by the unrestricted language. To circumvent this, we
still rely on the same idea in principle, but we revise the applied restrictions to achieve
decidability making use of the gained expressiveness in eALCOV. In the following,
we spell out the restrictions with some motivation right away, before we show that this
indeed yields a decidable procedure for checking MKNF-satisfiability.
3.1 Safe eALCOV KBs
Following [8], the overall idea is to reduce reasoning in eALCOV to a number of rea-
soning tasks in non-modal ALCOV (again including U ), for which each model of an
eALCOV KB is represented by means of an ALCOV KB. Formally, a set of interpre-
tations M is ALCOV representable if there exists an ALCOV KB KBM such that
M = {I | I satisfies KBM }. Then, undecidability can be caused by three sources.
First, certain partially quantified expressions are not ALCOV representable (Theorem
4.1 in [8]), which is why we recall the notion of subjectively quantified KBs. For that
purpose, we define that an ALCOV expression S is subjective if each ALCOV subex-
pression in S lies in the scope of at least one modal operator.
Definition 2. An eALCOV KB KB is subjectively quantified if each expression of the
form ∃R.C, ∀R.C occurring in KB satisfies one of the conditions: (1) R is an ALCOV
role and C is an ALCOV concept, or (2) R and C are both subjective and C is of the
form KD, ¬KD, AD or ¬AD.
There exists a slightly relaxed condition on subjectively quantified KBs [17], but for
our purposes the original one suffices.
Second, even if subjectively quantified, certain nested expressions can be problem-
atic, so we introduce (modally) flat concepts, that can be seen as a further restriction of
simple concepts in [8], which prohibit such nesting altogether. Formally, an eALCOV
concept is flat if it does not contain any modal operator in scope of another, and an
2
In [20], the term SROIQV(Bs , ×)KN F is used, but, for the sake of readability and with a
slight abuse of notation, we follow our introduced naming scheme here.
eALCOV KB KB is flat if each concept in it is flat. Thus, quantifier expressions of the
form (2) in Def. 2 are flat as long as D does not contain further modal operators.
Third, intuitively, we have to make sure that GCIs involving modal operators cannot
be used to derive an infinite number of true assertions (see also Theorem 4.10 in [8]).
Rather than introducing simple KBs as in [8,20], we build on nominals and nominal
schemas to introduce safe concepts.
Definition 3. Given a subjectively quantified, flat eALCOV KB KB, an eALCOV
concept C in KB is called safe if C is of the form D u{t} for some guard t ∈ NI ∪NV .
The idea is to use the nominal (schema) as a guard that restricts “applicability” of con-
cepts involving modal operators to individuals occurring in KB. This all combines in
the definition of safe eALCOV KBs, for which we from now on consider two disjoint
subsets of the eALCOV TBox T of KB: T 0 , the set of all axioms that contain no modal
operators, and Γ , the set of all axioms that contain at least one modal operator.
Definition 4. Let KB be an eALCOV KB that is subjectively quantified and flat. Then,
KB is safe if the following conditions are satisfied:
1. For each C v D ∈ Γ , C is subjective and safe, D is safe for the same guard as C,
and no operator K occurs in ∃ and ∀ restrictions in D;
2. There is no concept assertion in KB containing a subconcept of the form ∃KR.KC.
Notably, due to KB also being subjectively quantified and flat, any C v D ∈ Γ in a
safe KB can be rewritten into one such that all subjective subconcepts in it are safe.
For example, the safe KB containing just the axiom
((K(C t ∃R.D) u ∃KR.KG) t ¬AE) u {x} v ∀AS.AF u {x}
can be straightforwardly rewritten into
((K(C t ∃R.D) u {x}) u (∃KR.KG u {x})) t (¬AE u {x}) v ∀AS.AF u {x}.
In the following, we assume that any C v D ∈ Γ in a safe eALCOV KB is already
rewritten this way, i.e., all subjective subconcepts in Γ are assumed safe.
Comparing to simple KBs (Def. 8 in [20]), intuitively, KB being flat covers condi-
tion 3. while 1. of Def. 4 covers to 1. and 2. there. Condition 2. in Def. 4 is not strictly
required for decidability (as the case can be handled by finitely many models up to re-
naming of individuals [8]), but it will simplify the subsequent material without affecting
coverage of related formalisms. These new conditions for safe KBs certainly have quite
a different flavor compared to simple KBs in [8,20], but we believe that they are over-
all simpler and more easy to grasp, and at the same time not jeopardizing coverage of
related formalisms. Of course, we still need to show that there is a decidable procedure
for reasoning with safe eALCOV KBs.
3.2 Determining MKNF Models
We start by grounding a given safe eALCOV KB, i.e., we replace all occurring nominal
schemas with nominals in all possible ways in the usual manner. This yields an eALCO
KB (again including U ), which is trivially safe and obtained in finite time, though, in
general, of exponential size in terms of the input KB.
From now on, we follow the principal argument from [8] as used in [20], but with
some variations and simplifications due to our different restrictions and to some extent
inspired by the reasoning algorithms for the related Hybrid MKNF [30].
First, we will collect a set of modal atoms based on the occurrence of epistemic
concepts and roles in a given KB. In difference to [8], we only consider atoms over
individuals occurring in the given KB. In the following, we use M to denote either K
or A, and N to denote either M or ¬M, we assume Q ∈ {∃, ∀}, and we remind that
we consider that all subjective concepts in Γ are safe. Given a safe eALCO KB KB,
the set of modal atoms M A(KB) is defined inductively as follows:
(1) if MD u {a} for some a ∈ NI occurs in KB, then KD(a) ∈ M A(KB);
(2) if MD occurs (non-safe) in concept assertion C(a), then KD(a) ∈ M A(KB);
(3) if QMR.ND u {a} for some a ∈ NI occurs in KB, then KR(a, i), KD(i) ∈
M A(KB) for all i ∈ NI ;
(4) if QMR.ND occurs (non-safe) in concept assertion C(a), then KR(a, i), KD(i) ∈
M A(KB) for all i ∈ NI ;
(5) nothing else belongs to M A(KB).
A further difference to [8] is that we only collect modal atoms under K. This is justified
by the fact that for ensuring condition (1) of Def. 1, the same set of interpretations M
is considered for evaluating formulas under K and A. As an immediate benefit, when
introducing partitions of these modal atoms next and guessing model candidates, we do
not have to verify whether modal atoms under K and A are aligned.
We now introduce a partition of M A(KB), which is a pair (P, N ) of positive modal
atoms P and negative modal atoms N such that P ∩ N = ∅ and P ∪ N = M A(KB).
As already mentioned, such partition can be understood as a guess about which modal
atoms are supposed to be true (P ) and false (N ), and we can use it to simplify an
eALCO KB as follows. Given a safe eALCO KB KB and a partition (P, N ) of
M A(KB), KB[P ] denotes the eALCO KB obtained from KB and (P, N ) by:
1. replacing each occurrence of the form MD u {a} in KB and each (non-safe)
occurrence of the form MD in a concept assertion C(a) ∈ KB with > if KD(a) ∈
P and with ⊥ otherwise;
2. replacing each occurrence of ∃MR.M1 D u {a} (∃MR.¬M1 D u {a}) in KB
and each (non-safe) occurrence of the form ∃MR.M1 D (∃MR.¬M1 D) in a con-
cept assertion C(a) ∈ KB with > if there exists y such that KR(a, y) ∈ P and
KD(y) ∈ P (KD(y) 6∈ P ) and with ⊥ otherwise;
3. replacing each occurrence of ∀MR.M1 D u {a} (∀MR.¬M1 D u {a}) in KB and
each (non-safe) occurrence of the form ∀MR.M1 D (∀MR.¬M1 D) in a concept
assertion C(a) ∈ KB with > if for each y such that KR(a, y) ∈ P , KD(y) ∈ P
(KD(y) 6∈ P ) and with ⊥ otherwise.
Note that we leave N implicit here, as it is completely specified by P and the definition
of a partition of M A(KB). We generalize the notion of KB[P ], based on two partitions
(P, N ), (P 0 , N 0 ) of M A(KB), to KB[P 0 ][P ] which is obtained from KB in exactly
the same way, only that if M or M1 is K, then P 0 is used in the evaluation of the
conditions, while for M or M1 being A, P is used. In either case, it can readily be
verified that the resulting KB does not contain any modal operators, hence is an ALCO
KB (admitting U ) for which satisfiability can be checked using standard DL reasoners.
With this in place, we can define an ALCO KB which takes the modal atoms
guessed to be true into account, and use the resulting KB to check whether a guess
is consistent with the original eALCO KB. Let KB be a safe eALCO KB and (P, N ),
(P 0 , N 0 ) partitions of M A(KB). Then, ObKB,P 0 ,P denotes the following ALCO KB:
ObKB,P 0 ,P = KB[P 0 ][P ] ∪ {C(x) | KC(x) ∈ P 0 } ∪ {R(x, y) | KR(x, y) ∈ P 0 }
Then, partition (P, N ) of M A(KB) is consistent with the (safe) eALCO KB if the
following conditions hold:
(1) the ALCO KB ObKB,P,P is satisfiable;
(2) ObKB,P,P 6|= C(x) for each KC(x) ∈ N ;
(3) ObKB,P,P 6|= R(x, y) for each KR(x, y) ∈ N .
Basically, item (1) checks whether the guessed P does not yield contradictions w.r.t.
KB, while (2) and (3) verify that no modal atom occurs wrongfully in N .
A link between a set of interpretations and partitions is established next. Let M be
a set of interpretations over ∆. Then, M induces the partition (P, N ) of M A(KB):
P = {KC(x) | KC(x) ∈ M A(KB) and M |= KC(x)}
∪ {KR(x, y) | KR(x, y) ∈ M A(KB) and M |= KR(x, y)}
N = {KC(x) | KC(x) ∈ M A(KB) and M 6|= KC(x)}
∪ {KR(x, y) | KR(x, y) ∈ M A(KB) and M 6|= KR(x, y)}
We can show that the intended correspondence indeed holds.
Lemma 1. Let KB be a safe eALCO KB, M a set of interpretations over ∆ that
satisfies KB such that M |= KR(i1 , i2 ) only if i1 ≈ a ∈ NI and i2 ≈ b ∈ NI , and
(P, N ) the partition of M A(KB) induced by M. Then (P, N ) is consistent with KB.
Note that here, the particular restriction on M is necessary, otherwise the property
would not hold. Take (∃AR.AC)(a). Then, M = {I | I |= R(a, i) ∧ C(i) for
some i ∈ ∆ and i 6≈ a} clearly satisfies the assertion, yet the induced partition with
P = ∅ is not consistent with KB (because of (1) and the fact that that KB[P ][P ]
only considers modal atoms in M A(KB)). The same restriction is no longer necessary
for MKNF models for which the following one-to-one correspondence between every
MKNF model M of KB and the partition induced by M can be shown.
Theorem 1. A set M of interpretations over ∆ is an MKNF model for a safe eALCO
KB KB iff the partition (P, N ) of M A(KB) induced by M satisfies the following:
(1) (P, N ) is consistent with KB;
(2) M = {I | I |= ObKB,P,P }; and
(3) for each partition (P 0 , N 0 ) of M A(KB) such that P 0 ⊂ P , at least one of the
following conditions does not hold:
(a) the ALCO KB ObKB,P 0 ,P is satisfiable;
(b) ObKB,P 0 ,P 6|= C(x) for each KC(x) ∈ N 0 ;
(c) ObKB,P 0 ,P 6|= R(x, y) for each KR(x, y) ∈ N 0 .
As an immediate consequence of this procedure, we can show that safe eALCOV
KBs are ALCOV representable.
Corollary 1. Let KB be a safe eALCOV KB, M an MKNF model of KB, and (P, N )
be the partition of M A∆ (KB) induced by M. Then M = {I | I |= ObKB,P,P }.
4 Coverage within the Decidable Fragment
The established result in the previous section is certainly interesting in its own right,
since, arguably, the imposed restrictions and the applied construction is considerably
less complicated in terms of notation than the one applied in [8,20]. Anyway, the main
outlined purpose of this revision is to ensure that the new decidable fragment encom-
passes all the formalisms for which coverage was shown in [20] only for the full lan-
guage. In this section, we revisit this material and discuss relevant changes.
4.1 Monotonic Approaches
Naturally, our decidable language fragment of safe eALCOV KBs covers ALCOV
(with and without U ) and all its sub-languages. This does not include SROIQ, i.e.,
OWL 2 DL and its tractable profiles, but a trivial adjustment following the ideas in [20]
where modal operators are limited to ALCOV concepts is easily conceivable.
Coverage of RIF-CORE [3], i.e., n-ary Datalog, interpreted as DL-safe Rules [31]
carries over from [20] or alternatively from [25]. In fact, the latter does not even require
the usage of the universal role U which is just fine if we only want to embed a Datalog
program. However, if we want to cover an embedding of n-ary Datalog interacting with
DLs, then the former is required: consider the Datalog rule C(a) → D(a) and a concept
assertion C(a). The rule can be translated to ∃atom.(C u {a}) v ∃atom.(D u {a})
(slightly adjusted from [25]), but there is I such that atomI = ∅, i.e., D(a) is no
longer derivable. Thus, based on the former Datalog embedding, coverage of DL-safe
SWRL [31], AL-log [7], and CARIN [26] carries over, i.e., without much surprise all
monotonic approaches as outlined in [20] are covered.
4.2 ALCKN F
In [8], it is shown how several non-monotonic reasoning features (defaults, integrity
constraints, and role and concept closure) can be modeled in the full language ALCKN F
and it is argued that the restriction to simple KBs applied to achieve decidability does
not impede coverage. The full eALCOV language obviously includes ALCKN F by
design, but since we have changed the restrictions to achieve decidability, these results
do not carry over automatically, so we briefly discuss coverage of these features for safe
eALCOV KBs (and refer the reader for the detailed discussion to [8]).
First, closed DL-defaults [2] of the form
α : β1 , . . . , β n
d=
γ
are covered in [8], where α, βi , and γ are DL concepts and n ≥ 0. Closed defaults
are limited in their applicability to individuals explicitly mentioned in the knowledge
base. This is achieved in [8] by using a new atomic concept I in each translation of
a default and adding the assertions I(a) for each a appearing in the knowledge base.
Conceptually, this matches the idea of nominal schemas, so the translation of closed
defaults can be presented as a safe eALCOV axiom
τDK (d) = Kα u ¬A¬β1 u · · · u ¬A¬βn u {x} v Kγ u {x}
without the need to introduce new concepts or adding additional assertions, and it is
easy to see that Theorem 3.1 from [8] can be adapted accordingly.
Theorem 2. Let hΣ, Di be an ALC KB with defaults, where Σ is an ALC KB and D is
a set of ALC-defaults. The eALCOV KB τ (Σ, D) is such that, for every ALC-concept
C and every individual a ∈ NI , it holds hΣ, Di |= C(a) iff τDK (Σ, D) |= C(a).
Secondly, integrity constraints (ICs) are considered, and it is argued that ICs com-
monly apply to individuals explicitly mentioned in the considered KB and impose re-
strictions without changing the content of the KB. This is in line with our restrictions
on safe eALCOV KBs and it can be verified that all examples discussed in [8] can be
made safe explicitly by introducing guards {x} as for defaults. Finally, similar observa-
tions hold for the considerations on role and concept closure, i.e., all modeling features
presented in [8] can indeed be adjusted to safe eALCOV KBs without much effort.
4.3 Hybrid MKNF
Hybrid MKNF as a combination of DLs with non-monotonic rules is based on MKNF
logics as well, but of different expressivity due to the different restrictions applied to
the full MKNF language in each of the two approaches [30]. In [20], an embedding of
hybrid MKNF into epistemic DLs is presented (we refer to that paper for the techni-
cal details). Though not the full language of hybrid MKNF is embedded, the presented
fragment suffices to cover Answer Set Programming [11], i.e., disjunctive Datalog with
classical negation and non-monotonic negation under the answer set semantics. Un-
fortunately, the presented embedding is in general not covered within the decidable
fragment in [20] as shown with the simple example > v ∃U.({a} u C) and KD(a) ←
KC(a) as the latter would be embedded as K(∃U.({a}uC) v K(∃U.({a}uC) which
is not simple [20]. This can be remedied with safe eALCOV KB by changing the trans-
lation of MKNF rules dl(KH1 ∨ KHl ← KA1 , . . . , KAn , notB1 , . . . , notBm ) in
[20] to
Kdl(A1 ) u . . . u Kdl(An ) u ¬Adl(B1 ) u . . . u ¬Adl(Bm ) u {i} v
Kdl(H1 ) t . . . t Kdl(Hl ) u {i}
where i is a fresh individual and dl the translation function on (possibly classically
negated) atoms defined in [20]. Essentially, in the original embedding, such translated
concepts in GCIs would due to the universal role either be interpreted as ∆ or ∅. Here,
we introduce a nominal as guard that acts as a surrogate for all elements in ∆, thus
reducing such interpretation to either i or ∅. An adaptation of the results in [20] (Lemma
3 and Theorem 4) are then straightforward.
Theorem 3. Let K = (O, P) be a hybrid MKNF KB. M is an MKNF model of K iff
M1 = {J | J ∈ f am(I) with I ∈ M} is a hybrid MKNF model of dl(K).
This ensures that safe eALCOV KBs in fact embed the restricted version hybrid MKNF
and therefore also ASP.
5 Conclusions
We have studied epistemic extensions of DLs focusing here on eALCOV, i.e., ALC
extended with nominals, nominals schemas, the universal role, and two epistemic op-
erators for modeling non-monotonic reasoning. We have shown that this language en-
compasses all non-monotonic modeling features and approaches discussed in [20], and
that an extension to a few missing monotonic languages (e.g., SROIQ) is easily con-
ceivable. We have introduced a set of restrictions on the general language which is
different from that in [20], and we have shown that, under these restrictions, reasoning,
i.e., checking MKNF-satisfiability becomes decidable, and, unlike in previous work,
the restricted language still covers all the discussed modeling features.
An immediate matter for follow-up work is the computational complexity when
reasoning with epistemic DLs, a question that has only received limited attention so
far (in [8] a triple exponential space upper bound for reasoning with simple KBs has
been pointed out, while no results are mentioned in [20]). It is clear that the complexity
results established for reasoning with nominal schemas (without epistemic operators)
[25] can serve as first necessary lower bounds, i.e., for eALCOV in particular a minimal
lower bound is established by the fact that reasoning in ALCOV is 2EXPTIME-complete.
This does neither account for the universal role nor the epistemic operators. Since ALC
with arbitrary Boolean role constructors is NEXPTIME-complete [28,36] (as the restric-
tion to safe Boolean role constructors in [36] does not suffice to cover U ), and the
decision procedure for MKNF-satisfiability requires nondeterministically guessing the
right partition, by combining the different sources of complexity we conjecture a lower
bound of at least N2EXPTIME.
Another interesting topic for future work is to establish coverage for further re-
lated formalisms, for example by extending the expressiveness of rules permitted in
the embedding of Hybrid MKNF, which then allows us to include already established
embedding results for, e.g., [9,32] in [30] or by considering among others work on cir-
cumscription in DLs [4,33]. Building on the existing relation between epistemic exten-
sions of DLs and Hybrid MKNF, we can also investigate the relation to parameterized
logic programs [12,13], or multi-context systems [5] using the established connection
between these and Hybrid MKNF [21]. Finally, an implementation may be considered
given a) the more simple decision procedure proposed here and b) the recent work on
implementing nominal schemas [22,37,6,34] and Hybrid MKNF [1,16]. In particular
the encouraging results for Konclude [34,35] seem to indicate that this may in fact be
achievable in a feasible manner.
Acknowledgments This work was partially supported by Fundação para a Ciência e
a Tecnologia under project “ERRO – Efficient Reasoning with Rules and Ontologies”
(PTDC/EIA-CCO/121823/2010) and strategic project PEst/UID/CEC/04516/2013, and
by FCT grant SFRH/BPD/86970/2012.
References
1. Alferes, J.J., Knorr, M., Swift, T.: Query-driven procedures for hybrid MKNF knowledge
bases. ACM Trans. Comput. Log. 14(2), 16 (2013)
2. Baader, F., Hollunder, B.: Embedding defaults into terminological representation systems.
Journal of Automated Reasoning 14, 149–180 (1995)
3. Boley, H., Hallmark, G., Kifer, M., Paschke, A., Polleres, A., Reynolds, D. (eds.):
RIF Core Dialect. W3C Recommendation 22 June 2010 (2010), available from
http://www.w3.org/TR/rif-core/
4. Bonatti, P.A., Lutz, C., Wolter, F.: The complexity of circumscription in dls. J. Artif. Intell.
Res. (JAIR) 35, 717–773 (2009)
5. Brewka, G., Eiter, T.: Equilibria in heterogeneous nonmonotonic multi-context systems. In:
Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence. pp. 385–
390. AAAI Press (2007)
6. Carral, D., Wang, C., Hitzler, P.: Towards an efficient algorithm to reason over description
logics extended with nominal schemas. In: Faber, W., Lembo, D. (eds.) Web Reasoning and
Rule Systems - 7th International Conference, RR 2013. Proceedings. LNCS, vol. 7994, pp.
65–79. Springer (2013)
7. Donini, F.M., Lenzerini, M., Nardi, D., Schaerf, A.: AL-log: Integrating datalog and descrip-
tion logics. Journal of Intelligent Information Systems 10(3), 227–252 (1998)
8. Donini, F.M., Nardi, D., Rosati, R.: Description logics of minimal knowledge and negation
as failure. ACM Transactions on Computational Logic 3(2), 177–225 (2002)
9. Eiter, T., Ianni, G., Lukasiewicz, T., Schindlauer, R., Tompits, H.: Combining answer set
programming with description logics for the Semantic Web. Artificial Intelligence 172(12–
13), 1495–1539 (2008)
10. Fitting, M.: First-order logic and automated theorem proving. Springer, 2nd edn. (1996)
11. Gelfond, M., Lifschitz, V.: Classical negation in logic programs and disjunctive databases.
New Generation Computing 9, 365–385 (1991)
12. Gonçalves, R., Alferes, J.J.: Parametrized logic programming. In: Janhunen, T., Niemelä, I.
(eds.) Logics in Artificial Intelligence - 12th European Conference, JELIA 2010. Proceed-
ings. LNCS, vol. 6341, pp. 182–194. Springer (2010)
13. Gonçalves, R., Alferes, J.J.: Decidability and implementation of parametrized logic pro-
grams. In: Cabalar, P., Son, T.C. (eds.) Logic Programming and Nonmonotonic Reasoning,
12th International Conference, LPNMR 2013. Proceedings. LNCS, vol. 8148, pp. 361–373.
Springer (2013)
14. Grimm, S., Hitzler, P.: Semantic Matchmaking of Web Resources with Local Closed-World
Reasoning. International Journal of Electronic Commerce 12(2), 89–126 (2008)
15. Hitzler, P., Krötzsch, M., Parsia, B., Patel-Schneider, P.F., Rudolph, S. (eds.): OWL 2 Web
Ontology Language: Primer. W3C Recommendation 27 October 2009 (2009), available from
http://www.w3.org/TR/owl2-primer/
16. Ivanov, V., Knorr, M., Leite, J.: A query tool for EL with non-monotonic rules. In: Alani, H.,
Kagal, L., Fokoue, A., Groth, P.T., Biemann, C., Parreira, J.X., Aroyo, L., Noy, N.F., Welty,
C., Janowicz, K. (eds.) The Semantic Web - ISWC 2013 - 12th International Semantic Web
Conference, Proceedings, Part I. LNCS, vol. 8218, pp. 216–231. Springer (2013)
17. Ke, P.: Nonmonotonic Reasoning with Description Logics. Ph.D. thesis, University of
Manchester (2011)
18. Kifer, M., Boley, H. (eds.): RIF Overview. W3C Working Group Note 22 June 2010 (2010),
available from http://www.w3.org/TR/rif-overview/
19. Knorr, M., Alferes, J.J., Hitzler, P.: Local closed world reasoning with description logics
under the well-founded semantics. Artificial Intelligence 175(9–10), 1528–1554 (2011)
20. Knorr, M., Hitzler, P., Maier, F.: Reconciling OWL and non-monotonic rules for the semantic
web. In: Raedt, L.D., Bessière, C., Dubois, D., Doherty, P., Frasconi, P., Heintz, F., Lucas,
P.J.F. (eds.) ECAI 2012 - 20th European Conference on Artificial Intelligence. Proceedings.
Frontiers in Artificial Intelligence and Applications, vol. 242, pp. 474–479. IOS Press (2012)
21. Knorr, M., Slota, M., Leite, J., Homola, M.: What if no hybrid reasoner is available? hybrid
MKNF in multi-context systems. J. Log. Comput. 24(6), 1279–1311 (2014)
22. Krisnadhi, A., Hitzler, P.: A tableau algorithm for description logics with nominal schema.
In: Web Reasoning and Rule Systems - 6th International Conference, RR 2012. Proceedings.
LNCS, vol. 7497, pp. 234–237. Springer (2012)
23. Krötzsch, M.: Description Logic Rules, Studies on the Semantic Web, vol. 008. IOS
Press/AKA (2010)
24. Krötzsch, M., Maier, F., Krisnadhi, A.A., Hitzler, P.: A better uncle for OWL: Nominal
schemas for integrating rules and ontologies. In: Srinivasan, S., Ramamritham, K., Kumar,
A., Ravindra, M.P., Bertino, E., Kumar, R. (eds.) Proceedings of the 20th International World
Wide Web Conference, WWW2011. pp. 645–654. ACM (2011)
25. Krötzsch, M., Rudolph, S.: Nominal schemas in description logics: Complexities clarified.
In: Baral, C., Giacomo, G.D., Eiter, T. (eds.) Principles of Knowledge Representation and
Reasoning: Proceedings of the Fourteenth International Conference, KR 2014. AAAI Press
(2014)
26. Levy, A.Y., Rousset, M.C.: Combining Horn rules and description logics in CARIN. Artifi-
cial Intelligence 104, 165–209 (1998)
27. Lifschitz, V.: Nonmonotonic databases and epistemic queries. In: Mylopoulos, J., Reiter,
R. (eds.) Proceedings of the 12th International Joint Conferences on Artifical Intelligence,
IJCAI’91. pp. 381–386. Morgan Kaufmann (1991)
28. Lutz, C., Sattler, U.: The complexity of reasoning with Boolean modal logics. In: Wolter, F.,
Wansing, H., de Rijke, M., Zakharyaschev, M. (eds.) Proc. of the 3rd Int. Conf. on Advances
in Modal Logic (AiML 2000). pp. 329–348. World Scientific (2002)
29. Mehdi, A., Rudolph, S.: Revisiting semantics for epistemic extensions of description log-
ics. In: Burgard, W., Roth, D. (eds.) Proceedings of the Twenty-Fifth AAAI Conference on
Artificial Intelligence, AAAI 2011. AAAI Press (2011)
30. Motik, B., Rosati, R.: Reconciling Description Logics and Rules. Journal of the ACM 57(5),
93–154 (2010)
31. Motik, B., Sattler, U., Studer, R.: Query answering for OWL-DL with rules. Journal of Web
Semantics 3(1), 41–60 (2005)
32. Rosati, R.: DL+Log: A tight integration of description logics and disjunctive datalog. In:
Doherty, P., Mylopoulos, J., Welty, C.A. (eds.) 10th International Conference on the Princi-
ples of Knowledge Representation and Reasoning, (KR’06), Proceedings. pp. 68–78. AAAI
Press (2006)
33. Sengupta, K., Krisnadhi, A.A., Hitzler, P.: Local closed world semantics: Grounded circum-
scription for OWL. In: Aroyo, L., Welty, C., Alani, H., Taylor, J., Bernstein, A., Kagal, L.,
Noy, N.F., Blomqvist, E. (eds.) The Semantic Web - ISWC 2011 - 10th International Seman-
tic Web Conference, Proceedings. LNCS, vol. 7031, pp. 617–632. Springer (2011)
34. Steigmiller, A., Glimm, B., Liebig, T.: Reasoning with nominal schemas through absorption.
J. Autom. Reasoning 53(4), 351–405 (2014)
35. Steigmiller, A., Liebig, T., Glimm, B.: Konclude: System description. J. Web Sem. 27, 78–85
(2014)
36. Tobies, S.: Complexity results and practical algorithms for logics in knowledge representa-
tion. Ph.D. thesis, LuFG Theoretical Computer Science, RWTH-Aachen, Germany (2001)
37. Wang, C., Hitzler, P.: A resolution procedure for description logics with nominal schemas.
In: Takeda, H., Qu, Y., Mizoguchi, R., Kitamura, Y. (eds.) Second Joint International Con-
ference, JIST 2012. Proceedings. LNCS, vol. 7774, pp. 1–16. Springer (2012)