Context-sensitivity has been for long a subject of study in linguistics, logic and computer science. Recently the problem of representing and reasoning with contextual knowledge has been brought up in the research on the Semantic Web. In this paper we introduce a conservative extension to the Description Logic ALC which supports representation of ontologies containing relative terms, such as `big' or `tall', whose meaning depends on the reference to a particular comparison class (context). We specify the syntax and semantics of the language and present a sound and complete tableau decision procedure.
incoherencies simply by recognizing that certain terms, call them relative1, such
as The Biggest, acquire de nite meanings only when put in the context of
other denoting expressions | in this case, expressions denoting speci c
collections of objects, so-called comparison classes, with respect to which the relative
terms are used [
The problem of context-sensitivity has been for a long time a subject of
studies in linguistics, logic and even computer science. Recently, it has been
also encountered in the research on the Semantic Web [
In this paper we de ne a simple, conservative extension to the DL ALC, which is intended for representation of context-sensitive terminologies, where by contexts we understand speci cally comparison classes with respect to which the relative terms acquire precise meanings. In the following section we formally de ne the language, next we present a tableau calculus for deciding satis ability, and nally, in the last two sections, we shortly position our work in a broader perspective and conclude the presentation. 2
The language CALC , introduced in this section, extends the basic ALC logic with two modal-like operators, enabling construction of contextualized concept descriptions, which internalize the use of comparison classes in the language. The classes are denoted by means of arbitrary concept descriptions. Formally, the novel feature of CALC is founded on an extra modal dimension incorporated into DL interpretations, whose possible states are represented by subsets of the object domain.
In the following subsections we rst shortly recap the basic notions concerning DLs and then give a detailed account of the syntax and semantics of CALC . 2.1
A DL language is speci ed by a signature = (NI ; NC ; NR), where NI is a set
of individual names, NC a set of concept names, and NR a set of role names,
and a set of logical operators enabling construction of complex formulas [
The DL ALC sanctions concept descriptions de ned by means of concept names (atomic concepts), special symbols >; ? and the following concept constructors:
C; D; r ! :C j C u D j C t D j 9r:C j 8r:C
A knowledge base K = (T ; A) in ALC, consists of the terminological and the assertional component. A (general) TBox T contains concept inclusion axioms C v D (abbreviated to C D whenever C v D and D v C) for arbitrary concept descriptions C and D. An ABox A contains axioms of possibly two forms: concept assertions C(a) and role assertions r(a; b), where a, b are individual names, C a concept, and r a role.
The semantics is de ned in terms of an interpretation I = ( I ; I ), where I is a non-empty domain of individuals, and I is an interpretation function, which speci es the meaning of the vocabulary by mapping every a 2 NI to an element of I , every C 2 NC to a subset of I and every r 2 NR to a subset of I I . The function is inductively extended over complex terms in a usual way, according to the xed semantics of the logical operators. An interpretation I satis es an axiom in either of the following cases: { I j= C v D i { I j= C(a) i { I j= r(a; b) i
CI DI aI 2 CI
haI ; bI i 2 rI
Finally, I is said to be a model of a DL knowledge base, i.e. it makes the knowledge base true, if and only if it satis es all its axioms. 2.2
The syntax of ALC is extended in CALC with two additional concept constructors, based on modal-like operators h i and [ ]:
C; D ! hDiC j [D]C
A contextualized concept description consists of a relative concept C and a speci ed comparison class D, which co-determines the meaning of C. Intuitively, hDiC denotes all objects which are C as considered in the context of all objects which are D, whereas [D]C denotes all objects which are either not D or otherwise (like in the former case) are C as considered in the context of all objects which are D. For instance, hCityiThe Biggest describes the individuals that are the biggest as considered in the context of (all and only) cities, while [European City]:The Biggest describes all those individuals that are either not European cities, or if they are, they are not the biggest ones in that context. Other than that CALC does not di er from ALC on the syntactic level.
More interesting changes appear in the semantics of the language, which is essentially augmented with an additional modal dimension, with possible states | comparison classes | corresponding to subsets of the (global) domain of interpretation, and the accessibility relation corresponding to the -ordering of those subsets. In each state the vocabulary (of the relevant part) of the language is interpreted independently from the others. De nition 1 introduces the notion of context structure which characterizes an interpretation of a CALC language. De nition 1. A context structure for a set of languages fLwgw2W is a tuple C = hW; C; ; fIwgw2W i, where: { W }( ) is a set of comparison classes, with 2 W and ; 62 W , { C W W is an accessibility relation, s.t. w C v i v w { is a global domain of interpretation, { Iw = ( Iw ; Iw ) is an interpretation of Lw with respect to w:
Iw = w is a non-empty domain of individuals,
Iw is an interpretation function de ned as usual.
Instead of speaking of one language L, in many cases it is more convenient to refer to particular sublanguages fLwgw2W , which are based on the parts of the vocabulary of L deemed meaningful in particular contexts.2 We assume that individual names are interpreted rigidly, i.e. for every a 2 NI and every w; v 2 W , such that a belongs to the vocabulary of Lw and Lv, the context structure has to satisfy aIw = aIv . It is easy to observe that C imposes a partial order (re exive, asymmetric and transitive) on the set of contexts, with the root w^ = 2 W as its least element. Thus context structures correspond to rooted, partially ordered Kripke frames.
Given a context structure C = hW; C; ; fIwgw2W i we can now properly de ne the semantics of contextualized concept descriptions.
(hDiC)Iw = fx 2 ([D]C)Iw = fx 2
Iw j 9w C v; Iw j 8w C v;
Iv = DIw : x 2 CIv g Iv = DIw : x 2
Iv implies x 2 CIv g
As usual the operators can be de ned in terms of their dual counterparts, i.e. [D]C = :hDi:C and hDiC = :[D]:C. Furthermore, another less common relationship between the operators can also be derived, namely: [D]C = :D t hDiC and hDiC = D u [D]C.
As expected, the notion of satisfaction in CALC is relativized to context structure and a particular comparison class in that structure. A context structure C is a model of a knowledge base if and only if all the axioms in that knowledge base are satis ed at the root of C.
{ C; w^ j= C v D i { C; w^ j= C(a) i { C; w^ j= r(a; b) i
CIw^ DIw^ aIw^ 2 CIw^
haIw^ ; bIw^ i 2 rIw^
Note, that we interpret all axioms only at the roots of models. It follows that both syntactically and semantically CALC is a conservative extension of ALC, i.e. every satis able ALC knowledge base is a satis able CALC knowledge base. 2 For instance, the name Moscow is not meaningful when the focus is only on the Asian cities. Similarly, some concepts can be applicable only with respect to particular types of objects, e.g. natural numbers can be neither Hot nor :Hot.
The tableau calculus for CALC , presented in this section, is an extension of the
well-known procedures for ALC [
Apart from terms representing domain objects I = NI [ fx; y; : : :g, the calculus involves a set of context labels C = f ; ; : : :g used for marking comparison classes, where each label is a nite sequence of concept descriptions separated with a vertical line: = C1 j C2 j : : : j Cn. The empty label 2 C refers to the root of the context structure. The labels can be rendered into CALC by means of the function p : C 7! L, such that for every = C1 j : : : j Cn 1 j Cn 2 C : p( ) = hC1i : : : hCn 1iCn ; p( ) = > )u if : (C u D)(x) 2 S
then set S0 := S [ f : C(x); : D(x)g )t if : (C t D)(x) 2 S
then set S0 := S [ f : C(x)g or S0 := S [ f : D(x)g )9 if : (9r:C)(x) 2 S and x is not blocked in then set S0 := S [ f : r(x; y); : C(y)g, for a new -minimal y )8 if : (8r:C)(x) 2 S and : r(x; y) 2 S
then set S0 := S [ f : C(y)g ) if : (> C) 2 S and : (x) 2 S
then set S0 := S [ f : C(x)g )6 if : (C 6 D) 2 S then set S0 := S [ f : C(x); :D(x)g or S0 := S [ f : :C(x); D(x)g, for a a new )B if fC j for a xed : C(y) 2 Sg and y
fC j : C(x) 2 Sg x then mark y as blocked in
by x
A tableau proof for # = Vi #i, where every #i is a DL axiom, is initiated by setting a constraint system containing : #i for all i. At every stage of the procedure, the system contains only elements of the form: (1) : C(x); (2) : r(x; y); (3) : > C; (4) : C 6 D; for some 2 C , x; y 2 I and concept/role descriptions C; D; r. Note that TBox axioms can be rewritten in a usual manner into a single constraint : > d assume that all concepts descriptions are given inCvtDhe2TN:egCattioDn.NWoremmalorFeoorvmer, and that all occurrences of [D]C are replaced with the equisatis able :DthDiC.
The standard ALC inference rules are restated in Table 1. As usual we assume a well-ordering of the individual variables used in a proof for a proper application of the blocking mechanism. We always require that applications of the )9 rule are deferred until no other rules apply. We say that a system contains a clash if for some , x and A it contains both : A(x) and : :A(x). Besides )h i if : hCiD(x) 2 S
then set S0 := S [ f j C : D(x)g ) if j C : (x) 2 S
then set S0 := S [ f : C(x)g )6= if : C(x) 2 S and : :C(x) 2 S then set S0 := S [ f : p( ) 6 p( )g the ALC component, the inference engine comprises three additional rules, presented in Table 2. The meaning of the )h i rule is straightforward: it introduces a relative concept assertion within the scope of a newly generated context label, this way marking a transition of the proof into a di erent comparison class. The two remaining rules require some more comment. The ) rule accounts for the A ewnMnnnnnnnhAinnnnnnnnn QQQQQIQQQQQ
hBi IA =AI S Y ? e{hAik{{{{q{9 B fCCCCCIB =BI=
}{{{{ hBiCCCCC! B j A IBjA =AIB B j B hBt?QiQQQQQQ(
B8 t ? IBjB =BIB
IBt? =(Bt?)I
Fig. 2. A tree of context labels and the underlying context structure. fact that the accessibility relation between comparison classes has to follow their -ordering. Hence all individual terms introduced in a proof within the scope of a particular context label have to be simultaneously represented within the scope of its predecessor, and moreover they have to occur there as instances of the concept which denotes the successor comparison class. The ) rule ensures that exactly these conditions are satis ed. The )6= rule resolves synonymity between certain context labels. Observe, that the labeling generated by )h i is tree-shaped (see Figure 2), while the C ordering of the comparison classes does not have to be such in principle. In fact, di erent context labels (or rather their p-translations) might denote exactly the same comparison classes (e.g. consider operators hBi and hB t ?i in the picture). This is not a problem as long as there is no potential clash between the assertions occurring within the scope of di erent labels. In case there is such a possibility, the rule ensures that the labels indeed represent non-equivalent comparison classes.
It can be shown that the basic results of soundness, termination and
completeness hold for the calculus. Below we prove termination and sketch the proofs
of the remaining theorems. For their full versions we refer to the accompanying
technical report [
Lemma 1 (Soundness). Let S be a complete clash-free constraint system for #. Then # is satis able.
Sketch of proof. As in the typical proofs of soundness for tableau procedures for DLs, we use S as `a guide' to show that there exists a model for #. To this end we rst de ne a structure C = hW; C; ; fIwgw2W i as follows: { w 2 W for every occurring in S, where
w = Iw comprises all terms x such that : (x) 2 S { C for every and = j C occurring in S { x 2 AIw for every , x and A such that : A(x) 2 S { aIw = a for every and a 2 obj (#) such that : (a) 2 S { rIw (x; y) for every , x, y and r such that : r(x; y) 2 S (or in case x is blocked in by z) : r(z; y) 2 S Next, we show by induction on the structure of # that if w^ is the root of C then C; w^ j= #. Finally, we acknowledge that C, as de ned above, might not necessarily be a context structure in the sense of De nition 1. Nevertheless, we show that there always exists a way of transforming C into a proper context structure C0, such that if # is satis ed in C then it is also satis ed in C0. This proves the existence of a model for # and thus concludes the proof of soundness. Lemma 2 (Termination). There is no in nite sequence of inference steps via the tableau rules.
Proof. Consider a formula # in NNF with all occurrences of [D]C transformed into :D t hDiC. Clearly, there is only a nite number of h i operators used in #, and hence, there can be only a nite number of unique context labels occurring in the tableau proof for # due to application of the )h i rule. Given that, there can be also only nite number of inference steps via the )6= rule, as well as via the ) rule for any individual variable. Note, that other than occurrences of h i # does not contain any symbols from beyond the ALC, hence the only problem for termination is posed by application of the )9 rule (clearly, upon suspending it there can be always only a nite number of possible inference steps). But given a nite number of context labels it has to be the case that at some point the )B rule applies, and all -minimal individual variables occurring in S are blocked. Hence the tableau procedure for # terminates in a nite number of steps. Lemma 3 (Completeness). If # is satis able then there exists a complete clash-free constraint system for #.
Sketch of proof. We assume # is satis able, with C = hW; C; ; fIwgw2W i being a context structure such that C; w^ j= #. In a usual manner, we use C as an oracle in determining the construction of a complete clash-free constraint system for #. Essentially, we argue by induction on the possible applications of the tableau rules, that given # is satis able, it is impossible to derive a clash in the process of construction of a constraint system: if a constraint system for # is clash-free before the application of a rule, it has to remain such also after that. Since, by Lemma 2 the number of inference steps applicable to S has to be nite, therefore at some point one has to obtain a complete constraint system, which is clash-free. 4
For a small example of a CALC knowledge base we will formalize part of Figure 1 depicted in the introduction. Consider knowledge base K = (T ; A), where TBox and ABox are de ned as follows:
T = f (1) City European City t Asian City; (2) European City u Asian City v ?; (3) hCityiThe Biggest hAsian CityiThe Biggest g A = f (4) hCityiThe Biggest(Tokyo);
(5) hEuropean CityiThe Biggest(Moscow) g
The TBox states that every city is either a European or an Asian city, and that, in fact, the two classes are disjoint. The third axiom ensures that the concept The Biggest has the same instances in the context of all cities, and in the context of Asian cities. The axioms in the ABox assert that Tokyo is the biggest among all cities, whereas Moscow is the biggest in the context of European cities. Given this setup it can be shown, for instance, that the following entailments hold:
K j= hCity u :European CityiThe Biggest(Tokyo)
K j= hCityi:The Biggest(Moscow)
Due to limited space we will not present full tableau proofs and resort only to informal arguments. The validity of the rst entailment rests on the fact that according to the TBox Asian cities are exactly those that are non-European cities (from 1). The comparison class denoted by Asian City is therefore equivalent to that described by City u :European City, and so the two descriptions represent in fact the same state in the context structure. Consequently, since Tokyo is an instance of The Biggest in the former context (from 4 and 3), it has to be such also in the latter.
To see that the second entailment follows as well, assume on the contrary that :hCityi:The Biggest(Moscow), i.e. :City t hCityiThe Biggest(Moscow). Clearly Moscow is a city (from 5 and 1), hence it would have to be an instance of The Biggest in the context of all cities, and consequently, in the context of Asian cities (from 3). But this would mean that Moscow is an Asian city, which is not true (from 2 and 5).
Note that, as intended, there is no contradiction between the fact that Moscow
is an instance of The Biggest in the context of European cities and an instance
of :The Biggest in the context of all cities. Finally we can de ne a context
structure C = hW; C; ; fIwgw2W i which models K. We pose:
The logic discussed in the previous sections can be seen as a special case of
multidimensional DLs [
In general, the problem of representing and reasoning with contextual
knowledge, in particular in relation to DL-like knowledge bases, has been quite broadly
studied in the literature, for instance in [
Finally, from a di erent perspective, CALC shares also some signi cant
similarities with dynamic epistemic logics, and in particular, with the public
announcement logic (PAL) [
Providing a sound formal account of context-sensitivity and related phenomena, which abound in the real-life knowledge representation and reasoning scenarios, is a longstanding challenge in Arti cial Intelligence, and quite recently, also in the research on the Semantic Web. In this paper we have addressed a very speci c form of that problem, namely, representation of relative terms, whose meaning depends on the selection of comparison classes, to which the terms are applied. For such tasks we have proposed language CALC , a simple extension of the DL ALC, which by utilizing an additional modal dimension introduced into standard ALC models allows for a roughly independent interpretation of the vocabulary of the language in the context of di erent comparison classes. This way the resulting reasoning regime complies much closer to the intuitions associated with the use of relative terms in the natural language, e.g. it does not allow for inferring contradiction based on existence of complementary statements about an object, as long as the statements apply to di erent comparison classes.
Admittedly, the scope of the proposal is very limited and in no way can
it pretend to have solved the problem of context-sensitivity in the DL-based
representations of knowledge. Nevertheless, we have showed that by a careful
use of supplementary modal dimensions one can obtain extra expressive power,
which on the one hand is su cient to handle certain interesting representation
problems, while on the other does not require deep revisions on the syntactic,
semantic nor, most importantly, the proof-theoretic side of the basic DL paradigm.
Our belief is that in a similar manner, aspects of multi-dimensionality can o er
convenient formal means for addressing other phenomena related to imperfect
knowledge, such as uncertainty or vagueness, which currently are approached on
the grounds of formalisms involving a thorough reconstruction of the semantics
and the proof theory of DLs, e.g. probabilistic, possibilistic or fuzzy DLs [
In the future work on CALC we want to focus on de ning suitable mechanisms of support for both relative and absolute (rigid) terms, preferably by distinguishing between local (contextualized) and global (applicable to all contexts) terminological constraints, so that some parts of vocabulary can be rendered context-independent. In a broader perspective, we intend to investigate ways of extending the approach to other types of context-sensitivity as well as to other aspects of imperfect knowledge representations.
Acknowledgements The rst author is funded by a Hewlett-Packard Labs Innovation Research Program.