The paper presents a tableau calculus with several re nements for reasoning in the description logic SHOI. The calculus uses non-standard rules for dealing with TBox statements. Whereas in existing tableau approaches a xed rule is used for dealing with TBox statements, the tableau calculus uses a dynamically generated set of rened rules. This approach has become practical because reasoners with exible sets of rules can be generated with the tableau prover generation prototype MetTeL. We also de ne and investigate variations of the unrestricted blocking mechanism in which equality reasoning is realised by ordered rewriting and the application of the blocking rule is controlled by excluding its application to a xed, nite set of individual terms. Reasoning with the unique name assumption and excluding ABox individuals from the application of blocking can be seen as two separate instances of the latter. Experiments show the re nements lead to fewer rule applications and improved performance.
There exist various tableau algorithms for reasoning in description logics [
Di erent blocking mechanisms have been developed for description logic
tableau algorithms. A common point of these mechanisms is that they
essentially exploit kinds of the tree model property. They compare maximally
expanded label sets of concept expressions through the construction of tree-like
models. These blocking techniques provide strong termination results but some
care is needed to ensure soundness. For more expressive logics, for example, logics
with role inverse and nominals, back-and-forth traversal of a tree model is
required with implicit backtracking together with forms of dynamic blocking [
The paper is based on [
Long versions of the paper are [
Syntax and semantics of SHOI
The description logic SHOI [
A knowledge base consists of an ABox A, a TBox T and an RBox R. A nite number of concept assertions of the form a : C and role assertions of the form (a; b) : R constitute the ABox. The hierarchy between concepts are expressed in the TBox using a nite set of inclusion statements of the form C v D. The RBox is a nite set of transitivity statements Trans(r) for some atomic roles r and inclusion statements of the form R v T which are used to express the hierarchy between roles. Normalisation of the RBox is not assumed.
We de ne the closure R+ of role inclusions in the RBox R as the smallest RBox that contains R and satis es the following two properties: (i) if Q v R 2 R+ then Q v R 2 R+; (ii) if Q v R; R v T 2 R+ then Q v T 2 R+. Given an RBox R, let R + [ fR v R j R is a roleg.
An SHOI-modeldeIniostae ttuhpelReBIo=dxef (R I ; I ), where I is a non-empty domain of interpretation and I is an interpretation function which maps individuals to elements of I , concept names to subsets of I , and role names to binary relations over I . The interpretation function extends inductively to all concept and role expressions as follows.
a I =def faI g f 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
For any expression or statement E, E is true (valid) in the model I is denoted by I j= E and is de ned as follows:
I j= C (d)ef CI =
def I j= R v T () RI
def I j= C v D () CI
I T I DI
I j= a : C (d)ef aI 2 CI
def I j= (a; b) : R () (aI ; bI ) 2 RI
I j= Trans(r) (d)ef rI is transitive.
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 true in I. That is, C is satis able with respect to (A; T ; R) in I i CI 6= ? provided that I j= E for every E 2 A [ T [ R.
The termination result in the next section for a tableau calculus for SHOI relies on the nite model property of the logic.
Theorem 1 (Finite model property of SHOI [
E =def s : C j (s; t) : R j s t
We extend the interpretation of SHOI to the tableau language as follows. For every SHOI interpretation I, let the interpretation f I in I of the function f be an arbitrary function mapping triples (s; R; C) with s 2 I , R ( I )2, C I to elements of I . The semantics of tableau formulae is speci ed by: (f (a; R; C))I =def f I (aI ; RI ; CI );
I j= s
def t () sI = tI ;
I j= s : C I j= (s; t) : R
def () sI 2 CI ;
def () (sI ; tI ) 2 RI :
Since the interpretations of the formulae s t, s : ftg and t : fsg coincide, we refer to them as equalities, and to 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 to be tested for satis ability with respect to a knowledge base (A; T ; R), the root node of the tableau is the set fa : Cg [ A, where a denotes a fresh individual and A is the ABox. 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=?.
A rule is applicable, if the premises of the rule match formulae of one of the leaf nodes. If the rule is applied to a leaf node, then the tableau is extended, by attaching to the leaf node, n child nodes annotated with the formulae of the leaf node together with appropriate instantiations of the conclusions of the rule. In order to avoid redundancies we stipulate that a rule application is redundant if an annotation of one of the child nodes is contained in the leaf node annotation.
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(A; T ; R; C) a fully expanded tableau constructed in the calculus Tab for the input concept C (to be tested for satis ability) and the knowledge base (A; T ; R).
In this paper, equality reasoning for individuals is done by means of ordered rewriting for e ciency reasons. If an equality formula s t is derived in a node, it triggers a rewriting of the current node with respect to the equalities of the node and a xed reduction ordering.
Our tableau calculus TabSHOI for the description logic SHOI is given in Figure 1. It is not di cult to see that each rule of TabSHOI preserves satis ability. Consequently we can state: Theorem 2 (Soundness). The tableau calculus TabSHOI is sound for SHOI. That is, if a concept C is satis able with respect to the knowledge base (A; T ; R) then any fully expanded TabSHOI -tableau for (A; T ; R; C) has an open branch. (?): s : :C; s : C ?
s : 9R:C (9): f (s; R; C) : C; (s; f (s; R; C)) : R (:9): s : :9Tt:C::;C(s; t) : R (R v T 2 R ) (:9 ): s : :9T t ::C:;C(t; s) : R (R v T 2 R ) (tr): s : :9tT: ::C9;R(s:C;t) : R (R v T 2 R , Trans(R) 2 R) (tr ): s : :9tT: ::9CR; (t:C;s) : R (R v T 2 R , Trans(R) 2 R) (RBox): ((ss;; tt)) :: RT (R v T 2 R+) (TBox): s : (s::Cfstg D) (C v D 2 T ) s : ::C (::): s : C
s : C t D (t): s : C j s : D
s : :(C t D) (:t): s : :C; s : :D
(s; t) : R ( ): (t; s) : R
s : C (id1): s : fsg s : :ftg (id2): t : ftg
(s; t) : R (id3): s : fsg; t : ftg ( ): ss: fttg (s 6= t)
A tableau calculus Tab is complete i for every knowledge base (A; T ; R) and every concept C if C is unsatis able with respect to (A; T ; R) then there is a closed tableau Tab(A; T ; R; C).
Theorem 3 (Completeness). TabSHOI is a complete tableau calculus for the description logic SHOI.
A form of blocking or loop-checking is necessary in order to ensure
termination. We achieve termination by incorporating a variation of the unrestricted
blocking mechanism described in [
(ub): ss : ftsjg;s t: ::ffttgg (s 6= t): Termination condition: 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) rule have been performed.
The (ub) rule is applicable to any pair of distinct individual terms that are used as labels in the current leaf node. When it is applied, two tableau successor nodes are created. In the left node, s t acts as a trigger which induces rewriting modulo derived equalities. In the right branch, the leaf node is a copy of the current leaf node extended with the additional formula s : :ftg, which indicates that s and t are not equal.
Let TabSHOI (ub) be the calculus consisting of all the rules of TabSHOI and the (ub) rule. Since, the (ub) rule is sound, and TabSHOI is sound and complete (Theorem 3), we get: Theorem 4. TabSHOI (ub) is a sound and complete for SHOI.
Based on [
Theorem 5 (Termination). Any fair procedure based on the tableau calculus TabSHOI (ub) is terminating for satis ability in SHOI.
As branch selection fairness is particularly important, this provides a weak termination result and means that in an implementation breadth- rst search or more e cient depth- rst iterative deepening search guarantees termination. Mainstream description logic tableau algorithms with less eager blocking conditions are strongly terminating. We also expect to be able to show strong termination for algorithms based on TabSHOI (ub).
Theorem 6 (Decidability). Any fair procedure based on the tableau calculus TabSHOI (ub) and satisfying the termination condition is a decision procedure for SHOI and its sublogics. 4
The (ub) rule may potentially create a large number of branching points in the derivation, as it is applicable to all pairs of individual terms in the branch. The situation is worse if the knowledge base contains a large number of individuals and 9-expressions. It is thus important to nd ways of controlling the application of blocking without loosing termination. We may reduce the number of applications of the (ub) rule, and reduce the search space by imposing appropriate side conditions on the application of the blocking rule. Ideal are side-conditions, and additional premises, that maximise the chance of constructing a nite model without the need for backtracking. It is however not possible to know which identi cation of individual terms will be helpful for discovering a nite model quickly. It is clear that systematic approaches for selecting individual terms to identify are needed, and di erent approaches display di erent performances.
The following theorem holds for arbitrary restrictions of the (ub) rule. Theorem 7 (Soundness and completeness). The (ub) rule constrained by any additional premises or side-conditions is sound. TabSHOI extended with such a constrained rule is thus sound and complete for SHOI.
In this section we introduce a general technique for controlling the application of the (ub) rule. One possible way of controlling the (ub) rule is to nd individual terms whose identi cation is known not to be essential for termination. It could also be that the domain of application dictates that certain individuals cannot be equal. For example, a subset of the ABox individuals may be assumed to be uniquely named.
Let us assume it is possible to specify a nite set S of individual terms which we want to exclude from blocking or know their blocking is not essential. Consider the following variation of the (ub) rule.
(ubnoS): ss : ftsgj;s t: ::ffttgg (t 62 S; s 6= t) In particular, it is not applied to pairs of terms appearing in the set S.
Let TabSHOI (ubnoS) be the calculus consisting of all the rules of TabSHOI and the (ubnoS) rule.
Theorem 8. Let S be a nite set of individual terms. Then TabSHOI (ubnoS) is sound, complete and terminating for SHOI.
Replacing the (ub) rule with the (ubnoS) rule, the calculus remains sound
and complete, since the (ubnoS) rule is a sound rule. However, preservation of
termination needs to be formally proved. This can be done by showing that there
exists a nite open branch for any satis able concept C when constructing the
complete tableau using TabSHOI (ubnoS). Since the existence of an open branch is
ensured by soundness, we just need to show there is a nite open branch. This can
be shown by constructing a nite, fully expanded and open branch, with the use
of a model branch built for the given concept using TabSHOI (ub). Guided by the
model branch, a nite fully expanded branch for the same concept is constructed
by TabSHOI (ubnoS). During the construction, an association function is used to
limit the possible selection of branches to the ones that mimic the model branch.
The association function is formed using the instances of blocking rule which are
no longer applicable. The complete proof of a generic variant of this theorem for
arbitrary description logic is presented in [
Di erent variations of the (ubnoS) rule can be introduced based on how S is chosen. Possible criteria for choosing members of S are syntactic criteria, for example, individual terms that are not used as labels for any 9-expressions.
Also, the (ubnoS) rule can be used for reasoning modulo an implicit unique name assumption for a nite subset of the individual terms. This is expected to be more e cient than adding explicit inequality assertions to the input set to ensure the unique name assumption, which may cause a drop in performance by increasing the overhead for premise selection. Let Si be a nite set of individual terms which are assumed to be uniquely named. For each set Si, an instance of the (ubnoS) rule should be introduced. An ontology which contains national identi cation numbers of people as well as student identi cation numbers, is a good example for this case. None of the national identi cation numbers (represented by individuals) should be identi able, equally no student identi cation numbers should refer to the same person. But a national identi cation number and a student identi cation number can refer to the same person.
In our setting, ABox individuals are not excluded from being blocked as in
many description logic tableau systems and the blocking rule is applicable to
the pairs of ABox individuals. So, we may form a set S using all the ABox
individuals. Then, similar to [
(ubnoABox): ss : ftsjg;s t: ::ffttgg (t is not an ABox individual , s 6= t) 5
In this section we re ne the calculus TabSHOI presented in Section 3. The idea of the re nement is that the (TBox) rule is replaced by dynamically generated and re ned tableau rules. In the rst step, all the atomic concepts in the TBox T are equi-satis ably replaced by constant concepts and the parametric (TBox) rule is represented as a set of tableau rules for each C v D 2 T . The bene t of this replacement of the (TBox) rule by a set of rules is the possibility of re ning the rules. This allows to reduce the branching factor of the rules, while preserving soundness and completeness.
In the second step, we apply the atomic rule re nement introduced in [
s : fsg is re ned to s : A; s : B : s : :A j s : :B j s : C s : C
We apply the atomic rule re nement to all rules obtained from TBox statements. Consequently there are fewer branches in the conclusion and additional premises are added that limit application of the rules. (Similar re nements on instances of the (RBox) rule are possible for more expressive logics with negated role assertions.)
Let Tabdyn;T (ub) denote the calculus which consists of the re ned generated
SHOI
tableau rules from the TBox T and all rules of TabSHOI except the (TBox) rule.
That is, for each statement C v D 2 T a corresponding tableau rule is generated
and re ned according to the atomic rule re nement. Soundness and completeness
of Tabdyn;T (ub) is a direct consequence of the results in [
SHOI Theorem 9. Tabdyn;T (ub) is a sound, complete and terminating tableau cal
SHOI culus for reasoning in SHOI with respect to a knowledge base (A; T ; R) with a xed TBox T . 6
In order to compare the performance of provers based on the calculi TabSHOI (ub) and Tabdyn;T (ub), an experiment has been designed. MetTeL version 2.0-487
SHOI was used to generate provers based on TabSHOI (ub) and Tabdyn;T (ub) for variSHOI ous ontologies. MetTeL generates Java code for a tableau prover from the speci cation of the syntax of a logic and the speci cation of tableau calculus. By default, the tableau provers generated with MetTeL use a depth- rst left to right search strategy. While specifying the speci cation of tableau calculus, appropriate rule priorities were assigned to ensure fairness of the expansion strategy and hence guarantee termination. The generated provers were used with no modication in this experiment.
In order to embrace an extensive range of problems with varying input sizes
and expressivity, the experiment used the TONES ontology repository [
SHOI the remaining ontology axioms were translated so that the prover generated using the speci cation of Tabdyn;T (ub) could check its consistency. Inputs prepared for
SHOI both provers were then used with a log le from Fact++ to produce additional problem sets. Fact++ produces a log le which contains the class hierarchy of the ontology. For a randomly picked subsumption relation C v D in the hierarchy and a fresh individual s, s : C and s : D were added to the input le to form an additional satis able input and respectively s : C and s : :D to form an additional unsatis able input. This experiment was aimed at evaluating the e ect on reasoning performance when using Tabdyn;T (ub) in comparison to SHOI TabSHOI (ub). This means we checked the consistency of the input and omitted checking satis ability of all concepts and calculating concept hierarchies.
The developed translator successfully translated 628 ontologies and each prover was executed on 2480 inputs with a timeout of 100 seconds. The comparison was done by measuring the execution time of the prover. The results of this comparison are presented in Table 1. For the set of results with timeout, when a prover did not return any answer within 100 seconds, 100 seconds were used in the calculation of the average time. While for the set of results without timeout, if one of the provers under comparison required more than 100 seconds, that input is not included in the results. The results show that the generated provers based on the re ned tableau calculus were faster for unsatis able inputs. Inspection showed this was mainly a consequence of having additional closure rules. These closure rules were re nements of dynamically generated rules from TBox statements where all the conclusions are turned into premises in a rule. A signicant drop in memory use was exhibited when using Tabdyn;T (ub) compared to SHOI TabSHOI (ub) specially for unsatis able inputs. As expected, the performance of the system was not comparable with Fact++.
Moreover, an experiment to compare the performance of TabSHOI (ub) and TabSHOI (ubnoABox), using the same inputs as before, was designed. Since it is not yet possible to express rules such as the (ubnoS) rule in the MetTeL tableau rule language, we generated a prover for the tableau calculus TabSHOI without any blocking mechanism. Then, code implementing the (ubnoABox) rule was manually added to the generated Java code. In order to have a fair comparison, the prover for the (ub) rule was also created by manually adding code implementing the (ub) rule. The results of the comparison are presented in Table 2.
The experimental results show there is not a big di erence between the performance of the provers based on TabSHOI (ub) and TabSHOI (ubnoABox). This is mainly caused by the small number of ABox individuals in a large number of ontologies in the test set. 7
A re ned version of the tableau calculus in [
A comparison was done between the provers generated using the tableau calculus with dynamically generated tableau rules, and a prover with xed rules for dealing with TBox and RBox statements. The results show the former is more optimised for unsatis able inputs. The analysis of the reduction in the branching points and complexity is left as future work.
Other future plans include studying the relationship between properties of a logic and its required minimal blocking criteria. That is, expressing side conditions that can be used to control the unrestricted blocking rule to be applied as little as possible. This should be done without endangering termination.