1 Introduction

Representing and reasoning with contexts has recently gained increasing interest in the Semantic Web area, due to the need for interpreting knowledge resources with respect to contextual information given in their metadata. This led to a number of (description) logic based approaches e.g. [13, 14, 17, 18]. In this line of works, we consider the recent proposal of the Contextualized Knowledge Repository (CKR) framework [6, 17], with its latest formulation in [4].

A CKR knowledge base is a two-layer structure where the higher level consists of a global context and the lower level consists of a set of local contexts. The global context contains context-independent knowledge about the domain of discourse (global object knowledge) and the structure and properties of the local contexts (meta-knowledge). Local contexts contain knowledge that holds under specific situations (e.g. during a certain period of time, region in space). The global object knowledge is propagated to the local contexts and it is used to constrain local knowledge in different contexts. In [4] an extension to CKR was proposed by introducing a notion of justifiable exceptions. Axioms in the global context may be specified as defeasible, meaning that in general they are “inherited” in local instances, but these can be “overridden” on some exceptional instance if they would cause a local contradiction. A limitation of the proposal in [4] is that inheritance of defeasible axioms is restricted to the direction from the global to the local contexts: in general, one may want to specify more complex structures of contexts and control the knowledge propagation across such structures e.g. in the case of hierarchies of contexts specified by a context coverage relation [17].

Thus, in [7] we generalize this approach by allowing for local defeasible axioms in coverage contextual hierarchies. For the interpretation of overridings, we prefer models that prioritize the validity of defeasible axioms at the most specific contexts. In [7] we concentrate on ranked contextual hierarchies, namely hierarchies that can be divided in a linear order of levels: this restriction allows us to define a simple “global” preference on models based on the level of the overridden defeasible axioms. This also permits to easily adapt the translation to ASP programs from [4] by computing preference across answer sets by means of weak constraints [16] on the level of overridings.

In this paper, we continue the work in [7] by considering the case of CKRs with general contextual coverage structures. In order to cope with the interpretation of overriding in generic hierarchies, we need to adopt a “local” preference on models. Intuitively, a (non-strict) preference on local defeasible axioms is derived from their position in the coverage hierarchy: we prefer models which override the axioms in the higher contexts in the hierarchy, in order to prefer the most specific axioms in the lower contexts. However, while in [7] preference was mapped on the linear approximation provided by levels, with general hierarchies such preference has to be defined by considering the local coverage relations of the contexts of the overridden axioms. This provides a more accurate definition of the preference, but the comparison on the models is more complex. This aspect reflects on the reasoning method we provide for instance checking: we provide an algorithm, based on the preference semantic definition, that is able to derive the “preferred” answer sets which encode the expected interpretation of inheritance.

The contributions of this paper can be summarized as follows:

  • We describe the extension of the CKR semantics with defeasible axioms in local contexts, as provided in [7]. Inheritance and overriding of defeasible axioms is defined over a hierarchical coverage relation across local contexts: in order to concentrate on the contextual structure, we work on a restriction of CKR that we call simple CKR (sCKR). In this paper we consider general contextual hierarchies: in the definition of the semantics, we refine the definition of model preference to consider the “local” ordering of overridings in the contextual hierarchy.

  • We summarize the computational complexity of major reasoning tasks, in particular axiom entailment and conjunctive query (CQ) answering in the case of reasoning on general hierarchies. Under the new definition of model preference, we can show that axiom entailment is \(\varPi ^p_2\)-complete and CQ-answering is \(\varPi ^p_2\)-complete: as in the case of level-based preference, reasoning with preference increases the complexity of entailment, but it does not for CQ answering.

  • We extend to general hierarchies the reasoning method by a translation to datalog (with negation under answer set semantics) for simple CKRs in \(\mathcal {SROIQ}\text {-RL}\) proposed in [7]. In order to restrict reasoning on preferred models, we provide an algorithm for comparing answer sets based on the semantic definition of the local preference of overridings. The resulting reasoning procedure provides a sound and complete method for instance checking and conjunctive query answering on sCKR.

For space limitations, we refer the reader to [4, 7] for preliminaries on the definitions of \(\mathcal {SROIQ}\text {-RL}\) language and datalog programs under answer set semantics that we assume in the following sections.

2 Simple CKR with Justifiable Exceptions

We provide in this section the definition of simple CKR (sCKR) introduced in [7] adapted to the case of general hierarchies. With respect to the original formulation of CKR presented in [3, 4, 6], a simple CKR is still a two layered structure: however, in order to emphasize the role of the coverage relation, we simplify the upper layer to be a poset based on such relation.

Syntax. Consider a non empty-set of context names \(\varvec{\mathsf {N}}\subseteq \mathrm {NI}\). We define a coverage relation \(\prec \subseteq \varvec{\mathsf {N}}\times \varvec{\mathsf {N}}\). Given context names \(\mathsf {c}_1, \mathsf {c}_2 \in \varvec{\mathsf {N}}\), we say that \(\mathsf {c}_2\) covers \(\mathsf {c}_1\) if \(\mathsf {c}_1 \prec \mathsf {c}_2\). The coverage relation \(\prec \) is a strict partial order relation on \(\varvec{\mathsf {N}}\), i.e. it is irreflexive and transitive. Intuitively, \(\mathsf {c}_1\prec \mathsf {c}_2\) means that \(\mathsf {c}_2\) is more general than \(\mathsf {c}_1\), in the sense that \(\mathsf {c}_2\) refers to a portion of the world that covers the one described by \(\mathsf {c}_1\) [17]. We may use the non-strict relation \(\mathsf {c}_1\preceq \mathsf {c}_2\) to indicate that \(\mathsf {c}_1\) can be covered by \(\mathsf {c}_2\) or is the same context.

