This paper presents an abstract tableau calculus for the description logic SHOI. SHOI is the extension of ALC with singleton concepts, role inverse, transitive roles and role inclusion axioms. The presented tableau calculus is inspired by a recently introduced tableau synthesis framework. Termination is achieved by a variation of the unrestricted blocking mechanism that immediately rewrites terms with respect to the conjectured equalities. This approach leads to reduced search space for decision procedures based on the calculus. We also discuss restrictions of the application of the blocking rule by means of additional side conditions and/or additional premises.
Since the late nineteen eighties various tableau algorithms have been developed
for description logics [
In [
Being based on a sound tableau rule and equality reasoning, the unrestricted
blocking mechanism is generally sound and can be incorporated into sound and
complete labelled tableau calculi or related approaches. We have shown that if
the logic has the nite model property then adding the unrestricted blocking
mechanism guarantees also termination [
The aim of this paper is to formalise reasoning for a well-studied, expressive description logic in an abstract labelled tableau calculus incorporating unrestricted blocking. We also we want to explore the possibilities of emulating di erent kinds of existing blocking techniques. In particular, we present an abstract labelled tableau calculus for the description logic SHOI. The tableau calculus is in line with a re ned tableau calculus obtained in the tableau synthesis framework, but exploiting the tree model property of SHOI, transitive roles are accommodated via a propagation rule rather than a structural rule.
Di erent to most labelled tableau approaches the expansion of 9 expressions
introduces Skolem terms rather than constants. Another novelty is the use of
ordered rewriting to realise equality reasoning for singleton concepts (nominals)
and blocking. Though there are similarities with substitution and nominal
deletion approaches (e.g., [
The paper is structured as follows. The syntax and semantics of SHOI are de ned in Section 2. In Section 3 we de ne the tableau calculus for SHOI and in Section 4 we prove that it is sound, complete and terminating. Furthermore, we present examples of restricting the blocking rule by imposing constraints via additional premises and/or side conditions in Section 4. Due to space restrictions we do not discuss the emulation of all known existing blocking techniques but the examples given illustrate the general idea.
SHOI extends the description logic ALC with singleton concepts, role inverse, transitive roles and role inclusion axioms. The language of SHOI is de ned over disjoint countable sets of concept names (atomic concepts), individuals, and role names (atomic roles). The symbol A is used to denote an atomic concept, the symbols a and b denote individuals, and the symbol r denotes an atomic role. Concept and role expressions are built from atomic concepts, individuals, and atomic roles using connectives f g (singleton operator), :, t, and 9 : (existential restriction operator), (role inverse operator). Formally, concept and role expressions are de ned respectively by the following grammar rules, where C and D denote concept expressions and R denotes a role expression.
C; D =def A j fag j :C j C t D j 9R:C
R =def r j R The operators >, ?, u, and 8 : are de ned as usual. In order to simplify the syntax and avoid repetitive occurrences of the role inverse operator we assume that (r ) =defr. Further, in SHOI, any atomic role is allowed to be declared as transitive and the predicate Trans is used to denote this. Thus, for every atomic role r, Trans(r) is true i r is transitive.
A description logic knowledge base consists of an ABox A, a TBox T and an RBox R. The ABox consists of a nite number of concept assertions of the form a : C and role assertions of the form (a; b) : R. The TBox is used to express a hierarchy between concepts through a nite set of inclusion statements of the form C v D. A normalised TBox is a set of inclusion statements of the form > v C. The RBox is a nite set of inclusion statements of the form R v S and Trans(r), to specify a hierarchy between roles and de ne transitivity of some roles. We de ne the closure R+ of the RBox R as the smallest RBox that contains R and satis es the following properties.
{ if Q v R 2 R+ then Q v R 2 R+; { if Q v R; R v S 2 R+ then Q v S 2 R+.
Given an RBox R, let R denote the RBox R+ [ fR v R j R is a roleg.
The semantics of SHOI is de ned by an interpretation I = ( I ; I ) given by a pair of a non-empty set I , referred to as the domain of interpretation, and an interpretation function I . The function I maps individuals to elements of the domain, concept names to subsets of I and role names to binary relations over I . Regarding roles declared as being transitive, I must satisfy that rI is a transitive relation whenever Trans(r) is true. The function I extends to all concept and role expressions by induction on lengths of expressions as follows: aI =def faI g; (:C)I =def
I n CI ; (C t D)I =def CI [ DI ; (9R:C)I =def fx j 9y 2 CI (x; y) 2 RI g; (R )I =def f(x; y) j (y; x) 2 RI g:
According to the semantics, the inverse of a role is transitive i the role is transitive. Following this, we extend the predicate Trans to all role expressions so that Trans(r ) is true i Trans(r) is true.
Let E denote any concept expression, any concept inclusion, any role inclusion, any concept assertion or any role assertion. We indicate by I j= E that E is valid in the model I. We de ne:
I j= C (d)ef CI = I I j= a : C (d)ef aI 2 CI I j= R v S (d)ef RI SI I j= (a; b) : R (d)ef (aI ; bI ) 2 RI I j= C v D (d)ef CI DI
Because SHOI supports singleton concepts, every ABox statement a : C can
be encoded by the TBox statement fag v C. Also, every role assertion (a; b) : R
can be encoded as the TBox statement fag v 9R:fbg. Thus, without loss of
generality, we assume that a knowledge base is a pair (T ; R) which consists
of a normalised TBox T and an RBox R. It worth noting that the TBox can
be internalised as well [
A concept C is satis able in a model I i CI 6= ;. A concept is satis able in I with respect to a knowledge base if it is satis able in I whenever every statement of the knowledge base is valid in I. That is, C is satis able with respect to (T ; R) in I i CI 6= ; provided that I j= E for every E 2 T [ R. 3
In this section we present a labelled semantic ground tableau calculus for SHOI.
The language of the tableau calculus is an extension of the language of SHOI with equality formulae and individual terms used as labels. We add a function symbol f which takes a triple (s; R; C) consisting of an individual term s, a role expression R and a concept expression C as its arguments and de ne the set of (individual) terms s inductively by the following grammar rule, where a denotes any individual, C any concept and R any role.
s =def a j f (s; R; C) Terms which are not ABox individuals can be viewed as being Skolem terms.
Formulae in the tableau language are de ned by the following grammar rule, where s and t are individual terms, C is a concept and R is a role.
E =def s : C j (s; t) : R j s t
We extend the interpretation of SHOI expressions to the formulae of the tableau language. For every SHOI interpretation I, let the interpretation f I in I of the function f be an arbitrary function mapping triples (x; ; ) with x 2 I , ( I )2, I to elements of I . We let (f (a; R; C))I =def f I (aI ; RI ; CI );
I j= s
def t () sI = tI ;
I j= (s : C)I I j= (s; t) : R
def () sI 2 CI ;
def () (sI ; tI ) 2 RI :
The interpretations of the formulae s t, s : ftg and t : fsg coincide. In accordance with their interpretation we refer to these formulae as equalities. We also refer to the formulae of the form s : :ftg as inequalities.
Let Tab denote a tableau calculus comprising of a set of inference rules. A derivation or tableau for Tab is a nitely branching, ordered tree whose nodes are annotated by sets of tableau formulae. Assuming that C is the input concept expression to be tested for satis ability with respect a knowledge base (T ; R) the root node of the tableau is the set fa : Cg, where a denotes a fresh individual. Successor nodes are constructed in accordance with a set of inference rules in the calculus. The inference rules have the general form
X0 X1 j : : : j Xn
(side-condition); where X0 is the set of premises and the Xi are the sets of conclusions. If n = 0, the rule is called closure rule and written X0=?.
If is a substitution that acts on tableau formulae and X = fE1; : : : ; Ekg is a set of tableau formulae then X denotes the set fE1 ; : : : ; Ek g. A rule is applicable to a tableau if there is a leaf node annotated with a set N and there is a substitution such that X0 N , where X0 is the set of premises of the rule, and the side-condition of the rule is true for N . is called the matching substitution of the rule application. We assume in a rule individual symbols, concept symbols and role symbols represent variables that are matched with individual terms, concept expressions and role expressions respectively. We also say the rule is applicable to the formulae X0 in (the leaf node of) the branch.
If a rule of the calculus is applicable to a leaf node of the tableau with a matching substitution , then the tableau is extended by attaching to the leaf node n child nodes annotated with N [ Xi for i = 1; : : : n, respectively. In order to avoid redundancies we stipulate that a rule application to a leaf node annotated with N is redundant if there is a conclusion set Xi for some i = 1; : : : n of the rule such that Xi N , where is the matching substitution. This ensures rules are not applied more than once to the same sets of formulae.
A branch in the tableau is a maximal path from the root of the tableau to a leaf node. If a closure rule has been applied in a branch then the branch is said to be closed. If a branch is not closed, it is called open. A tableau is closed if all its branches are closed. A branch is fully expanded if no more rules are applicable to its leaf node modulo redundancy. We call a tableau fully expanded i all its branches are fully expanded. We denote by Tab(T ; R; C) a fully expanded tableau constructed in the calculus Tab for the input concept C and the knowledge base (T ; R).
We need equality reasoning for individual terms to achieve termination for
the calculus. Equality reasoning can be provided in various ways. One is to
supply special tableau rules for reasoning modulo equalities within the branch
in a similar way as is done in [
(R v S 2 R ) (R v S 2 R , Trans(R) 2 R)
(R v S 2 R , Trans(R) 2 R) (?): (t): s : :C; s : C s : C?t D s : C j s : D ( +):
s : 9R:C (9): f (s; R; C) : C; (s; f (s; R; C)) : R
s : :9S:C; (s; t) : R (:9): t : :C
s : :9S :C; (t; s) : R (:9 ): t : :C (+): s : :9S:C; (s; t) : R
t : :9R:C s : :9S :C; (t; s) : R (RBox): (s; tt):::R9R :C (s; t) : S (R v S 2 R+) s : ::C (::): s : C
s : :(C t D) (:t): s : :C; s : :D
(s; t) : R ( ): (t; s) : R
s : C (id): s : fsg s : :ftg (id2): t : ftg
(s; t) : R (cng): s : fsg; t : ftg
s : fsg (C 2 T ) (TBox): s : C ( ): ss: fttg (s 6= t) all individual terms in any tableau derivation are ground we are dealing with a special case of rewriting, namely, ground rewriting.
In this paper, a rewrite system R is a binary relation on the set of all individual terms and consists of rewrite rules which are pairs of individual terms. In order to handle equalities, we orient each equality formula appearing in the current branch of a tableau derivation according to a special ordering which is a strict partial order on individual terms. We denote by s ! t a rewrite rule (s; t) in which s t. Thus, if an equality formula s t appears in a node of a branch then either s ! t or t ! s is added as a rewrite rule to the rewrite system of the branch. A term which cannot be rewritten (with respect to a rewrite system) is said to be in normal form. A normal form of a term s is denoted by nf(s). A rewrite system is terminating if there is a normal form for each term.
Our tableau calculus TabSHOI for the description logic SHOI is given in Figure 1. The (?) rule is the closure rule. The (::) rule removes occurrences of double negation on concepts. The (t) and (:t) rules are standard rules for handling concept disjunctions. Given a tableau formula s : 9R:C, the (9) rule introduces an individual term f (s; R; C) as an R-successor of s (instead of introducing a fresh individual as might be done in other presentations). The (:9) rule is equivalent to the standard rule for universally restricted concept expressions. The (:9 ) rule allows the backward propagation of concept expressions along inverted links. The ( ) rule inverts a given link.
The (+) rule propagates negated existential concept restriction along a transitive link while the ( +) rule does the same for inverse occurrences of transitive roles. Equalities of the form s : fsg are tautologies, used in our calculus as domain predicates for keeping track of the terms that have been introduced to a branch. This is achieved with the three rules (id), (id2) and (cng). The (TBox) rule concatenates every concept of the normalised TBox with every label occurring on the branch. The (RBox) propagates a link of a role into its superrole according to the closure R+ of the given RBox R.
The ( ) rule is a special rule adding, what we call, a rewrite trigger s t to the branch. Let be any reduction ordering on the set of individuals in the branch. The addition of any tableau formula s t to a set N of formulae which annotates a leaf tableau node immediately triggers the following rewrite process. Suppose that s t (the case t s is symmetrical). Then, s ! t is added to a rewrite system R associated with the current tableau branch. The tableau is extended by attaching one child node to the current leaf node. The child node is annotated by the set N 0 obtained by rewriting all the tableau formulae in N with respect to the rewrite system R. In particular, this means that, in N 0 every term s is replaced by a term u such that s ! u with respect to R. 4
It is not di cult to see that each rule of TabSHOI is sound, i.e., preserves satis ability of concept assertions. Consequently: Theorem 1 (Soundness). The tableau calculus TabSHOI is sound for the description logic SHOI. That is, if a concept C is satis able with respect to the knowledge base (T ; R) then any fully expanded TabSHOI -tableau for (T ; R; C) has an open branch.
A tableau calculus Tab is complete i for every knowledge base (T ; R) and every concept C if C is unsatis able with respect to (T ; R) then there is a closed tableau Tab(T ; R; C). In order to prove completeness of TabSHOI , we prove its constructive completeness which implies completeness. A tableau calculus Tab is constructively complete if for every open branch in any fully expanded tableau Tab(T ; R; C) there is a model which validates the knowledge base (T ; R) and satis es C.
Theorem 2 (Completeness). TabSHOI is a (constructively) complete tableau calculus for the description logic SHOI.
Next, we establish termination. A tableau calculus Tab is (weakly) terminating if any tableau Tab(T ; R; C) has a nite open branch provided that C is satis able concept with respect to the knowledge base (T ; R).
Although TabSHOI is a sound and complete tableau calculus for the
description logic SHOI, it is not terminating. In order to achieve termination, a form of
blocking or loop-checking is necessary. One possibility is to add the unrestricted
blocking mechanism described in [
In this paper, we take a slightly di erent route and introduce a modi ed version of the unrestricted blocking mechanism. It is given by the (ub-rw) rule and ordered rewriting.
(ub-rw): ss : ftsjg;s t: ::ffttgg (s 6= t) Here, s t is a rewrite trigger as introduced in Section 3. Premises of this rule are instantiated with any two distinct terms s and t used as labels in a set of tableau formulae N annotating the current leaf node. As a result of a rule application two successor nodes are created. If s t (respectively t s) then in the left node a rewrite rule s ! t (respectively t ! s) is added to the rewrite system R. The left node is annotated with a copy of N , which is rewritten with respect to the newly obtained rewrite system R. The right node is annotated with a copy of N extended with the additional formula s : :ftg. This formula indicates the case that s and t are not equal.
The calculus consisting of all the rules of TabSHOI and the rule (ub-rw) is denoted by TabSHOI (ub-rw). Clearly, the (ub-rw) rule is sound. Therefore: Theorem 3. The calculus TabSHOI (ub-rw) is a sound and (constructively) complete for the description logic SHOI.
In order to ensure termination for a procedure based on TabSHOI (ub-rw)
the rule application strategy must satisfy the following condition.
(c2) In every open branch there is some node from which point onward before
any application of the (9) rule all possible applications of the (ub-rw) rule
have been performed.
(The unrestricted blocking mechanism in [
Provided that condition (c2) holds, a su cient and necessary condition for
termination of the tableau procedures based on TabSHOI (ub-rw) is that SHOI
has the nite model property with respect to its standard semantics. This can
be shown in a similar way as in [
The nite model property for SHOI can be shown by a ltration argument. Theorem 4 (Finite model property of SHOI). The description logic SHOI has the nite model property.
Therefore, using the results of [
The (ub-rw) rule creates potentially many branching points in a derivation, especially if the number individuals and 9-expressions in the knowledge base is high. A way to reduce the number of applications of the (ub-rw) rule and thus reduce the search space is to apply the blocking rule less often. This can be achieved by adding side-conditions and/or premises to the rule. Ideal would be side-conditions and additional premises that maximise the chance of constructing a nite model without the need for backtracking.
In the remaining section, we give some examples of restricted versions of the (ub-rw) rule. They all preserve soundness and completeness. We have: Theorem 6 (Soundness and completeness). The (ub-rw) rule constrained by additional premises or side-conditions is sound. Thus, TabSHOI extended with such a modi ed rule is sound and complete for SHOI.
Most existing description logic tableau algorithms aim to construct models given by relational tree structures where the nodes are individuals (or individual terms, if Skolem terms would have been used) and are annotated with label sets of concept expressions. A label set of a term s is the set L(s)=deffC j s : C 2 N g: These label sets are then used in the tests of standard blocking mechanism such as subset ancestor blocking and dynamic anywhere equality blocking.
An emulation of subset ancestor blocking can be realised through the selective application of the (ub-rw) rule, realised by adding a side-condition: (ub -rw): ss : ftsjg;s t: ::ffttgg (s 6= t, s is an ancestor of t and L(t) L(s)) In this rule the application of the (ub-rw) rule is restricted to a term s and its successor term t, where the label set of s is a superset of the label set of t. In our setting, as the calculus creates Skolem terms in the (9) rule, a term s is an ancestor of a term t, if s is a subterm of t.
Standard ancestor subset blocking is used in tableau algorithms for
description logics ALC, S and SH [
Application of the (ub-rw) rule can be limited by ignoring the pairs of terms
where the application of the rule is not critical for termination. E.g., it is
possible to ignore pairs where both terms appear before some xed node of a tableau
derivation. We believe, as there are a nite number of individuals before a xed
tableau node, excluding them does not endanger termination. In particular, the
pairs where both terms are ABox individuals can be ignored as in [
(ubNo ABox-rw): ss : ftsjg;s t: ::ffttgg (s 6= t, not both s and t are ABox individuals) We can de ne a variation of the (ub-rw) rule restricted to the terms that are known to be the ones that may cause in nite derivations. For TabSHOI , in nite derivations can be caused only by in nite applications of the (9) rule. This means we may focus blocking on the terms to which the (9) rule may eventually be applicable, i.e., the terms which have an 9-expression in their label sets. We may formulate the (ub-rw) rule as follows to re ect this restriction: (ub9-rw): s : 9R:C; t : 9S:D s t j s : :ftg (s 6= t) Here, 9R:C, 9S:D are two 9-expression that can be matched with any 9-expression. This rule is applicable to any pair of terms s and t which both have a 9-expression in their label sets.
The three variations of the (ub-rw) rule just presented are all sound, thus preserving soundness (and completeness) of the calculus is not an issue. An issue is to show under which conditions and for which logics termination can be ensured. Because of the side-conditions or additional premises these variations of the (ub-rw) rule are no longer applied to every possible pair of terms. Thus, condition (c2) does not hold. We believe however it can be proved that search strategies can be adopted where blocking applies to su ciently many pairs so that the procedure terminates.
Next we illustrate how the ( ) rule [
s : 9R:C j (s; tn) : R; tn : C j (s; f (s; R; C)) : R; f (s; R; C) : C Here, t1; : : : ; tn are all existing terms, covering all given ABox individuals and all introduced Skolem terms on the current branch. The ( ) rule is actually a modi ed version of the (9) rule. Instead of creating a new term to satisfy an 9-expression, this rule tries to satisfy the 9-expression by reusing existing terms. If all the attempts to satisfy the 9-expression with existing terms end in contradictions, then a new term f (s; R; C) is introduced.
In our abstract calculus we can simulate the ( ) rule with the (9) rule and modifying the (ub-rw) rule to:
(ub -rw): ss : ftsjg;s t: ::ffttgg (s 6= t, t is a Skolem term) We should use a rule application strategy where after each application of the (9) rule, the (ub -rw) rule is applied to the newly added Skolem term and every existing term. In contrast to the previous blocking variations, the (ub -rw) rule satis es condition (c2), since all possible term comparisons are performed before any application of the (9) rule. Hence termination is ensured.
Theorem 7 (Termination). Any implementation, fair in the sense of [