=Paper=
{{Paper
|id=None
|storemode=property
|title=Adding Context to Tableaux for DLs
|pdfUrl=https://ceur-ws.org/Vol-846/paper_30.pdf
|volume=Vol-846
|dblpUrl=https://dblp.org/rec/conf/dlog/FuP12
}}
==Adding Context to Tableaux for DLs==
https://ceur-ws.org/Vol-846/paper_30.pdf
Adding Context to Tableaux for DLs
Weili Fu and Rafael Peñaloza
Theoretical Computer Science,
TU Dresden, Germany
weili.fu77@googlemail.com, penaloza@tcs.inf.tu-dresden.de
Abstract. 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 pro-
vided. 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.
1 Introduction
Several non-standard reasoning tasks for DL ontologies can be described as re-
peated 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 per-
formed 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 con-
sequence. An obvious way to solve this task is to test each of the potentially
exponentially many sub-ontologies for the consequence, and classify them ac-
cording 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 [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, glass-
box extensions are not even guaranteed to terminate.
In this paper we focus on a special case in which the contexts are linearly or-
dered. 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 possibilis-
tic reasoning [13,11], trust management, or granularity reasoning. We develop a
glass-box approach for extending tableau-based decision algorithms into proce-
dures 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 prob-
lems 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 Basic Definitions
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 Pf in (O) denote the set of all
finite subsets of O. A consequence property (c-property) is a set P ⊆ Pf in (O)
such that O ∈ P implies O0 ∈ 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 : ¬∃r.B(a) ax2 : (¬A u B)(b) ax3 : ∀r.A(a) ax4 : r(a, b) (1)
then Oexa ∈ Pexa ; that is, Oexa is inconsistent. In general, we will call the sets
O ∈ Pf in (O) ontologies.
For several applications, axioms cannot be considered to have all equal im-
portance, 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 on-
tology. Depending on the specific application at hand, these contexts can have
different meanings, such as access rights, level of expertise, trustworthiness, ne-
cessity 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
O≥` := {t ∈ O | lab(t) ≥ `}.
Clearly, if ` ≤ `0 , then O≥`0 ⊆ O≥` . Conversely, every ontology O defines an
element λO ∈ L (called the label of O), given by λO := min{lab(t) | t ∈ O}. 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 ν ∈ L
is called a (O, P)-boundary if for every element ` ∈ L the following holds:
`≤ν iff O≥` ∈ 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 sub-
ontology O≥`2 = {¬A u 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 Pexa .
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) sub-
ontology O0 ⊆ O that still belongs to P is called a MinA for O, P.1 If O1 , . . . , Om
are all the MinAs for O, P, then
ν = max{λOi | 1 ≤ i ≤ m} (2)
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 {ax1 , ax2 , ax4 } and {ax2 , ax3 , ax4 } are the MinAs for Oexa , Pexa . The second
1
These minimal sub-ontologies are also called justifications [9].
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 [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.
3 General Tableaux
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 (a1 , . . . , an )
where P ∈ Σ is an n-ary predicate and a1 , . . . , an ∈ D. Similarly, a Σ-pattern
is of the form P (x1 , . . . , xn ) where P ∈ Σ and x1 , . . . , xn ∈ 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 ∈ Pf in (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 ∈ 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 ) → {B1 , . . . , Bm }, where
B0 , . . . , Bm are finite sets of Σ-patterns and N ∈ Pf in (O), and input rules
of the form t → B, where t ∈ 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 ) → {B1 , . . . , Bm }, 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 = {(∅, 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.
Definition 4. An input rule t → B is applicable to an S-state (A, O) if t ∈ O
and B 6⊆ A. An expansion rule R : (B0 , N ) → {B1 , . . . , Bm } 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) ∈ M
yields the set M0 = (M\{S})∪{(A∪B, O)}; application of an expansion rule R
to S = (A, O) ∈ M with ρ yields M0 = (M \ {S}) ∪ {(A ∪ Bi σ, O) | 1 ≤ i ≤ m},
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 ∈ 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:
R∃ : ({∃r.C(x)}, ∅) → {{r(x, y), C(y)}},
Rt : ({C t D(x)}, ∅) → {{C(x)}, {D(x)}}.
It also has input rules, for dealing with the ABox axioms used. For example, for
concept assertions, we use
Ra : C(a) → {C(a)},
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 = {(∅, 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, block-
ing 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 [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(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 ∈/ Bρ. The notions of saturated sets of S-
states 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
{C | C(x) ∈ B} ⊆ {C | C(a1 ) ∈ B}.
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 Boundary Extensions of General Tableaux
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 B into A is
ins` (B, A) := {b ∈ B | b is `-insertable into A}.
The `-insertion of these elements into A yields the set of labeled assertions
A d` B := A ∪ ins` (B, A), where each assertion a ∈ A \ ins` (B, A) keeps its
old label lab(a), each assertion in ins` (B, A) \ A is labeled with `, and the label
of each assertion b ∈ 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 ∈ O and inslab(t) (B, A) 6= ∅. An expansion rule of the form
R : (B0 , N ) → {B1 , . . . , Bm } 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 ` := min{lab(α) | α = bρ, b ∈ B0 or α = s, s ∈ N }. 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) ∈ M yields the set M0 = (M \ {S}) ∪ {(A dlab(t) B, O)}; labeled
application of the expansion rule R to S = (A, O) ∈ M with ρ yields the new set
M0 = (M \ {S}) ∪ {(A d` Bi σ, O) | 1 ≤ i ≤ m}, 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 →S lab M0 . M is labeled saturated if there
is no M0 with M →S lab M0 .
∗
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 A0 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 A0 = Cρ.
The label of this clash set is `A0 = min{lab(a) | a ∈ A0 }.
Given a set of labeled S-states M = {S1 , . . . , Sn }, the clash degree induced
by M is `M := min{max{`A0 | A0 is a clash set in Si } | 1 ≤ i ≤ n}
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.
Theorem 7. Let P be a c-property on O and S a correct tableau for P. For
every ontology O ∈ Pf in (O) the following holds:
∗
→S lab M with M la-
for every finite chain of rule applications {(∅, O)} −
beled 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 correct-
ness 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 optimiza-
tions based on the choice of an ordering that leads to shorter chains of rule
applications.
Unfortunately, this general approach for extending tableaux into boundary-
computation 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.
4.1 Prioritized Rule Applications
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 M0 if M0 is obtained from M by an ordered rule appli-
cation. M is ordered saturated if there is no M0 with M →S ord 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 →S ord M1 →S ord 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 ∈ 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 →S ord 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 . t
u
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-
states 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 ∈ Pf in (O). For every set of
labeled S-states M, it holds that
∗ ∗
{(∅, O)} −
→S ord M iff {(∅, O≥` )} −
→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
∗ ∗
→S ord M0 . Then `M = `M0 .
→S ord M −
{(∅, O)} −
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 [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 ex-
tension. 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 condi-
tion. 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 block-
ing) for P. For every ontology O ∈ Pf 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 M1 →S ord M2 →S ord . . .;
∗
– for every chain of rule applications {(∅, O)} −→S ord M with M labeled satu-
rated, the clash degree `M induced by M is a (O, P)-boundary.
5 Conclusions
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 exist-
ing 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 S-
states 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 exe-
cution. Since several DL reasoners now implement incremental reasoning (e.g.
Pellet,2 FaCT++,3 or CEL4 ), we believe that an implementation of our glass-
box approach for reasoning in DLs with linearly ordered contexts will be a simple
step.
References
1. Baader, F., Buchheit, M., Hollunder, B.: Cardinality restrictions on concepts. Ar-
tificial Intelligence 88(1–2), 195–213 (1996)
2. Baader, F., Knechtel, M., Peñaloza, R.: Context-dependent views to axioms and
consequences of semantic web ontologies. Journal of Web Semantics 12–13, 22–40
(April 2012), available at http://dx.doi.org/10.1016/j.websem.2011.11.006
2
http://clarkparsia.com/pellet/
3
http://code.google.com/p/factplusplus/
4
http://lat.inf.tu-dresden.de/systems/cel/
3. Baader, F., Peñaloza, R.: Automata-based axiom pinpointing. Journal of Auto-
mated Reasoning 45(2), 91–129 (August 2010), special Issue: Selected Papers from
IJCAR 2008
4. Baader, F., Peñaloza, R.: Axiom pinpointing in general tableaux. Journal of Logic
and Computation 20(1), 5–34 (February 2010), special Issue: Tableaux and Ana-
lytic Proof Methods
5. Baader, F., Peñaloza, R., Suntisrivaraporn, B.: Pinpointing in the description logic
EL+ . In: Hertzberg, J., Beetz, M., Englert, R. (eds.) Proceedings of the 30th Ger-
man Annual Conference on Artificial Intelligence (KI’07). Lecture Notes in Ar-
tificial Intelligence, vol. 4667, pp. 52–67. Springer-Verlag, Osnabrück, Germany
(2007)
6. Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge Uni-
versity Press, 2 edn. (2002)
7. Horrocks, I., Sattler, U.: A description logic with transitive and inverse roles and
role hierarchies. Journal of Logic and Computation 9(3), 385–410 (1999)
8. Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for very expressive descrip-
tion logics. Journal of the Interest Group in Pure and Applied Logic 8(3), 239–264
(2000)
9. Kalyanpur, A., Parsia, B., Horridge, M., Sirin, E.: Finding all justifications of
OWL DL entailments. In: Aberer, K., Choi, K.S., Noy, N.F., Allemang, D., Lee,
K.I., Nixon, L.J.B., Golbeck, J., Mika, P., Maynard, D., Mizoguchi, R., Schreiber,
G., Cudré-Mauroux, P. (eds.) Proc. of the 6th Int. Semantic Web Conf. and 2nd
Asian Semantic Web Conf. (ISWC’07,ASWC’07). LNCS, vol. 4825, pp. 267–280.
Springer-Verlag, Busan, Korea (2007)
10. Lee, K., Meyer, T., Pan, J.Z.: Computing maximally satisfiable terminologies for
the description logic ALC with GCIs. In: Parsia, B., Sattler, U., Toman, D. (eds.)
Proc. of the 2006 Description Logic Workshop (DL’06). Lake District, UK (2006)
11. Lesot, M.J., Couchariere, O., Bouchon-Meunier, B., Rogier, J.L.: Inconsistency
degree computation for possibilistic description logic: An extension of the tableau
algorithm. In: Proceedings of the Annual Meeting of the North American Fuzzy
Information Processing Society (NAFIPS 2008). pp. 1–6. IEEE Computer Society
Press (2008)
12. Parsia, B., Sirin, E., Kalyanpur, A.: Debugging OWL ontologies. In: Ellis, A.,
Hagino, T. (eds.) Proc. of the 14th Int. Conf. on World Wide Web (WWW’05).
pp. 633–640. ACM (2005)
13. Qi, G., Pan, J.Z.: A tableau algorithm for possibilistic description logic. In:
Domingue, J., Anutariya, C. (eds.) Proceedings of the 3rd Asian Semantic Web
Conference (ASWC 2008). Lecture Notes in Computer Science, vol. 5367, pp. 61–
75. Springer-Verlag (2008)
14. Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of de-
scription logic terminologies. In: Gottlob, G., Walsh, T. (eds.) Proc. of the 18th Int.
Joint Conf. on Artificial Intelligence (IJCAI’03). pp. 355–362. Morgan Kaufmann,
Los Altos, Acapulco, Mexico (2003)