We can now define the language used in the local contexts to express their knowledge.

Definition 1 (contextual language)

Given a set of context names \(\varvec{\mathsf {N}}\), for every description language \(\mathcal{L}_{\varSigma }\) we define \(\mathcal{L}_{\varSigma ,\varvec{\mathsf {N}}}\) as the description language \(\mathcal{L}\) with the following additional rule for concept and role formation: \(\textit{eval}(X,\mathsf {c})\) is a concept (resp. role) of \(\mathcal{L}_{\varSigma ,\varvec{\mathsf {N}}}\) if X is a concept (resp. role) of \(\mathcal{L}_{\varSigma }\) and \(\mathsf {c}\in \varvec{\mathsf {N}}\).

Definition 2 (defeasible axiom)

A defeasible axiom is any expression of the form \({\mathrm D}(\alpha )\), where \(\alpha \) is an axiom of \(\mathcal{L}_{\varSigma }\). The DL language \(\mathcal{L}_{\varSigma ,\varvec{\mathsf {N}}}^{{\mathrm D}}\) extends \(\mathcal{L}_{\varSigma ,\varvec{\mathsf {N}}}\) with the set of defeasible axioms in \(\mathcal{L}_{\varSigma }\).

Using these definitions, simple CKRs are defined as follows:

Definition 3 (simple Contextualized Knowledge Repository, sCKR)

A Simple Contextualized Knowledge Repository (sCKR) over \(\varSigma \) and \(\varvec{\mathsf {N}}\) is a structure \(\mathfrak {K}= \langle \mathfrak {C}, \mathrm {K}_{\varvec{\mathsf {N}}} \rangle \) where:

  • \(\mathfrak {C}\) is a poset \((\varvec{\mathsf {N}}, \prec )\) and

  • \(\mathrm {K}_{\varvec{\mathsf {N}}} = \{\mathrm {K}_\mathsf {c}\}_{\mathsf {c}\in \varvec{\mathsf {N}}}\) for each context name , \(\mathrm {K}_\mathsf {c}\) is a DL knowledge base over \(\mathcal{L}_{\varSigma ,\varvec{\mathsf {N}}}^{{\mathrm D}}\).

Example 1

We adapt the corporation example from [7] to the case of a simple non-ranked hierarchy. Let us consider a sCKR \(\mathfrak {K}_{org} = \langle \mathfrak {C}, \mathrm {K}_{\varvec{\mathsf {N}}} \rangle \) describing the organization of a corporation. The corporation wants to define different policies with respect to its local branches. The hierarchy of contexts \(\mathfrak {C}\), representing the corporation organization, is shown in Fig. 1.

Fig. 1.
figure 1

Context hierarchy of example sCKR.

The company can enforce policies depending on the branch and its influence on the local sites. The corporation is active in the fields of Musical instruments (\( M \)), Electronics (\( E \)) and Robotics (\( R \)). A supervisor (\( S \)) can be assigned to manage only one of these fields. By putting defeasible axioms in the correct contexts in \(\mathrm {K}_{\varvec{\mathsf {N}}}\), we can assign local supervisors to their field:

In \(\mathsf {c}_ world \) we say that supervisors are assigned to Electronics, while in the sub-context for \(\mathsf {c}_ branch2 \) we contradict this by assigning all local supervisors to the Robotics area and in \(\mathsf {c}_ branch1 \) we further specialize this by assigning supervisors to the Musical instruments area. In the contexts for local sites we have information about the instances (here we consider only \(\mathsf {c}_ local1 \) for simplicity). Note that different assignments of areas for i are possible by instantiating the defeasible axioms: intuitively, we want to prefer the interpretations that override the higher defeasible axioms in \(\mathsf {c}_ world \) and \(\mathsf {c}_ branch2 \)\(\Diamond \)

sCKRs restrict the original CKR definition in [3, 4, 6] in order to concentrate on aspects of defeasibility across contexts. Any sCKR can be easily translated in a CKR (by suitably adapting the interpretation of coverage context relation like in the following definition of semantics). Differently from [7], we do not restrict the form of the poset \(\mathfrak {C}\). Thus, the definition of preference across different models can not be based on syntactic properties of the hierarchy: it will be defined over a local ordering on elements of the semantics (clashing assumptions).

Semantics. An interpretation for a sCKR is a set containing an interpretation for each local context.

Definition 4 (sCKR interpretation)

An interpretation for \(\mathcal{L}_{\varSigma ,\varvec{\mathsf {N}}}\) is a family \(\mathfrak {I}= \{\mathcal {I}(\mathsf {c})\}_{\mathsf {c}\in \varvec{\mathsf {N}}}\) of \(\mathcal{L}_{\varSigma }\) interpretations, such that \(\varDelta ^{\mathcal {I}(\mathsf {c})}\,{=}\, \varDelta ^{\mathcal {I}(\mathsf {c}')}\) and \(a^{\mathcal {I}(\mathsf {c})} \,{=}\, a^{\mathcal {I}(\mathsf {c}')}\), for every \(a \,{\in }\, \mathrm {NI}_\varSigma \) and \(\mathsf {c},\mathsf {c}' \,{\in }\, \varvec{\mathsf {N}}\).

The interpretation of concepts and role expressions in \(\mathcal{L}_{\varSigma ,\varvec{\mathsf {N}}}\) is obtained by extending the standard interpretation to \(\textit{eval}\) expressions: for every \(\mathsf {c}\in \varvec{\mathsf {N}}\), \(\textit{eval}(X,\mathsf {c}')^{\mathcal {I}(\mathsf {c})} = X^{\mathcal {I}(\mathsf {c}')}\). We consider the notion of axiom instantiation and clashing assumption as defined in [4].

