We consider the problem of reasoning with ontologies where every axiom is associated to a context, and contexts are related through a total order. These contexts could represent, for example, a degree of trust associated to the axiom, or a level of granularity for the knowledge provided. We describe an extension of tableaux-based decision procedures into methods that compute the best-fitting context for the consequences of an ontology, and apply it to the tableaux algorithm for ALC. We also describe an execution strategy that preserves most of the standard optimizations used in modern DL reasoners.
Several non-standard reasoning tasks for DL ontologies can be described as repeated standard reasoning, over some of its sub-ontologies. This is the case, for example, in axiom-pinpointing [14,12,3], where the tasks is to identify the class of sub-ontologies entailing a consequence, or access control [2], where users are assigned views to specific subontologies, and one wants to decide which users can or cannot deduce some implicit consequence.
One can think of the sub-ontologies over which standard reasoning is performed as contextual views to the whole ontology. The task is then to partition the contexts into those that entail and those that do not entail the desired consequence. An obvious way to solve this task is to test each of the potentially exponentially many sub-ontologies for the consequence, and classify them according to the result. However, it is possible to exploit the structure of the set of contexts to obtain a more efficient method.
Notice that every set of sub-ontologies defines a partial ordering ≤ via the superset relationship: O ≤ O iff O ⊆ O. This partial order can always be extended to a lattice in which every context is join-prime [6]. It has been shown that there is an element ν in this lattice, called the boundary, such that the following holds for every context O represented by a label O : O entails the consequence iff O ≤ ν [2]. If the lattice is distributive, then the boundary can be computed in polynomial time on the size of the input ontology [3].
So far, all the methods implemented for computing boundaries are based on a black-box approach, in which an unmodified reasoner is called repeatedly until the boundary has been found. In fact, attempts to produce a glass-box approach for e.g. axiom-pinpointing [4], where the reasoner is modified to directly compute the boundary, encounter the problem that most of the optimizations used in implemented DL reasoners do not work in the modified procedures, making the glass-box approaches much less efficient than black-box ones. Moreover, glassbox extensions are not even guaranteed to terminate.
In this paper we focus on a special case in which the contexts are linearly ordered. That is, for every pair of sub-ontologies O, O , either O ⊆ O or O ⊆ O. This simple setting still covers a wide variety of applications, such as possibilistic reasoning [13,11], trust management, or granularity reasoning. We develop a glass-box approach for extending tableau-based decision algorithms into procedures that compute the boundary for the consequence decided by the original tableaux. A prioritization ordering of the rule applications of these procedures ensures that the boundary-computation procedure behaves almost identically to the original tableau. This entails not only termination of the algorithm, but also that most of the optimization techniques used by modern DL reasoners are still applicable to the extensions. An additional benefit of our method is that it can deal with arbitrary blocking conditions, without losing its correctness.
The paper is divided as follows. We first introduce the basic reasoning problems we are interested in, followed by a general notion of tableaux. In Section 4 we describe the labeled extensions of tableaux, that output a boundary for the desired property, and provide the prioritization ordering that ensures that these extensions behave well. We wrap up by arguing that our approach can be seen as a special case of incremental reasoning, and hence should be easy to implement in modern DL reasoners.
We start by introducing the general notion of consequence properties that are decided by general tableaux. To avoid unnecessary confusion, we present slightly simplified versions of the notions of consequence properties and tableaux, which suffice for the goals of this paper. We consider also a general notion of axioms, which can e.g. be assertions, GCIs, or concept definitions. then O exa ∈ P exa ; that is, O exa is inconsistent. In general, we will call the sets O ∈ P f in (O) ontologies.
For several applications, axioms cannot be considered to have all equal importance, but are provided with a label that represents the context to which they belong. We consider only labels that come from a finite totally ordered set (L, ≤). For the rest of this paper, we will denote the elements of L as 0 , 1 , . . . , k , with the implicit ordering i ≤ j iff i ≤ j. In particular, 0 is the least-and k is the greatest-element of L.
We will use the elements of the set L to define different contexts of an ontology. Depending on the specific application at hand, these contexts can have different meanings, such as access rights, level of expertise, trustworthiness, necessity degree, etc.
Every axiom t in an ontology O is assigned a label lab(t) ∈ L, which expresses the contexts from which this axiom can be accessed. An ontology extended with such a labeling function lab will be called a labelled ontology. Each element ∈ L defines the context sub-ontology
For a given labeled ontology, we want to compute the so-called boundary of the c-property P. Intuitively, the boundary divides the contexts where P follows from those where it does not follow. Definition 2. Let O be a labeled ontology and P a c-property. An element ν ∈ L is called a (O, P)-boundary if for every element ∈ L the following holds:
When it is clear from the context, we will usually omit the prefix (O, P), and call this ν a boundary.
Continuing with our example, let the label of every axiom appearing in (1) be lab(ax i ) = i , 1 ≤ i ≤ 4. The (O exa , P exa )-boundary is then 2 since the subontology O ≥ 2 = {¬A B(b), ∀r.A(a), r(a, b)} is inconsistent, while the ontology O ≥ 3 = {∀r.A(a), r(a, b)} is consistent, i.e. does not belong to P exa .
It was shown in [2] that if O ∈ P, then the (O, P)-boundary always exists, is unique, and can be computed using axiom-pinpointing techniques. Given an ontology O that belongs to a c-property P, a minimal (w.r.t. set inclusion) subontology O ⊆ O that still belongs to P is called a MinA for O, P. 1 If O 1 , . . . , O m are all the MinAs for O, P, then
is the (O, P)-boundary. However, using this method for computing the boundary may result in an unnecessary overhead. In our running example, we can see that {ax 1 , ax 2 , ax 4 } and {ax 2 , ax 3 , ax 4 } are the MinAs for O exa , P exa . The second MinA has label 2 . If we happen to compute this second MinA first, then there is no need to continue computing MinAs, as it is clear that any new MinA O must contain the axiom ax 1 , and hence have label 1 < 2 . This new MinA will have no influence in the computation of the maximum from Equation ( 2). This problem is in fact more pronounced than what the example shows, since a single ontology can have exponentially many MinAs [5], and the boundary can be computed by a black-box algorithm that calls a decision procedure for P at most k = |L| times; namely, once for each ∈ L, to decide whether or not O ≥ ∈ P.
In this section we recall some of the notions of general tableaux [4]. We use V and D to denote two disjoint, countably infinite sets of variables and constants, respectively. A signature Σ is a set of predicate symbols, where each predicate P ∈ Σ is equipped with an arity. A Σ-assertion is of the form P (a 1 , . . . , a n ) where P ∈ Σ is an n-ary predicate and a 1 , . . . , a n ∈ D. Similarly, a Σ-pattern is of the form P (x 1 , . . . , x n ) where P ∈ Σ and x 1 , . . . , x n ∈ V. Whenever the signature is clear from the context, we simply say pattern (assertion). Given a set of assertions A (resp. patterns B), cons(A) (resp. var(B)) denotes the set of constants (resp. variables) occurring in A (resp. B).
A substitution is a mapping σ : V → D, where V ∈ P f in (V). In this case, we say that σ is a substitution on V. The substitution
An S-state is a pair S = (A, O) where A is a finite set of assertions and O is a finite set of axioms. The tableau algorithm works on sets of S-states. It starts with the set M = {(∅, O)} and uses the rules in R to modify this set. Each rule application picks an S-state S from M and replaces it by finitely many new S-states that extend the first component of S. When no rules are applicable, then it tests whether the resulting set of S-states contains a clash; in that case, it accepts the ontology, and rejects it otherwise.
and (iii) for every 1 ≤ i ≤ m and every substitution ρ on var(B 0 ∪ B i ) extending ρ we have
Given a set of S-states M, application of an input rule
where σ is a substitution that extends ρ and maps the fresh variables of R to distinct new constants. If M is obtained from M by a rule application, we write
The S-state (A, O) contains a clash if there is a C ∈ C and a substitution ρ on var(C) with Cρ ⊆ A. M is full of clashes if every S ∈ M contains a clash.
A simple example of a tableau is the one for deciding inconsistency of ALC ABoxes. Its clashes are all the sets {D, ¬D}, where D is a concept name. It has different expansion rules dealing with the constructors of ALC. For example, the rules for existential restrictions and disjunction are as follows:
It also has input rules, for dealing with the ABox axioms used. For example, for concept assertions, we use
where a is the constant representing the individual name a.
A tableau is correct for a c-property P if every chain of rule applications starting with M 0 = {(∅, O)} eventually reaches a saturated set of S-states M (i.e. it terminates) and it holds that O ∈ P iff M is full of clashes.
In general, tableaux are not guaranteed to terminate, as their expansion rules may trigger the applicability of new expansion rules. This happens, for instance, in the tableaux algorithm for deciding inconsistency w.r.t. general TBoxes. To avoid this problem, a blocking condition is usually introduced. Intuitively, blocking disallows the application of a rule, whenever its application would not lead to the production of any new clashes; that is, when further expansions would not change the acceptance status of the input ontology. Several blocking conditionslike e.g. subset blocking [1], equality blocking [7], pairwise blocking [8], etc-have been studied in the literature. Rather than trying to define and deal with each of these conditions independently, we consider a general notion of blocking.
A blocking condition is simply a set of finite sets of Σ-assertions and Σpatterns, using only the variables from var(B 0 ). Intuitively, these describe the situations in which the rule should not be applied. Every expansion rule is then extended with a blocking condition B, and the rule applicability condition is restricted to satisfy additionally (iv) A / ∈ Bρ. The notions of saturated sets of Sstates and correctness w.r.t. a c-property are adapted accordingly. For example, the subset blocking condition disallowing the applicability of the existential rule in ALC is described by the set of all finite sets of Σ-assertion and Σ-patterns B where the only variable used is x and such that there exist constants a 1 , . . . , a n and roles r 1 , . . . , r n such that r i (a i , a i + 1) for all i, 1 ≤ i < n, r i (a n , x), and
In the next section, we show how to transform tableaux that are correct for a c-property P into procedures that directly compute the (O, P)-behaviour, for any given ontology O. We focus first on tableaux without any blocking condition, which can be used for deciding consistency of ALC ABoxes. Later on, we show how to extend this construction to tableaux with blocking conditions, allowing us to reason w.r.t. general TBoxes also.
Given a tableau S that is correct for the c-property P, we show how to construct an algorithm that computes the boundary for P. For the moment, we focus on tableaux without blocking conditions, but later describe how to deal with blocking also.
For an input labeled ontology O, the modified algorithm also works on sets of S-states, but every assertion a occurring in the first component of an S-state is also equipped with a label lab(a); we call this a labeled S-state. The application of rules must take the labels of the assertions and axioms into account.
If A is a set of labeled assertions and ∈ L, then we say that an assertion a is -insertable into A if either (i) a / ∈ A or (ii) a ∈ A but > lab(a). Given a set B of (unlabeled) assertions and a set A of labeled assertions, the set of -insertable elements of
where is the degree of the rule application, defined above, and σ is a substitution that extends ρ and maps the fresh variables of R to distinct new constants. If M is obtained from M by a labeled rule application, we write M → S lab M . M is labeled saturated if there is no M with M → S lab M .
Consider a finite chain of labeled rule applications {(∅, O)} * − → S lab M such that M is labeled saturated. The label of an assertion appearing in M expresses the contexts that can derive this assertion. A clash in an S-state depends on the joint presence of possibly several assertions; thus, we need to find the contexts from which all of these assertions can be derived: this is given by the minimum of the labels of all these assertions. To decide the property P, it suffices to have one clash per S-state S; hence, we are only interested in the maximum of the labels of all the clashes in a given state. As every S-state in M is required to have at least one clash, we again compute the minimum of the labels obtained from each S-state. We formalize this next. Definition 6. A set of assertions A is called a clash set in a labeled S-state S = (A, O) if there is a clash C ∈ C and a substitution ρ on var(C) with A = Cρ.
Given a set of labeled S-states M = {S 1 , . . . , S n }, the clash degree induced by
It can be shown, using similar techniques to the ones developed in [4] for pinpointing extensions of general tableaux that the clash degree is always the boundary for the c-property decided by the original tableau. Notice that this result does not depend on the order in which rules are applied. From a given set of S-states, several rules could be applicable, but the correctness of the labeled extension does not depend on which one is chosen first. This is an important feature of tableaux and their extensions, as it allows optimizations based on the choice of an ordering that leads to shorter chains of rule applications.
Unfortunately, this general approach for extending tableaux into boundarycomputation methods also inherits some of the negative properties of pinpointing extensions of tableaux. In particular, (i) the labeled extension of a terminating tableau is not guaranteed to terminate (see [4] for an example), and (ii) even if it terminates, the labeled extension needs to run until saturation to guarantee that the clash label computed is indeed the boundary. The second point is used as an argument against glass-box approaches, as it disallows one of the most basic optimizations for tableaux, namely stopping the application of expansion rules on states where a clash has already been detected.
We now show that if we prioritize rule applications with a higher degree, then both of these problems disappear. Moreover, the same approach will allow us to deal with general blocking conditions in Section 4.2.
By definition, the boundary is the largest context from which the c-property can be derived. A simple idea to compute this boundary is then to try to first produce all the assertions that can be derived from a context-that is, from all the axioms having a label greater or equal to some i -before applying rules that use axioms with a smaller label. We implement this idea by prioritizing labeled rule applications with a higher degree. Definition 8. The ordered extension of a tableau S is the labeled extension of S where, if several rules are applicable to a set of labeled S-states M, then one rule application having the highest degree is applied.
We write M → S ord M if M is obtained from M by an ordered rule application. M is ordered saturated if there is no M with M → S ord M .
Several rule applications may have the same (highest) degree. In that case, it is irrelevant which one of these is chosen. This prioritization ordering has the consequence that the degree of successive rule applications is non-increasing.
obtained by applying a rule with degree to M 1 , and M 1 is obtained by applying a rule with degree to M 0 , then ≤ .
Proof. M 1 differs from M 0 by having some S-states S 1 , . . . , S m that modify the assertional component of a S-state S ∈ M 0 in the following way: some new assertions labeled with are added, and some existing assertions get their label increased to . In any case, all assertions appearing in some S-state of M 1 with label greater than are also in an S-state of M 0 . If > , then all the assertions and axioms used to execute the rule M 1 → S ord M 2 have a label strictly greater than , and hence this rule was applicable also to an S-state in M 0 . But > implies that would not be applied, since it violates the prioritization ordering. hence ≤ .
A simple consequence of this lemma is that the labels of assertions appearing in the S-states are never modified by further ordered rule applications, as such modification would imply a rule application with a higher degree than the rule that originally created the assertion. This means that a rule is only ordered applicable if it adds new assertions to the S-state, and thus, for any set of Sstates reachable from the initial set {(∅, O)} a rule is ordered applicable iff it is applicable in the original sense of Definition 4, as described by the following theorem.
Theorem 10. Let S be a tableau over O and O ∈ P f in (O). For every set of labeled S-states M, it holds that
where is the smallest label appearing in M.
In particular, if S terminates in every input-as is the case for every tableau that is correct for some c-property-then its ordered extension must also terminate.
Corollary 11. The ordered extension of any terminating tableau is terminating.
More interesting, the execution of the ordered extension can be stopped as soon as the set of S-states M is full of clashes, as further rule applications will not modify the clash degree.
Corollary 12. Let M, M be sets of S-states such that M is full of clashes and
Consider now a tableau with blocking conditions associated to its rules, that is correct for a property P. In general, the same blocking condition cannot be used for restricting rule applications in its labeled extension. This would lead to a clash degree that may be strictly smaller than the actual boundary that this extension tries to compute, as can be seen by a simple adaptation from the examples provided in [10] for subset blocking and in [4] for equality blocking. The reason for this is that, since the blocking condition is independent of the labels used, it might be that the assertions that trigger the blocking of a rule application may depend on different contexts.
To solve this problem, a modification of the blocking condition that also takes into account the labels was proposed in [10,4]. However, it is not clear whether more complex blocking conditions would require a more elaborate labeled extension. Moreover, we want to produce a boundary-computing algorithm that works for any kind of blocking condition that fits our very general framework.
Fortunately, if we consider the prioritized rule-application ordering of ordered extensions of tableaux, we can use Theorem 10 and Corollary 12 to show that the same blocking conditions yield a correct computation of the boundary.
To define the labeled extensions of tableaux with blocking, we adapt the notion of labeled applicability of a rule to take into account the blocking condition. An expansion rule R with a blocking condition B is labeled applicable to a labeled S-state (A, O) if it satisfies the three conditions from Definition 5 and additionally (iv) A / ∈ B. If a tableau with blocking is correct for a c-property P, then it terminates on every input and when it reaches a saturated set of S-states, this is full of clashes iff the input ontology satisfied the property. We thus have the following result.
Theorem 13. Let P be a c-property on O and S a correct tableau (with blocking) for P. For every ontology O ∈ P f in (O) the following holds:
the ordered extension of S terminates on O; that is, there is no infinite chain of rule applications {(∅, O)} → S ord M 1 → S ord M 2 → S ord . . .; for every chain of rule applications {(∅, O)} * − → S ord M with M labeled saturated, the clash degree M induced by M is a (O, P)-boundary.
We have presented a general approach for extending general tableaux algorithms that can decide a c-property P, into methods that can compute the boundary for P w.r.t. to a set of linearly ordered contexts. Our approach can be used for extending the tableau-based algorithm for deciding consistency of ALC ABoxes w.r.t. general TBoxes, but is not limited to this logic. In fact, adding transitive and inverse roles, or considering more complex blocking conditions would not be a problem for our framework. However, our notion of general tableaux requires a monotonic extension of the consequences deduced, and cannot identify previously introduced individuals in a clean way. In future work we will study whether we can construct a tableau for reasoning in full SROIQ(D).
Our approach follows the lines of pinpointing extensions of tableaux, but has several advantages over these, mainly due to the simplicity of the linear ordering. By prioritizing the rule applications according to their degree-applying rules with higher degree first-we obtained an algorithm that does not differ much from the original tableau. The main intuition behind this prioritization of the rule applications is that it deduces all the consequences from a context higher in the ordering before testing contexts defined by a smaller label. Labeled rule applications using this ordering never modify the label of a previously existing assertion, and always add new assertions with non-increasing labels. Thus, chains of ordered rule applications correspond to rule applications of the original tableau. This in particular ensures that termination of a tableau transfers to its ordered extension, a property that is not shared by pinpointing extensions, or extensions based on lattices that are not linearly ordered.
The execution of ordered extensions of tableaux can be seen as incremental reasoning: given an ontology O, the ordered extension first saturates the tableau using only the axioms having the greatest label n . If this produces a set of Sstates that is full of clashes, then we know that n is the boundary for (O, P). Otherwise, it adds the axioms with label n−1 , and continues the tableau execution. Since several DL reasoners now implement incremental reasoning (e.g. Pellet,2 FaCT++,3 or CEL4 ), we believe that an implementation of our glassbox approach for reasoning in DLs with linearly ordered contexts will be a simple step.