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 [
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 O0 iff O0 O. This partial order can always be
extended to a lattice in which every context is join-prime [
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 [
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; O0, either O O0 or O0 O.
This simple setting still covers a wide variety of applications, such as
possibilistic reasoning [
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. 2
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.
Definition 1. Let O be a set of axioms, and let Pfin(O) denote the set of all finite subsets of O. A consequence property (c-property) is a set P Pfin(O) such that O 2 P implies O0 2 P for every O O0.
Intuitively, c-properties model consequence relations in logic that are monotonic; i.e. they describe which sets of axioms have or entail a desired consequence. For example, one can consider the set O of all concept- and role-assertions in the DL ALC and Pexa the set of all inconsistent ALC ABoxes. If Oexa is the ABox having the assertions ax1 : :9r:B(a) ax2 : (:A u B)(b) ax3 : 8r:A(a) ax4 : r(a; b) (1) then Oexa 2 Pexa; that is, Oexa is inconsistent. In general, we will call the sets O 2 Pfin(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) 2 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 ` 2 L defines the context sub-ontology
O ` := ft 2 O j lab(t) `g: Clearly, if ` `0, then O `0 O `. Conversely, every ontology O defines an element O 2 L (called the label of O), given by O := minflab(t) j t 2 Og. It follows from this definition that O O0 whenever O0 O.
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 is called a (O; P)-boundary if for every element ` 2 L the following holds: 2 L ` iff
O ` 2 P.
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(axi) = `i; 1 i 4. The (Oexa; Pexa)-boundary is then `2 since the subontology O `2 = f:A u B(b); 8r:A(a); r(a; b)g is inconsistent, while the ontology O `3 = f8r:A(a); r(a; b)g is consistent, i.e. does not belong to Pexa.
It was shown in [
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 O0 must
contain the axiom ax1, 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 [
In this section we recall some of the notions of general tableaux [
A substitution is a mapping : V ! D, where V 2 Pfin(V). In this case, we say that is a substitution on V. The substitution on V 0 extends on V if V V 0 and (x) = (x) for all x 2 V . If B is a set of patterns with var(B) V , then B denotes the set of assertions obtained from B by replacing each variable by its image over the substitution .
Definition 3. Let O be a set of axioms. A tableau for O is a tuple S = ( ; R; C) where – is a signature, – R is a set of expansion rules of the form (B0; N ) ! fB1; : : : ; Bmg, where B0; : : : ; Bm are finite sets of -patterns and N 2 Pfin(O), and input rules of the form t ! B, where t 2 O and B is a finite set of -assertions, and – C is a set of finite sets of -patterns, called clashes.
Given an expansion rule R : (B0; N ) ! fB1; : : : ; Bmg, the variable y is a fresh variable in R if it occurs in one of the sets B1; : : : ; Bm but not in B0.
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 = f ;
( ; O)g 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.
Definition 4. An input rule t ! B is applicable to an S-state (A; O) if t 2 O and B 6 A. An expansion rule R : (B0; N ) ! fB1; : : : ; Bmg is applicable to an S-state (A; O) with substitution on var(B0) if (i) N O, (ii) B0 A, and (iii) for every 1 i m and every substitution 0 on var(B0 [ Bi) extending we have Bi 0 6 A.
Given a set of S-states M, application of an input rule R to S = (A; O) 2 M yields the set M0 = (MnfSg)[f(A[B; O)g; application of an expansion rule R to S = (A; O) 2 M with yields M0 = (M n fSg) [ f(A [ Bi ; O) j 1 i mg, where is a substitution that extends and maps the fresh variables of R to distinct new constants. If M0 is obtained from M by a rule application, we write M !S M0. M is saturated if there is no M0 with M !S M0.
The S-state (A; O) contains a clash if there is a C 2 C and a substitution on var(C) with C A. M is full of clashes if every S 2 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 fD; :Dg, 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:
R9 : (f9r:C(x)g; ;) ! ffr(x; y); C(y)gg;
Rt : (fC t D(x)g; ;) ! ffC(x)g; fD(x)gg: It also has input rules, for dealing with the ABox axioms used. For example, for concept assertions, we use
Ra : C(a) ! fC(a)g; 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 M0 = f(;; O)g eventually reaches a saturated set of S-states M (i.e. it terminates) and it holds that O 2 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 conditions—
like e.g. subset blocking [
A blocking condition is simply a set of finite sets of -assertions and patterns, using only the variables from var(B0). 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 2= 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 a1; : : : ; an and roles r1; : : : ; rn such that ri(ai; ai + 1) for all i; 1 i < n, ri(an; x), and fC j C(x) 2 Bg fC j C(a1) 2 Bg.
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. 4
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 ` 2 L, then we say that an assertion a is `-insertable into A if either (i) a 2= A or (ii) a 2 A but ` > lab(a). Given a set B of (unlabeled) assertions and a set A of labeled assertions, the set of `-insertable elements of B into A is
ins`(B; A) := fb 2 B j b is `-insertable into Ag: The `-insertion of these elements into A yields the set of labeled assertions A d` B := A [ ins`(B; A), where each assertion a 2 A n ins`(B; A) keeps its old label lab(a), each assertion in ins`(B; A) n A is labeled with `, and the label of each assertion b 2 A \ ins`(B; A) is updated to `.
Definition 5. The input rule t ! B is labeled applicable to a labeled S-state S = (A; O) if t 2 O and inslab(t)(B; A) 6= ;. An expansion rule of the form R : (B0; N ) ! fB1; : : : ; Bmg is labeled applicable to a labeled S-state (A; O) with substitution on var(B0) if (i) N O, (ii) B0 A, and (iii) for every 1 i m and every substitution 0 on var(B0 [ Bi) extending we have ins`(Bi 0; A) 6= ;, where ` := minflab( ) j = b ; b 2 B0 or = s; s 2 N g. We call this ` the degree of the rule application.
Given a set of labeled S-states M, the labeled application of the input rule R to S = (A; O) 2 M yields the set M0 = (M n fSg) [ f(A dlab(t) B; O)g; labeled application of the expansion rule R to S = (A; O) 2 M with yields the new set M0 = (M n fSg) [ f(A d` Bi ; O) j 1 i mg, 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 M0 is obtained from M by a labeled rule application, we write M !Slab M0. M is labeled saturated if there is no M0 with M !Slab M0. ( ; O)g !Slab M such
Consider a finite chain of labeled rule applications f ; 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 A0 is called a clash set in a labeled S-state S = (A; O) if there is a clash C 2 C and a substitution on var(C) with A0 = C . The label of this clash set is `A0 = minflab(a) j a 2 A0g.
Given a set of labeled S-states M = fS1; : : : ; Sng, the clash degree induced by M is `M := minfmaxf`A0 j A0 is a clash set in Sig j 1 i ng
It can be shown, using similar techniques to the ones developed in [
Theorem 7. Let P be a c-property on O and S a correct tableau for P. For every ontology O 2 Pfin(O) the following holds: for every finite chain of rule applications f(;; O)g !Slab M with M labeled saturated, the clash degree `M induced by M is a (O; P)-boundary. 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 [
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 !Sord M0 if M0 is obtained from M by an ordered rule application. M is ordered saturated if there is no M0 with M !Sord M0. 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. Lemma 9. Let M0 !Sord M1 !Sord M2. If M2 is obtained by applying a rule with degree ` to M1, and M1 is obtained by applying a rule with degree `0 to M0, then ` `0.
Proof. M1 differs from M0 by having some S-states S1; : : : ; Sm that modify the assertional component of a S-state S 2 M0 in the following way: some new assertions labeled with `0 are added, and some existing assertions get their label increased to `0. In any case, all assertions appearing in some S-state of M1 with label greater than `0 are also in an S-state of M0. If ` > `0, then all the assertions and axioms used to execute the rule M1 !Sord M2 have a label strictly greater than `0, and hence this rule was applicable also to an S-state in M0. But ` > `0 implies that `0 would not be applied, since it violates the prioritization ordering. hence ` `0. tu
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 S( ; O)g a rule is ordered applicable iff it states reachable from the initial set f ; 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 2 Pfin(O). For every set of labeled S-states M, it holds that f(;; O)g !Sord M iff f(;; O `)g !S M, 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; M0 be sets of S-states such that M is full of clashes and f(;; O)g !Sord M !Sord M0. Then `M = `M0 . 4.2
Dealing with Blocking
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 [
To solve this problem, a modification of the blocking condition that also takes
into account the labels was proposed in [
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 2= 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 2 Pfin(O) the following holds: – the ordered extension of S terminates on O; that is, there is no infinite chain of rule applications f(;; O)g !Sord M1 !Sord M2 !Sord : : :; – for every chain of rule applications f(;; O)g !Sord 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.
3 http://code.google.com/p/factplusplus/ 4 http://lat.inf.tu-dresden.de/systems/cel/