We study the problem of reasoning over weighted ontologies. We assume that every axiom is labeled with an element of a distributive lattice (called its weight) and try to compute its so-called boundary, with respect to a given property. We show that axiom pinpointing is the most general instance of this problem. Finally, we present three applications of the problem of boundary computation.
In recent years, the study of pinpointing and other related problems has gained notoriety, due to the need to correct ontologies of very large size. The main motivation for pinpointing arises from the fact that ontology development is an error prone activity. Once an ontology grows beyond the few hundred axioms, it is not hard to encounter unexpected consequences that follow from it. Although not all unexpected consequences are necessarily wrong|indeed, they may be correct instances which were just previously unknown to the knowledge engineer|there is always a need to understand why they follow and, given the case, correct the ontology to get rid of them.
Axiom pinpointing deals with the problem of nding minimal subsets of an
ontology that entail a given consequence. These sets usually receive the name of
MinAs or justi cations. There exist two basic approaches toward pinpointing.
One tries to nd a monotone Boolean formula , called the pinpointing formula,
that encodes the set of all MinAs through a bijection with the minimal valuations
that satisfy [
Even when working on particular problems, the study of general solutions can
be helpful for shining light over speci c problems or characteristics that may not
be evident at rst sight. Thus, the study of pinpointing of general tableaux [
We introduce the notion of a boundary for a property. The boundary is a generalization of the pinpointing formula, where the axioms may be labeled arbitrarily, with elements of any distributive lattice. In other words, we have a weighted ontology. Intuitively, a boundary is an element of the lattice that separates the subontologies from which the property follows of those from which the property does not follow. We then investigate whether it is possible to compute such a boundary. In a way, we show that we already have a deep understanding of the boundary, through our knowledge of the pinpointing formula. In fact, we show that the pinpointing formula can be seen as an abstract representation of all the boundaries for a given property, which can be instantiated via a homomorphism between the free distributive lattice and the particular lattice under consideration at the moment.
Reasoning over weighted ontologies has applications beyond a better understanding of axiom-pinpointing. In general, we can think of axioms holding a weight that can represent how trusted it is, or how much it costs to access or use it, etc.
The paper is divided as follows. In Section 2, we motivate and introduce our notion of boundaries for properties. Then, in Section 3 we show that the boundary can always be computed as the image of the pinpointing formula through an adequate lattice homomorphism. Finally, before our conclusions, we present in Section 4 three scenarios where the computation of a boundary solves a reasoning problem with respect to DLs. 2
We start this section by introducing the properties we want to reason about. In general, a property can be de ned as a set of inputs, whose elements correspond exactly to those satisfying the property. In this work we want to reason with respect to knowledge bases, which are basically sets of axioms. However, not every set of axioms can be called a knowledge base. Consider, for instance, acyclic TBoxes: these are sets of concept de nitions that are irredundant and acyclic. Notice that every subset of an acyclic TBox is itself an acyclic TBox. Following these ideas, we consider knowledge bases as sets of axioms satisfying an admissibility restriction (we call these sets admissible) such that if T is admissible, then every subset of T is also admissible.
We de ne a property as a set of tuples of the form (I; T ), where I is an input and T is an admissible set of axioms. Such tuples are called axiomatized inputs. We are interested only in properties that are monotone with respect to the knowledge base in the sense that whatever follows from T must also follow from any (admissible) superset of T . A property P is called a consequence property (abbreviated as c-property) if (I; T ) 2 P implies that for every admissible set of axioms S, if T S, then (I; S) 2 P. Examples of c-properties are unsatis ability of concepts or subsumption w.r.t. TBoxes. The reason for imposing this monotonicity in the properties is to keep in track with previous notions of pinpointing. Recall that axiom pinpointing tries to nd all minimal subontologies from which the a given consequence follows; if the property relating ontologies with consequences is not monotone, nding such minimal sets does not make much sense.
Rather than just reasoning over a knowledge base T , we are interested in computing what will be later called a boundary based on weights associated to each of the axioms. This boundary will allow us to understand how weightdependent portions of the ontology in uence the property. This is now explained more formally.
Let (S; ) be a distributive lattice and = (I; T ) an axiomatized input. A
mapping lab : T ! S is called a labeling function. Intuitively, we want to compute
the highest point s in the lattice where we can cut our ontology without losing
the property; i. e. that the property still follows from the ontology having only
axioms whose label is greater than or equal to s . This generalizes the notion of
a pinpointing formula [
De nition 1 (Pinpointing formula). Let (I; T ) 2 P, lab a function mapping each t 2 T with a unique propositional variable, and P the set of all propositional variables labeling an element of T . A monotone Boolean formula over P is called a pinpointing formula for (I; T ) if for every S T it holds that (I; S) 2 P if and only if the valuation flab(t) j t 2 Sg satis es .
Notice that the set of distinct monotone Boolean formulas over P de nes a distributive lattice where the order is de ned by i ) . In this setting, conjunction corresponds to the greatest lower bound operator, and disjunction to the least upper bound. Additionally, each valuation V uniquely identi es an element of the lattice V = Vp2V p and a subontology TV = ft 2 T j lab(t) 2 Vg. This latter de nition is equivalent to TV = ft 2 T j V lab(t)g.
In the general case, we want to follow the same ideas as for pinpointing; thus, we de ne for every element s of the lattice S the subset Ts = ft 2 T j s lab(t)g. We are then looking for an element s 2 S that behaves as a pinpointing formula with respect to the lattice S and the labeling function lab; i. e. such that for every s 2 S it holds that s s if and only if (I; Ts) 2 P. Unfortunately, such a value does not necessarily exist, as shown by the following example.
Example 1. Consider the distributive lattice (S4; 4) having the four elements S4 = f0; a1; a2; 1g, where 0 and 1 are the least and greatest elements, respectively, and a1; a2 are incomparable w.r.t. 4. Let T be a set formed by the axioms ax1 and ax2, which are labeled by the elements a1 and a2 of S4, respectively, and let P be the c-property de ned as P = f(I; S) j jSj 1g, where jSj denotes the cardinality of S. It is easy to see that, given the axiomatized input = (I; T ), there is no element s that satis es the condition described above. Indeed, if we choose 0 or a1, then a2 violates the condition, as a2 6 s , but (I; Ta2 ) 2 P. And if 1 is chosen, then 1 itself violates it, as 1 s but (I; T1) 2= P. The reason why the property in this example fails to have an adequate s arises from asking the condition that s s i (I; Ts) 2 P to be satis ed by every element s 2 S. Indeed, if we look again at the case of pinpointing, we only ask this condition to follow for every valuation; that is, for formulas having no disjunction. Recall that in this speci c lattice, disjunction corresponds to the least upper bound (or join) operator. Then, valuations are join prime elements of the free distributive lattice; that is, they cannot be constructed as the join of other elements of the lattice. This notion will allow us to overcome the problem shown in Example 1.
De nition 2 (Join prime). Let (S; ) be a lattice. Given a set R S, let R denote the closure of R under the meet operator.1 An element s 2 S is called join prime relative to R if for every R0 R , s Lr2R0 r implies that there is an r0 2 R0 such that s r0. The element s is called simply join prime if it is join prime relative to S.
Obviously, any element that is join prime relative to a set R is also join prime relative to any subset of R. Moreover, if s is join prime relative to R and belongs to the sublattice generated by R, then s 2 R . Nonetheless, the converse is not true; that is, there may be elements of R that are not join prime relative to R. We will consider only the elements that are join prime relative to the image of the labeling function lab to de ne the boundary.
De nition 3 (Boundary). Let (S; ) be a lattice, P a c-property, = (I; T ) an axiomatized input and lab : T ! S a labeling function. Let Slab be the image of lab and Slab the sublattice generated by Slab. An element s 2 Slab is called a boundary for in P if for every element r 2 Slab that is join prime relative to Slab it holds that r s i (I; Tr) 2 P.
Returning to Example 1, we have that Slab = fa1; a2g and Slab = S4. The only element of S4 that is not join prime relative to Slab is 1, which is itself a boundary.
Notice that we have restricted the discourse in De nition 3 to the join prime elements relative to Slab that belong to Slab. This restriction is done without loss of generality. Indeed, as S is a distributive lattice, so is Slab. Then, every element s of Slab can be written as the join of all the join prime elements (relative to Slab) in Slab that are smaller or equal to s. This in particular shows that for every r 2 S that is join prime relative to Slab, if (I; Tr) 2 P, then there is a r0 2 Slab join prime relative to Slab such that (I; Tr0 ) 2 P. For simplicity, for the rest of this paper we will assume w.l.o.g. that S = Slab. As the ontology is nite and nitely generated distributive lattices are also nite, this assumption in particular entails that S is also nite. 3
Up to now we have presented the pinpointing formula of a property w.r.t. a given axiomatized input as a special case of boundary, from which we attempted to 1 To avoid confusion with the Boolean operators, we denote the lattice operators by (join) and (meet). develop the general notion. As it turns out, the pinpointing formula can be seen as an abstract representation of a boundary w.r.t. distributive lattices. Given a labeling function, the pinpointing formula can be then instantiated to the desired boundary. We proceed now to explain this in more detail.
Recall that the de nition of pinpointing formula requires a labeling function that maps each axiom in T to a unique propositional variable. The closure of the image of this labeling function over the logical operators disjunction and conjunction yields the lattice of all monotone Boolean formulas over the set of labels. This lattice, which we will denote BT , is in fact the free distributive lattice generated by jT j incomparable elements. As the labels of any two di erent axioms are incomparable w.r.t. BT , this mapping in fact de nes the most general distributive lattice one can produce through a labeling function. We will exploit these characteristics building an homomorphism between BT and the distributive lattice S that preserves the boundary; i. e. that maps the pinpointing formula to the boundary on S.
In the following, we consider a c-property P and an axiomatized input = (I; T ) such that 2 P. We denote by labB the labeling function that maps each axiom in T with a unique propositional variable in BT , and by the pinpointing formula for .
Consider now a distributive lattice S and let labS be a labeling function mapping each axiom in T to an element of S. We build a function h : BT ! S inductively, as follows: for every propositional variable p 2 BT , let t 2 T be such that labB(t) = p; then h(p) = labS (t). Given two formulas 1; 2 2 BT , we de ne h( 1 ^ 2) = h( 1) h( 2) and h( 1 _ 2) = h( 1) h( 2). Obviously, the function h is an homomorphism. We show now that it maps the pinpointing formula to a boundary.
in P.
be a pinpointing formula for , then h( ) is a boundary for Proof. Assume w.l.o.g. that is in DNF; that is, = 1 _ : : : _ n, where each i is a conjunction of propositional variables. Then, for every i; 1 i n, h( i) 2 (Slab) , and h( ) = Ln
i=1 h( i). We need to show that, for every r 2 S join prime relative to Slab, r h( ) i (I; Tr) 2 P. For r 2 S, de ne the valuation Vr := flabB(t) j r labS (t)g. Notice that Tr = TVr and h(Vr) = r. We have then that (I; Tr) 2 P i (I; TVr ) 2 P which, as is a pinpointing formula, holds i Vr satis es i r = h(Vr) h( ). tu
This theorem tells us that computing the pinpointing formula for an
axiomatized input su ces for obtaining the boundary w.r.t. any distributive lattice and
any labeling function. There exist several methods for computing the
pinpointing formula either by modifying a decision procedure [
For instance let S be a ( nite) total order, which is obviously a distributive lattice where all the elements are join prime. Given a labeling function lab, we can compute a boundary for making polynomially many calls to a reasoner as follows. Let sn < : : : < s2 < s1 be all elements of S. Starting from i = 1, iteratively test whether (I; Tsi ) 2 P. If the answer is no, then increase i by one, and test again; otherwise, i. e. if the answer is yes, then si is the boundary. This black-box process needs at most n calls to the reasoner. Notice that n is bounded by the number of axioms in T , as S is in fact the image of lab. Thus, if P can be decided in polynomial time in the size of T , then this method computes the boundary in polynomial time in the same measure. In the next section we will show a setting where nding a boundary over a total order is useful.
In [
On the other hand, computation of a boundary through the pinpointing formula has the clear bene t of needing to be done only once and be applicable even if the lattice or labeling function change, as long as the ontology itself remains unmodi ed. 4
Additionally from the computation of a pinpointing formula, there exist other scenarios where the computation of a boundary is a problem of interest. In this section we present three such cases: access control formalisms, fuzzy, and possibility reasoning. 4.1
Consider the following setting. We have a distributive lattice de ning a rights hierarchy. Each axiom in an ontology is associated to a security level : an element in the rights hierarchy representing the minimum rights necessary for accessing or viewing the axiom. Lower elements of the rights hierarchy represent higher security levels; thus, for instance, public axioms may be labeled with the supremum element 1, while con dential information should have a security level close to the in mum of the lattice.
This ontology is then accessed by users. Each user is associated also with an element of the lattice, which corresponds to its access level. The access level represents the rights this user has for watching axioms in the ontology: she should be able to see all the axioms having a security level that is at most as high as her access level. In other words, if s is the access level of the user, then she has access to the subontology Ts.
Obviously, the goal of an ontology is not merely to rest alone and be observed by the users; instead, users should be able to reason over it and deduce implicit consequences from the explicitly stated axioms. However, a user with access level s should be able to see only those consequences that follow from Ts, but not others that may be derivable from axioms with a higher security level. Thus, reasoning should depend on the user's access level.
One possible way of performing this reasoning is to rst compute the subontology Ts and only derive consequences from it. Although such a method would yield the correct results, it is in many cases impractical and undesirable. Consider for instance the computation of the concept lattice from the ontology. This task is usually very time consuming, but may be done once and for all, and then stored in an easily accessible way. If we decide to perform reasoning with respect to each of the ontologies Ts, then it would be necessary to compute a concept hierarchy for each access level s, and store them independently. A better strategy is simply to compute the boundary of each subsumption relation building the hierarchy.
For the boundary to behave in the desired manner, the access levels assigned to users need to be join irreducible relative to the set of labels of axioms. This restriction actually makes sense for an access control application. Indeed, elements that are not join prime have an ambiguous behaviour. Informally, if we denote as Ps all the consequences that can be deduced from Ts, then an access level of the form s1 s2 refers to an individual that can see all consequences in Ps1 \ Ps2 , but not those in Ps1 n Ps2 . This is a very strange condition, to say the least.
Additionally, it is not uncommon that security and access levels change with time. A simple example of this would be nancial information that becomes public after several years being con dential, or an individual that is promoted to a more trusted position. In such a case, computing the pinpointing formula as an abstract representation of the boundary appears as a good idea since changes in the labeling function that de nes the security level do not a ect the pinpointing formula, and hence no new reasoning, apart from updating the homomorphism from BT to the rights hierarchy, is necessary. 4.2
A totally di erent application of a boundary is aiding in reasoning in DLs extended with fuzzy operators. More precisely, we consider Godel norm and its residuum. For a better understanding, we brie y recall the main concepts of fuzzy logic and instantiate them to the fuzzy ALC.
Generally speaking, a fuzzy logic is a logic in which the crisp constructors
(such as conjunction and disjunction) are replaced by fuzzy constructors,
generally instantiated in the shape of t-norms and residua. These functions try to
simulate the behaviour of the well-known crisp operators, but allowing for
values in the whole range between 0 and 1. More formally, a triangular norm (or
t-norm for short) is a function t : [0; 1] [0; 1] ! [0; 1] that is commutative,
monotone, associative and has 1 as its neutral element. A t-norm usually
replaces the conjunctive operator of the logic. There exist several t-norms (see,
e.g. [
For every t-norm that is left continuous there is a unique binary operation r called the residuum or R-implication, such that r(x; y) = supfz j t(x; z) yg. The name of R-implication is motivated by the fact that this operation is typically used to replace the crisp implication. With these two operators, we can then de ne others in such a way that desired logical properties are satis ed. For instance, fuzzy disjunction (called triangular conorm or s-norm for short) is de ned as s(x; y) = 1 t(1 x; 1 y) as a generalization of De Morgan laws.
With these operators, we can de ne a variant of ALC, in which reasoning is done with respect to fuzzy TBoxes. These TBoxes are sets of GCIs labeled with a number in [0; 1] representing a degree in which the GCI must be satis ed. When using the Godel t-norm, this logic is a special case of the logic introduced in [18].
The syntax of fuzzy-ALC is identical to that of ALC, except for fuzzy-GCIs which, as said before, are tuples of the form (C v D; n), where C; D is a GCI and n 2 [0; 1]. A fuzzy-TBox is a set of fuzzy-GCIs.
The semantics of this logic is also based on interpretations, but in this case
they need to express not only whether e.g. an individual belongs to a concept, but
also to which degree this is done. Thus, an interpretation I is a tuple I = ( I ; I )
where I is a non-empty set and I is a function that maps each concept name A
to a membership function AI : I ! [0; 1] and each role name r to a membership
function rI : I I ! [0; 1]. This function can then be extended to concepts
using the standard fuzzy interpretation for the crisp constructors [
An interpretation I is a model of the fuzzy-GCI (C v D; n) if and only if infd2 I fr(CI (d); DI (d)gg n. I is a model of the fuzzy-TBox T if it is a model of every fuzzy-GCI in T .
We are interested in the problem of fuzzy subsumption : we say that a concept C is fuzzy subsumed by a concept D with degree n 2 [0; 1] w.r.t. a fuzzyTBox T , denoted as (C vT D; n), i for every model I of T it holds that infd2 I fr(CI(d); DI(d)gg n.
It can be shown that if we consider Godel t-norm tG with its standard snorm sG, residuum rG and negation nG, then for every n 2 [0; 1] it holds that (C vT D; n) if and only if C is (crisp) subsumed by D w.r.t. the ontology Tn = fC v D j (C v D; m) 2 T with n mg.
In fuzzy reasoning, it is interesting to nd the best degree bound ; that is, the highest value of n such that (C vT D; n) holds. In the particular case of the Godel norm, this problem reduces to nding the boundary with respect to the total ordering in the segment [0; 1], but restricted to those values that label some GCI in T . Notice that this yields a nite total ordering, and hence the black-box approach sketched in the previous section can be used for computing the best degree bound within the same complexity bound as merely deciding subsumption w.r.t. crisp TBoxes. In particular, this means that this problem can be solved for the fuzzy logic f-EL+ [17] in polynomial time measured in the size of the TBox.
It is important to notice, however, that the choice of Godel t-norm is fundamental for this approach to work. Indeed, the idempotency of this t-norm and its associated conorm is the main responsible for the generation of the nite total order that makes the de nition of boundary applicable in this setting. Thus, although fuzzy logics can be de ned for non-idempotent t-norms, the decision procedure obtained by computing boundaries is of no aid in them. 4.3
One other application for the computation of boundaries refers to possibilistic
reasoning [
Given an ontology T , where every axiom t has an associated certainty degree (t), we de ne, for every n 2 (0; 1] the subontology Tn in the obvious way; that is, Tn = ft 2 T j (t) ng. We can then reason about the necessity degree of distinct consequences of this knowledge base [14]: we say that C is subsumed by D with degree n w.r.t. T i the following three conditions are satis ed: (i) Tn is consistent; (ii) C vTn D; and (ii) for all m > n, C 6vTm D.
For deciding whether a subsumption follows with a given degree n0, the
computation of a boundary is useful in two di erent ways. First, one needs to
nd the minimum n such that Tn is consistent. Notice that, due to Condition (i)
above, for any n smaller than such a minimum, reasoning will not yield any
consequence; this is known as the drowning problem of possibilistic logic [
Once we have found the reduced consistent ontology, we need to nd the maximum n such that the subsumption relation follows from Tn. This corresponds once again to the computation of a boundary, whose result is exactly the necessity degree.
As in the previous subsection, the lattice considered for possibilistic reasoning is a total ordering, where only nitely many elements are actually relevant. Thus, possibilistic reasoning can be done within the same complexity bounds as standard DL reasoning.
One thing that must be noticed in this case is that the drowning problem is not always a desirable property, even in possibilistic reasoning. Thus, alternative de nitions have been devised for such reasoning (see, e.g. [14]). Although it is not absolutely certain that boundary computation is not possible using these alternative de nitions, a nave application of the methods presented in this work yields an incorrect answer. Thus, if boundary computation is to be useful in this setting, a more elaborate approach will be necessary. 5
We have presented the problem of boundary computation, which allows us to reason about portions of ontologies, depending on weights associated to the axioms. A previously known instance of boundary computation, which also worked as motivation for our general framework, is that of axiom pinpointing. We showed that the pinpointing formula can be seen as an abstract representation of all boundaries with respect to a given property. In fact, given an instance of a distributive lattice S and a labeling function lab, there is an homomorphism that maps the pinpointing formula to the boundary w.r.t. S and lab. Thus, previously known methods for computing the pinpointing formula can be directly applied to the computation of a boundary. Additionally, if the lattice S and the labeling function lab are known and xed, the methods can be easily adapted to compute this boundary directly, without detouring through the pinpointing formula, improving this way the total execution time of the algorithm. We have shown the usefulness of our general approach by presenting three basic applications additionally to pinpointing. First, we showed how the boundary can help reasoning over a rights hierarchy, to control access to an ontology and the consequences derivable from it. Then we showed how boundaries relate to non-standard logics by showing their applicability to special cases of fuzzy- and possibilistic reasoning.
This paper gives just the rst steps towards a general study of boundaries, and as such there is much work that can still be done. For one, it would be desirable to nd more settings where the computation of a boundary yields a value of interest. Another area of future research is the analysis of distributive lattices and labeling functions, with the aim of nding classes where computing the boundary requires less resources than pinpointing, which is known to be hard even for very inexpressive logics. Third, we are interested in nding out whether similar ideas can be applied to more general algebraic structures, rather than distributive lattices. Such a generalization could be helpful for reasoning with respect to other t-norms, or the variants of possibilistic logic. Alternatively, it could be used to compute properties that change over time, or where the repeated use of the same axiom has a di erent in uence on the result than a single application. Last, pinpointing has shown that it is not always necessary to compute the exact pinpointing formula, and that approximate solutions are sometimes easy to compute. We would like to investigate settings where approximate boundaries would be of interest, particularly when an approximation su ces to adequately solve a problem. 13. T. Meyer, K. Lee, R. Booth, and J. Z. Pan. Finding maximally satis able terminologies for the description logic ALC. In Proc. of the 21st Nat. Conf. on Arti cial Intelligence (AAAI 2006). AAAI Press/The MIT Press, 2006. 14. G. Qi, J. Z. Pan, and Q. Ji. Extending description logics with uncertainty reasoning in possibilistic logic. In ECSQARU '07: Proceedings of the 9th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty, volume 4724 of LNAI, pages 828{839, Berlin, Heidelberg, 2007. Springer-Verlag. 15. R. Reiter. A theory of diagnosis from rst principles. Arti cial Intelligence, 32(1):57{95, 1987. 16. S. Schlobach, Z. Huang, R. Cornet, and F. Harmelen. Debugging incoherent terminologies. Journal of Automated Reasoning, 39(3):317{349, 2007. 17. G. Stoilos, G. B. Stamou, and J. Z. Pan. Classifying fuzzy subsumption in fuzzyEL+. In F. Baader, C. Lutz, and B. Motik, editors, Proceedings of the 2008 Description Logic Workshop (DL 2008), volume 353 of CEUR Workshop Proceedings.
CEUR-WS.org, 2008. 18. U. Straccia. Reasoning within fuzzy description logics. Journal of Arti cial Intelligence Research, 14:137{166, 2001. 19. B. Suntisrivaraporn, G. Qi, Q. Ji, and P. Haase. A modularization-based approach to nding all justi cations for OWL DL entailments. In J. Domingue and C. Anutariya, editors, Proceedings of the 3rd Asian Semantic Web Conference (ASWC'08), volume 5367 of LNCS, pages 1{15. Springer-Verlag, 2008. 20. C. B. Tresp and R. Molitor. A description logic for vague knowledge. In Proc. of the 13th Eur. Conf. on Arti cial Intelligence (ECAI'98), pages 361{365, 1998.