Definition 5 (axiom instantiation)

Given an axiom \(\alpha \in \mathcal{L}_\varSigma \) with FO-translation \(\forall \mathbf {x}.\phi _\alpha (\mathbf {x})\), the instantiation of \(\alpha \) with a tuple \({\mathbf {e}}\) of individuals in \(\mathrm {NI}\), written \(\alpha ({\mathbf {e}})\), is the specialization of \(\alpha \) to \({\mathbf {e}}\), i.e., \(\phi _\alpha ({\mathbf {e}})\), depending on the type of \(\alpha \).

Definition 6 (clashing assumptions and sets)

A clashing assumption for a context \(\mathsf {c}\) is a pair \(\langle \alpha , {\mathbf {e}} \rangle \) such that \(\alpha ({\mathbf {e}})\) is an axiom instantiation of \(\alpha \), and \({\mathrm D}(\alpha ) \in \mathrm {K}_{\mathsf {c}'}\) is a defeasible axiom of some . A clashing set for \(\langle \alpha ,{\mathbf {e}} \rangle \) is a satisfiable set S of ABox assertions such that \(S \cup \{\alpha ({\mathbf {e}})\}\) is unsatisfiable.

A clashing assumption \(\langle \alpha , {\mathbf {e}} \rangle \) represents that \(\alpha ({\mathbf {e}})\) is not (DL-)satisfiable, and a clashing set S provides an assertional “justification” for the assumption of local overriding of \(\alpha \) on \({\mathbf {e}}\). We extend our interpretations to account for such notions.

Definition 7 (CAS-interpretation)

A CAS-interpretation is a pair \(\mathfrak {I}_{ CAS }=\langle \mathfrak {I},\chi \rangle \) where \(\mathfrak {I}\) is an interpretation and \(\chi \) maps every \(\mathsf {c}\in \varvec{\mathsf {N}}\) to a set \(\chi (\mathsf {c})\) of clashing assumptions for context \(\mathsf {c}\).

Definition 8 (CAS-model)

Given a sCKR \(\mathfrak {K}\), a CAS-interpretation \(\mathfrak {I}_{ CAS }= \langle \mathfrak {I}, \chi \rangle \) is a CAS-model for \(\mathfrak {K}\) (denoted \(\mathfrak {I}_{ CAS } \models \mathfrak {K}\)), if the following holds:

  1. (i)

    for every \(\alpha \in \mathrm {K}_\mathsf {c}\) (strict axiom), and \(\mathsf {c}'\preceq \mathsf {c}\), \(\mathcal {I}(\mathsf {c}')\models \alpha \);

  2. (ii)

    for every \({\mathrm D}(\alpha ) \in \mathrm {K}_\mathsf {c}\), \(\mathcal {I}(\mathsf {c})\models \alpha \);

  3. (iii)

    for every \({\mathrm D}(\alpha ) \in \mathrm {K}_\mathsf {c}\) and \(\mathsf {c}'\prec \mathsf {c}\), if \(\mathbf {d} \notin \{ {\mathbf {e}}\mid \langle \alpha ,{\mathbf {e}} \rangle \in \chi (\mathsf {c}')\}\), then \(\mathcal {I}(\mathsf {c}') \models \phi _\alpha (\mathbf {d})\).

In order to generalize the model preference to general hierarchies, in this paper we consider a local preference on clashing assumption sets (cf. discussion in [7]). The preference is defined directly along the coverage relation:

\(\chi _1(\mathsf {c}) > \chi _2(\mathsf {c})\), if for every \(\eta = \langle \alpha _1,{\mathbf {e}} \rangle \in \chi _1(\mathsf {c}) \setminus \chi _2(\mathsf {c})\) with \({\mathrm D}(\alpha _1)\) at a context , there exists an \(\eta ' = \langle \alpha _2,{\mathbf {f}} \rangle \in \chi _2(\mathsf {c}) \setminus \chi _1(\mathsf {c})\) with \({\mathrm D}(\alpha _2)\) at context such that .

This definition reflects the intuition that if we make in \(\chi _1(\mathsf {c})\) an exception at \(\mathsf {c}_1\), then a “more costly” exception should be made at a context \(\mathsf {c}_2\) below \(\mathsf {c}_1\) by \(\chi _2(\mathsf {c})\) that is not made by \(\chi _1(\mathsf {c})\).

Two DL interpretations \(\mathcal {I}_1\) and \(\mathcal {I}_2\) are \(\mathrm {NI}\)-congruent, if \(c^{\mathcal {I}_1} = c^{\mathcal {I}_2}\) holds for every \(c\in \mathrm {NI}\). This naturally extends to a (CAS) interpretation \(\mathfrak {I}_{ CAS } = \langle \mathfrak {I}, \chi \rangle \) by considering all context interpretations \(\mathcal {I}(\mathsf {c})\) in \(\mathfrak {I}\). We say that a clashing assumption \(\langle \alpha , {\mathbf {e}} \rangle \in \chi (\mathsf {c})\) is justified for a \( CAS \) model \(\mathfrak {I}_{ CAS }\), if some clashing set \(S = S_{\langle \alpha ,{\mathbf {e}} \rangle ,\mathsf {c}}\) exists such that, for every CAS-model \(\mathfrak {I}_{ CAS }' = \langle \mathfrak {I}',\chi \rangle \) of \(\mathfrak {K}\) that is \(\mathrm {NI}\)-congruent with \(\mathfrak {I}_{ CAS }\), it holds that \(\mathcal {I}'(\mathsf {c}) \models S_{\langle \alpha ,{\mathbf {e}} \rangle ,\mathsf {c}}\).

Definition 9 (justified CAS model)

A \( CAS \) model \(\mathfrak {I}_{ CAS }\) of a sCKR \(\mathfrak {K}\) is justified, if every \(\langle \alpha , {\mathbf {e}} \rangle \in CAS \) is justified in \( CKR \).

To interpret the intended preference on defeasible axioms, sCKR models not only need to require the existence of a CAS model justifying the exceptions, but also require that such CAS model “minimizes” the position in the hierarchy of the overridden defeasible axioms: in this way, in case of alternative solutions, axioms at the lower parts of the coverage hierarchy (i.e. more specific) are preferred to axioms at the higher contexts (i.e. more general). In the current setting, model preference is defined from local priority by the following condition:

\(\mathfrak {I}^1_{ CAS } = \langle \mathfrak {I}^1, \chi _1 \rangle \) is preferred to \(\mathfrak {I}^2_{ CAS } = \langle \mathfrak {I}^2, \chi _2 \rangle \) iff there exists some \(\mathsf {c}\in \varvec{\mathsf {N}}\) s.t. \(\chi _1(\mathsf {c}) > \chi _2(\mathsf {c})\) and not \(\chi _2(\mathsf {c}) > \chi _1(\mathsf {c})\), and for no context \(\mathsf {c}' \ne \mathsf {c}\in \varvec{\mathsf {N}}\) it holds that \(\chi _1(\mathsf {c}') < \chi _2(\mathsf {c}')\) and not \(\chi _2(\mathsf {c}') < \chi _1(\mathsf {c}')\).

We note that this definition of model preference (together with the ordering on clashing assumption sets) provides a non-symmetric and non-transitive relation over models.

Definition 10 (CKR model)

An interpretation \(\mathfrak {I}\) is a CKR model of a sCKR \(\mathfrak {K}\) (in symbols, \(\mathfrak {I}\models \mathfrak {K}\)) if:

  • \(\mathfrak {K}\) has some justified CAS model \(\mathfrak {I}_{ CAS }= \langle \mathfrak {I}, \chi \rangle \);

  • there exists no justified CAS model \(\mathfrak {I}_{ CAS }' = \langle \mathfrak {I}, \chi ' \rangle \) that is preferred to \(\mathfrak {I}_{ CAS }\).

Example 2

Considering the sCKR \(\mathfrak {K}_{org}\) of previous example, we note that different justified \( CAS \) models are possible, corresponding to the different assignments of the supervisor individual i in the \(\mathsf {c}_ local1 \) context to the alternative product areas denoted by the defeasible axioms in the upper contexts. We have three possible assignments, corresponding to three different clashing assumptions maps for the local context:

$$\begin{aligned} \begin{array}{ll} \chi _1(\mathsf {c}_ local1 ) = \{\langle S \sqsubseteq E, i \rangle , \langle S \sqsubseteq R, i \rangle \} \\ \chi _2(\mathsf {c}_ local1 ) = \{\langle S \sqsubseteq M, i \rangle , \langle S \sqsubseteq R, i \rangle \} \\ \chi _3(\mathsf {c}_ local1 ) = \{\langle S \sqsubseteq M, i \rangle , \langle S \sqsubseteq E, i \rangle \} \end{array} \end{aligned}$$

By the definition of ordering on clashing assumption sets, we have in particular that:

$$\chi _1(\mathsf {c}_ local1 )> \chi _2(\mathsf {c}_ local1 ) \qquad \chi _1(\mathsf {c}_ local1 )> \chi _3(\mathsf {c}_ local1 ) \qquad \chi _3(\mathsf {c}_ local1 ) > \chi _2(\mathsf {c}_ local1 )$$

Thus, following the definition of model preference, there is one preferred model for our sCKR which corresponds to \(\chi _1\): note that it corresponds to the intended interpretation in which the defeasible axiom \({\mathrm D}(S \sqsubseteq M)\) associated to the most specific context wins over the more general rules asserted for the higher contexts. \(\Diamond \)

We remark that the presented local model preference relation is only one of the possible solutions for an ordering condition that encodes our intended reading for the priority of overridings. Further ordering conditions can be devised e.g. by considering instances and axioms in comparisons or different properties of the ordering relation. We leave the formulation and study of properties for such alternative orderings as a direction for future work.

Reasoning and Complexity. We summarize in the following the reasoning tasks and the main complexity results as in [7]. We consider these reasoning tasks:

  • -entailment, where denotes for an axiom \(\alpha \) that \(\alpha \) is entailed in every CKR-model of \(\mathfrak {K}\) at context (i.e., );

  • (Boolean) conjunctive query (CQ) answering \(\mathfrak {K}\models \exists \mathbf {y}\gamma (\mathbf {y})\), where \(\gamma (\mathbf {y}) = \gamma _1\wedge \cdots \wedge \gamma _m\) is a conjunction of atoms , where each is a context name and \(\alpha _i(\mathbf {t}_i)\) is an assertion in which variables occur, which is existentially closed.

It has been shown in [4] that justified \( CAS \)-model checking, i.e. deciding whether a given \( CAS \)-interpretation is a justified \( CAS \)-model of a given CKR \(\mathfrak {K}\) is feasible in polynomial time, and that satisfiability (existence of a CKR-model) is NP-complete. Furthermore, -entailment testing and (Boolean) CQ-answering were shown to be coNP- and \(\varPi ^p_2\)-complete problems, respectively.

In the case of reasoning with contextual hierarchies, while the complexity of satisfiability remains unchanged, model checking is intractable already for the ranked hierarchies of [7]. As a consequence, the complexity of -entailment increases, while CQ answering remains unchanged. In what follows, we assume the setting of [4] for the complexity analysis.

Proposition 1

Deciding whether a CAS-interpretation \(\mathfrak {I}_{ CAS }\) of a sCKR \(\mathfrak {K}\) is a CKR-model is coNP-complete.

Informally, \(\mathfrak {I}_{ CAS }\) can be refuted if it is not a justified CAS-model of \(\mathfrak {K}\), which can be checked in polynomial time using the techniques in [4], or some preferred model \(\mathfrak {I}'_{ CAS }\) exists; the latter can be guessed and checked in polynomial time. The coNP-hardness can be shown by a reduction from a variant of UNSAT.

Theorem 1

Suppose \(\mathfrak {K}\) is a sCKR with global preference induced by a local preference > that is polynomial-time decidable. Then deciding -entailment is \(\varPi ^p_2\)-complete.

In particular, we note that the model ordering we propose in this paper satisfies the condition (CP) considered in [7] to motivate the \(\varPi ^p_2\)-hardness.

Theorem 2

Deciding whether an sCKR \(\mathfrak {K}\) entails a Boolean CQ \(\gamma \) is \(\varPi ^p_2\)-complete for profile-based preference.

These results can be motivated similarly: intuitively, a CKR-model \(\mathfrak {I}_{ CAS }\) that does not entail \(\gamma \) can be guessed and checked with the help of an NP oracle (ask whether no preferred \(\mathfrak {I}'_{ CAS }\) exists and whether \(\gamma \) is entailed), and similarly for local preference. The \(\varPi ^p_2\)-hardness is inherited from ordinary CKR.

For data complexity (i.e. the CKR \(\mathfrak {K}\) is fixed and only the assertions in the knowledge modules vary), while CKR model checking remains coNP-complete, the complexity of -entailment drops to \(\varDelta ^p_2[O(\log n)] = \mathrm{P^{NP}}|_{\Vert [k]}\) (cf. [10]): the problem can be decided with a constant number k of rounds of parallel NP oracle queries and it is complete for this class. On the other hand, CQ entailment remains \(\varPi ^p_2\)-complete.

3 Reasoning Procedure for General Hierarchies

In this section we adapt the reasoning method for sCKR in \(\mathcal {SROIQ}\text {-RL}\) presented in [7] to the case of general hierarchies. Basically, the datalog translation presented in [7] (and based on the one in [4]) can be adopted to the current setting for reasoning with simple CKRs and local defeasible axioms: while in the translation in [4] inference is obtained from all answer sets of the resulting program (i.e. cautious reasoning), in order to reason on the inheritance of local defeasible axioms we need to select the preferred answer sets accordingly to the model ordering defined on sCKR models. However, in this case we can not take advantage of a specific form of the contextual hierarchies: thus, we provide a general algorithm (based on the semantic definition of model preference) to compute the preferred models w.r.t. the ordering of their clashing assumptions.

Language and Normal Form. As in the original version of the translation, we limit the defeasible axioms to the language of \(\mathcal {SROIQ}\text {-RLD}\): i.e. in defeasible axioms, \(D \sqcap D\) can not appear as a right-side concept and each right-side concept \(\forall R.D\) has \(D \in \mathrm {NC}\). Also, we consider the normal form and normal form transformation proposed in [4] for the formulation of the rules (considering the formulas that can appear in the simple CKRs) and we assume again the Unique Name Assumption.

Translation Overview. The translation to datalog extends the one presented in [4]: the non-trivial use of non-monotonic negation and inference on negative literals by contradiction for the interpretation of exceptions is here extended to reason on local defeasible inheritance. However, since we do not consider the computation of preference in the translation, differently from rules in [7] we do not consider weak constraints on the level of overriding.

Formally, we consider the datalog translation composed by the rules in [8] by leaving out the rules in Table 8 and the global input rule for the interpretation of levels (igl-level) in Table 3.

As in the original formulation (inspired by the materialization calculus in [15]), the translation includes sets of input rules (which encode DL axioms and signature in datalog), deduction rules (datalog rules providing instance level inference) and output rules (that encode in terms of a datalog fact the ABox assertion to be proved). The translation is composed by the following sets of rules:

\(\mathcal {SROIQ}\text {-RL}\) Input and Deduction Rules: rules in \(I_{rl}(S, c)\) translate to datalog facts (in a given context c) \(\mathcal {SROIQ}\text {-RL}\) axioms and signature. For example, atomic concept inclusions are translated with the rule \(A \sqsubseteq B \mapsto \{\mathtt{subClass}(A,B,c)\}\). Deduction rules in \(P_{rl}\) encode the inference rules for \(\mathcal {SROIQ}\text {-RL}\) axioms: e.g., for atomic concept inclusions:

$$\begin{aligned} \mathtt{instd}(x,z,c,t) \leftarrow \mathtt{subClass}(y,z,c), \mathtt{instd}(x,y,c,t). \end{aligned}$$

Global and Local Translations: global input rules \(I_{glob}(\mathfrak {C})\) encode the interpretation of the contextual structure. E.g., \(\mathsf {c}_1 \prec \mathsf {c}_2 \mapsto \{\mathtt{prec}(\mathsf {c}_1, \mathsf {c}_2)\}\) translates coverage across contexts as instances of the \(\mathtt{prec}\) predicate. Local input and deduction roles implement the interpretation of \(\textit{eval}\): note that differently from [4], \(\textit{eval}\) can be only defined over single contexts instead of context classes.

Defeasible Axioms Input Translations: defeasible input rules \(I_{{\mathrm D}}(S,c)\) declare that a local axiom is defeasible: differently from the translation in [4], the resulting atoms also contain the context in which the axiom has been introduced. For example, \({\mathrm D}(A \sqsubseteq B)\) in context \(\mathsf {c}\) translates to \(\mathtt{def\_subclass}(A,B,\mathsf {c})\).

Overriding Rules: overriding rules in \(P_{\mathrm D}\) provide rules defining when an axiom of a certain form is locally overridden. With respect to rules in [4], this version of overriding rules has to consider the context in which the defeasible axiom has been declared: this is needed in order to reason on the local preference of the overridden axiom in the algorithm for the computation of preferred models. For example, for axioms of the form \({\mathrm D}(A \sqsubseteq B)\) in context \(\mathsf {c}\):

figure a

Inheritance Rules: \(P_D\) provides the rules for defeasible inheritance of axioms from the higher to the lower local contexts in the coverage structure. The definition of rules in the case of (general) hierarchies also considers the \(\mathtt{prec}\) relation across contexts, which defines the direction of inheritance. E.g., the following rule propagates a (possibly defeasible) atomic concept inclusion axiom:

figure b

Note that this rule propagates also to instances of strict axioms, since their overriding is never verified.

Test Rules: the test rules in \(P_{\mathrm D}\) are used to instantiate and define the “environments” for the tests for negative literals in overriding rules. The mechanism is analogous to the one in [4], but rules need to be adapted to the new definition of \(\mathtt{ovr}\) atoms and \(\mathtt{prec}\) (i.e., they need to consider the context in which the axiom has been declared).

Fig. 2.
figure 2

Procedure \({\texttt {PrefModels}}\) for computation of answer set preference

Fig. 3.
figure 3

Procedure \({\texttt {lessThanM}}\) for comparison of answer sets

Model Preference Algorithm. The presented translation computes all justified models for the input sCKR: in order to recognize the preferred models, we need to apply to the computed answer sets the conditions of the model ordering definition. In the case of general hierarchies, we provide the algorithm \({\texttt {PrefModels}}\) that, given the sCKR translation \(PK(\mathfrak {K})\) as input, produces the set of preferred answer sets as output.

A pseudo-code for \({\texttt {PrefModels}}\) is presented in Fig. 2: for every answer set A of the input program, the procedure tests whether there does not exist a different answer set B for which \({\texttt {lessThanM}}(A,B)\) holds (i.e. A is minimal w.r.t. the preference). If that is the case, A is added to the set of results (i.e. preferred models).

The procedure for \({\texttt {lessThanM}}\) is shown in Fig. 3. Intuitively, it provides a comparison between two input answer sets A and B by implementing the condition for model comparison: A is recognized as preceding B if there exists a context \(\mathsf {c}\in \varvec{\mathsf {N}}\) such that the preference on clashing assumptions in context \(\mathsf {c}\) (tested by the procedure \({\texttt {lessThanCAS}}\)) is verified and in no other context this order is disregarded.

The procedure for \({\texttt {lessThanCAS}}\) is presented in Fig. 4. It provides a comparison across clashing assumptions sets for the specific context \(\mathsf {c}\) from the input answer sets A and B, based on the definition of local (clashing assumption sets) preference in the semantics: with respect to \(\mathsf {c}\), B is preferred to A if, for every clashing assumption (i.e. \(\mathtt{ovr}\) atom) from B (and not in A) on a defeasible axiom in , there exists a clashing assumption from A (and not in B) on a defeasible axiom in such that \(\mathsf {c}_1 \prec \mathsf {c}_2\).

Fig. 4.
figure 4

Procedure \({\texttt {lessThanCAS}}\) for comparison on clashing assumptions sets

We note that, in case of a transitive definition of the model preference, we can modify \({\texttt {PrefModels}}\) so that the pre-computation and storage of all answer sets is not needed: we can compute an answer set A of P at a time and verify if the \({\texttt {lessThanM}}\) condition holds w.r.t. a set of candidate models \( Cand \) (initially empty); in case A is recognized as a candidate for preferred model, it is added to \( Cand \) and any other model B in \( Cand \) s.t. \({\texttt {lessThanM}}(B,A)\) is removed from \( Cand \).

Translation Process. Given a sCKR \(\mathfrak {K}= \langle \mathfrak {C}, \mathrm {K}_{\varvec{\mathsf {N}}} \rangle \) in \(\mathcal {SROIQ}\text {-RLD}\) normal form, a program \(PK(\mathfrak {K})\) that encodes \(\mathfrak {K}\) is obtained as follows:

  1. 1.

    the global program for \(\mathfrak {C}\) is built as: \(PG(\mathfrak {C}) = I_{glob}(\mathfrak {C})\)

  2. 2.

    for each \(\mathsf {c}\in \varvec{\mathsf {N}}\), we define each local program \(PC(\mathsf {c}, \mathfrak {K})\) as: \(PC(\mathsf {c}, \mathfrak {K}) = P_{rl} \cup P_{loc} \cup P_{{\mathrm D}} \cup I_{loc}(\mathrm {K}_\mathsf {c}, \mathsf {c}) \cup I_{rl}(\mathrm {K}_\mathsf {c}\cup \mathrm {K}_\mathsf {c}^{\mathrm D}, \mathsf {c}) \cup I_{{\mathrm D}}(\mathrm {K}_\mathsf {c}, \mathsf {c})\) where \(\mathrm {K}_\mathsf {c}^{\mathrm D}= \{\alpha \in \mathcal{L}_\varSigma \,|\,{\mathrm D}(\alpha ) \in \mathrm {K}_\mathsf {c}\}\).

  3. 3.

    The CKR program \(PK(\mathfrak {K})\) is defined as: \(PK(\mathfrak {K}) = PG(\mathfrak {C}) \cup \bigcup _{\mathsf {c}\in \varvec{\mathsf {N}}} PC(\mathsf {c}, \mathfrak {K})\)

Query answering \(\mathfrak {K}\models \mathsf {c}: \alpha \) is then obtained by testing whether the (instance) query, translated to datalog by \(O(\alpha , \mathsf {c})\), is a consequence of the preferred models of \(PK(\mathfrak {K})\), i.e., whether \({\texttt {PrefModels}}(PK(\mathfrak {K})) \models O(\alpha , \mathsf {c})\) holds. Analogously, this can be extended to conjunctive queries as in [4].

Correctness. We can show that the presented process provides a sound and complete reasoning method for instance checking (with respect to \(\mathsf {c}\)-entailment) and conjunctive query answering for normal form \(\mathcal {SROIQ}\text {-RLD}\) simple CKRs with general context hierarchies. The result is shown by extending the correspondence between minimal justified CKR-models of \(\mathfrak {K}\) and answer sets of \(PK(\mathfrak {K})\) from [4] to the “preferred” answer sets computed by the PrefModels algorithm. As in the original formulation, the adoption of UNA and named models (i.e. restricting to models having a \(N \subseteq \mathrm {NI}\setminus \mathrm {NI}_S\) s.t. the interpretation of atomic concepts and roles belongs to \(N^\mathcal{I}\)) allows to concentrate on Herbrand models for \(\mathfrak {K}\), denoted as \(\hat{\mathfrak {I}}(\chi )\).

Let \(\mathfrak {I}_{ CAS } = \langle \mathfrak {I}, \chi \rangle \) be a justified named CAS-model. We can build from its components a corresponding Herbrand interpretation \(I(\mathfrak {I}_{ CAS })\) of the program \(PK(\mathfrak {K})\): the construction is similar to the one in [4] (and its adaptation to hierarchies detailed in [8]).

It is then possible to show that the answer sets of the final program \(PK(\mathfrak {K})\) correspond with the least justified models of \(\mathfrak {K}\) by the following result:

Lemma 1

Let \(\mathfrak {K}\) be a sCKR in \(\mathcal {SROIQ}\text {-RLD}\) normal form, then:

  1. (i).

    for every (named) justified clashing assumption \(\chi \), the interpretation \(S = I(\hat{\mathfrak {I}}(\chi ))\) is an answer set of \(PK(\mathfrak {K})\);

  2. (ii).

    every answer set S of \(PK(\mathfrak {K})\) is of the form \(S = I(\hat{\mathfrak {I}}(\chi ))\) with \(\chi \) a (named) justified clashing assumption for \(\mathfrak {K}\).

As in the case of [7], the result can be proved along the lines of Lemma 6 in [4] by showing that the answer sets of \(PK(\mathfrak {K})\) coincide with the sets \(S=I(\hat{\mathfrak {I}}(\chi ))\) where \(\chi \) is a justified clashing assumption of \(\mathfrak {K}\).

In the case of general hierarchies, the correspondence with sCKR models is obtained by considering the set of answer sets returned by the \({\texttt {PrefModels}}\) algorithm and the notion of model preference on justified \( CAS \)-models in the semantics.

Lemma 2

Let \(\mathfrak {K}\) be a sCKR in \(\mathcal {SROIQ}\text {-RLD}\) normal form. Then, \(\hat{\mathfrak {I}}\) is a CKR model of \(\mathfrak {K}\) iff there exists a (named) justified clashing assumption \(\chi \) s.t. \(I(\hat{\mathfrak {I}}(\chi ))\) is a preferred answer set of \({\texttt {PrefModels}}(PK(\mathfrak {K}))\).

Proof (Sketch)

The existence of a justified \(\chi \) corresponds to the first condition of Definition 10 and is derived from Lemma 1. Then, we have to show that \(I(\hat{\mathfrak {I}}(\chi ))\) is an answer set returned by \({\texttt {PrefModels}}(PK(\mathfrak {K}))\) if it corresponds to a preferred (justified) model of \(\mathfrak {K}\) as in the second condition of Definition 10. This can be verified by the formulation of the algorithm: the procedure \({\texttt {lessThanCAS}}\) applies the definition of preference on clashing assumption sets to the corresponding \(\mathtt{ovr}\) atoms of the answer sets; the preference is then lifted to preference on answer sets by \({\texttt {lessThanM}}\) using the definition of model preference; finally, \({\texttt {PrefModels}}\) applies this preference test on all answer sets, in order to verify that there does not exist other answer sets that are preferred to the ones that are returned.    \(\Box \)

The correctness for instance checking is obtained as consequence of previous results:

Theorem 3

Let \(\mathfrak {K}\) be a sCKR in \(\mathcal {SROIQ}\text {-RLD}\) normal form. \(\alpha \) and \(\mathsf {c}\) such that \(O(\alpha , \mathsf {c})\) is defined. Then \(\mathfrak {K}\models \mathsf {c}:\alpha \) iff \({\texttt {PrefModels}}(PK(\mathfrak {K})) \models O(\alpha , \mathsf {c})\).

Similarly to [4], this result can be extended to answering of a conjunctive query Q, by constructing its translation O(Q) by applying output rules to its atoms.

Theorem 4

Let \(\mathfrak {K}\) be a sCKR in \(\mathcal {SROIQ}\text {-RLD}\) normal form. and let \(Q = \exists \mathbf {y}\gamma (\mathbf {y})\) be a Boolean CQ on \(\mathfrak {K}\). Then \(\mathfrak {K}\models Q\) iff \({\texttt {PrefModels}}(PK(\mathfrak {K})) \models O(Q)\).

4 Related Work

We briefly recall some relevant works related to CKR that include notions of defeasibility in contextual systems and in DLs (we refer to [4, 7] for an extended comparison).

We first notice an analogy with non-monotonic multi-context systems (MCS) [9]. The idea of MCS is to align knowledge from different contexts (locally based on possibly different logics) in a single system using non-monotonic bridge rules. CKRs with defeasible inheritance may be realized in the MCS framework by controlling knowledge propagation by bridge rules: on the other hand, in sCKR the knowledge propagation is implicitly defined by the coverage semantics. A different non-monotonic semantics for MCS was proposed in [1], based on argumentation semantics of Defeasible Logic extended with distribution of knowledge and preferences across contexts. Conflicts over external literals are resolved using a local context preference, where clashes across arguments are considered. In CKR, preference is defined by the interpretation of the coverage structure. Our notion of overriding compares to a “conflict” among two arguments for conflicting literals.

Different proposals have been made in DLs to incorporate notions of “normality” in concepts and subsumptions. For example, [12] formalize in their logic \(\mathcal {ALC}{+}\mathbf{T }_{min}\) the intuition that a prototypical element of a concept C is a “typical element” of C. The typicality operator T on concepts is interpreted by extending DL interpretations with a preference relation on the domain: each element in T(C) is a member of C minimal w.r.t. such preference. The models of \(\mathcal {ALC}{+}\mathbf{T }_{min}\) are restricted to the ones which minimize the set of exceptional instances. Similarly to our approach, in this work membership of an element in a concept must be blocked: however, instead of using model minimization, in CKR exceptions have to be justified in terms of a semantic consequence.

Another approach to represent overriding in DLs is [2]: it proposes a family \(\mathcal{D}\mathcal{L}^{N}\) of non monotonic DLs defined by extending DLs with an operator \(\text {N}C\) for normality concepts and with defeasible inclusions (DIs) \(C \sqsubseteq _n\!D\), interpreted as “normally, instances of C are instances of D, unless stated otherwise”. The semantics of a defeasible inclusion \(C \sqsubseteq _n\!D\) w.r.t. normal individuals \(\text {N}E\) is defined to manage the conflicts of inclusions on \(\text {N}E\): to decide which DIs should be overridden, a priority relation \(\prec \) is defined on DIs. The idea of axiom overriding is similar in spirit to our approach. A difference stands in the definition of precedence between defeasible axioms: in CKR, precedence is defined by the coverage hierarchy. As shown in [4], similarly to this approach we can deal with property inheritance at the instance level: however, in case of clashing inheritances that can not be resolved using preference, our semantics allows to reason by cases on all alternative models.

5 Conclusions

In this paper we extended the work introduced in [7] on CKR contextual framework with defeasible axioms in local contexts and knowledge propagation along a context hierarchy. We considered the case of general coverage hierarchies: we defined a CKR model preference relation by lifting a local preference on overridings (i.e. clashing assumptions). The ordering preserves the intuition of prioritizing the validity of defeasible axioms at more specific contexts. Then, we extended the ASP based reasoning method proposed in our previous works with an algorithm for the computation of preferred models: we have shown that this leads to a complete reasoning method for instance checking and CQ answering with respect to the proposed semantics.

There are different directions for future work. As discussed in previous sections, we are interested in defining different notion of preference on defeasible axioms: we aim to study their different semantic properties, their behavior with respect to complexity of reasoning and their different effects of knowledge propagation. We can also consider to introduce different contextual relations other than coverage (with different rules for knowledge propagation) and study their interaction. We are also interested in applying the current work on contextual hierarchies to CKRs in different DL languages (see e.g. [5]) and study different reasoning approaches and their implementation. For example, the datalog translation and the computation of preferred models by the \({\texttt {PrefModels}}\) algorithm can be implemented under a common formalism in nested HEX-programs [11].