Using Cognitive Entropy to Manage Uncertain Concepts in Formal Ontologies

Using Cognitive Entropy to Manage Uncertain Concepts in Formal Ontologies Joaqu´ın Borrego-D´ıaz and Antonia M. Ch´avez-Gonz´alez Departamento de Ciencias de la Computaci´on e Inteligencia Artificial E.T.S. Ingenier´ıa Inform´atica-Universidad de Sevilla Avda. Reina Mercedes s.n. 41012-Sevilla {jborrego,tchavez}@us.es Abstract. A logical formalism to support the insertion of uncertain concepts in formal ontologies is presented. It is based on the search of extensions by means of two automated reasoning systems (ARS), and it is driven by what we call cognitive entropy. 1 Introduction The challenge of data management with logical trust arose from the statement of the Semantic Web (SW). An important problem is the need for extending or revising ontologies. Such task is, from the point of view of companies, dangerous and expensive: since every change in ontology would affect the overall knowledge of the organization. It is also hard to be automated, because some criteria for revision cannot be fully formalized. Despite its importance, the tools designed to facilitate the syntactic extension or ontological mapping do not analyze, in general, their effect on the (automated) reasoning. Our aim is to design tools for extending ontologies in a semi-automated way, that is one of the problems present in several methods for cleaning data in the SW, when it implies ontological revision (see e.g. [1] [3]). The method is based on the preservation by extensions of the notion of ontology robustness,see[8]. lattice categoricity,(describedinsect.3),isgoingtobeappliedinaspecialcase: the change is induced by the user, who has detected the (cognitive) necessity of adding a notion. That is, a vague concept which comprises a set of elements with features roughly shaped by the existing concepts. In Ontological Engineering, careful consideration should be paid to the accurate classification of objects: the notion becomes a concept when its behavior is constrained by new axioms that relate it to the initial concepts. This scenario emphasizes the current need for an explanation of the reasoning behind cleaning programs. That is, a formalized explanation of the decisions made by systems. Note that such explanations are necessary for the desirable design of logical algorithms to be used by generalpurpose cleaning agents [4]. It is evident that the task will need not only specific This work is partially supported by the project TIN2004-03884 of Spanish Ministry of Education and Science, cofinanced by FEDER founds. automated reasoning systems (ARSs) for SW, but also those for general purpose. The reason is that some tasks are not directly related to reasoning services for the SW [2] [17] [8]. Thus, we use ARSs for first order logic theories, in favor of one reaches major generality. Among the challenges the problem raises in a dynamic setting as the SW, there are three of them which are specially interesting from the point of view of automated reasoning. They seem to obstruct the design of a fully formalised methodology [4] from classical database field: –We can not suppose the database to be stable (because new facts could be added in the future). –Usually, the specification of an ontology is syntactically complex, so it is very likely that classical axiomatization of database theory becomes inconsistent, even if ontology itself is consistent. –It is possible that the database does not contain facts about the whole relations of the language. However, some limitations can be solved by weakening the requirements imposed in both database and ontological reasoning [8] [2]. The method proposed is based on the assistance of two ARS, McCune’s OTTER and MACE4 (http://www-unix-mcs.anl.gov). The first one, OTTER, is an automated theorem prover (ATP) based on resolution and support set strategy. The program allows great autonomy: its auto2 mode suffices to find almost every automated proof that have been required. The second one, MACE4, is an automatic model finder sharing formula syntax with OTTER. It is based on Davis-Putnam-Loveland-Longemann’s procedure to decide satisfiability. It has been useful for analyzing the models of the involved theories. Finally, it would be good to add some information about MACE4. Despite it has not been formally verified to work correctly, once the result by MACE4 is determined, it is not difficult to certify that the models it gives are correct. It is necessary to use OTTER to prove that the list of models is exhaustive. Thus, MACE4 has been used as an automatic assistant to induce new results and investigate the effect of diverse axiomatizations, which must be certified later. 2 Logic-Based Ontological Extensions Once the need for revision is accepted, the task can be seen, up to some extent -and specially when one designs her/his own logical theory-, from two points of view. The first one considers it like a task similar to belief revision, analyzing it by classic methods of AI. Nevertheless, the effort can be expensive, because it must study once again the impact of revision on the foundational features of the source ontology. The second one has a foundational character. The evolution of ontology should obey ground principles which are accepted on this matter. For example, preserving some sort of backward compatibility, if it is possible (extracted from [15]): –The ontology should be able to extend other ontologies with new terms and definitions. –The revision of an ontology should not change the well-formedness of resources that commit themselves to an earlier version of the ontology. However, such principles are more adequate if the source ontology is robust, in the following sense [4]: An ontology is robust if its core is clear, stable (except for extensions); if every model of its core exhibits similar properties w.r.t. the core language, and if it is capable of admitting (minor) changes made out of the core without committing core consistency. By core we understand a portion of ontology that we consider as a sound theory with well known properties, and which is accepted as the best for the concepts involved. We can consider two kinds of extensions: –Extension by definition. It produces conservative extensions. If definitions are not provided for the new elements, conservation can fail. –Ontological insertion: Essentially new (nondefinable) concepts/relations are inserted. The task is to design good axioms to specify the new ones from core theory. An interesting case occurs in the task of ATP-aided cleaning of logic databases. The bottom-up change generation in ontologies -due to the analysis of track interaction among the Knowledge Base, the ATP and the userinduces ontological revision. It can simulate new elements in ontology to be inserted (such as Skolem noise [2]). We analyze here a slightly different problem, which appears when the user is the person who decides to insert a new concept by collecting a set of data. The extension by definition is the basis of definitional methodologies for building formal ontologies. It is based on the following principles [7]: 1. Ontologies should be based upon a small number of primitive concepts. 2. These primitives should be given definite model theoretic semantics. 3. Axioms should only be given for the primitive concepts. 4. Categorical axiom sets should be sought. 5. The remaining vocabulary of the ontology (which may be very large), should be introduced purely by means of definitions. In this paper, the first three principles are assumed. The fourth one will be replaced by lattice categoricity. Categoricity is a strong requirement that can be hard to achieve and to preserve. Even when it is achieved, the resultant theory may be unmanageable (even undecidable) or unintuitive. This phenomenon might suggest that we restrict the analysis of completeness to coherent parts of the theory. However, it is not a local notion: since minor changes commit the categoricity and it is expensive to repeat the logical analysis. With respect to the last principle, starting with a basic theory, it seems hard to define a new concept/relationship. It is better to consider it only as the starting point to build an ontology, thinking thus that we are in early steps of the process, where ontological insertions are necessary. Finally (although it is not the topic of this paper), we would like to add that an ontological insertion should be supported by a good theory about its relationship with the original ontology. It should as well be supported by a nice way of expanding a representative class of models of the source theory to the new one. This class of models must contain the intended models (those that the ontology designer wants to represent). It can be required an interpretation of the new elements which should be formalised, and a re-interpretation of the older ones, which must be compatible with basic original principles. 3 Lattice Categorical Theories In order to solve in practice the several logical problems that ontological insertion raises we will analyze the categoricity of the structure of the concepts of the ontology. We are going to take into account compatibility which has been previously mentioned, and we will try to obtain definitions of the concepts inserted in the new ontology. We will also analyze categoricity of structure of concepts of ontology. For the sake of clarity, we suppose that the set of concepts has a lattice structure. Actually, this is not a constraint: there are methods to extract ontologies from data which produce such structure (such as the Formal Concepts Analysis [14]) and, in general, the ontology is easy to be extended by definition, verifying lattice structure. Although we think about Description Logics [5] as ontological language (the logical basis for ontology languages as OWL, see http://www.w3.org/TR/owl-features/), the definitions are useful for full first order logic (FOL), so we give the definitions in FOL language. On the one hand, a lattice categorical theory is the one that proves the lattice structure of its basic relationships. This notion is weaker than categoricity or completeness. On the other hand, lattice categoricityis a reasonable requirement: the theory must certify the basic relationships among the primitive concepts. In [8] we argued that completeness can be replaced by lattice categoricity to facilitate the design of feasible methods for extending ontologies. Let us summarize these ideas. Given a fixed FOL language, let C={C1,...,C n}be a (finite) set of concept symbols, let Tbe a theory (in the general case, definable concepts in Tcan be considered). Given MamodelofT,M|=T, we consider the structure L(M,C), in the language LC={,⊥,≤}∪{c1,...,c n}, whose universe are the interpretations in Mof the concepts (interpreting cias CM i), is M,⊥is ∅and ≤is the subset relation. We assume from now on that L(M,C) is requested to have a lattice structure for every theory we consider. This requirement simplifies the examples. The relationship between L(M,C)andthemodelMitself is based in two facts. The first one, the lattice Lcan be characterized by a finite set of equations EL, plus a set of formulas ΘCcategorizing the lattice under completion, that is, ΘC includes the domain closure axiom, the unique names axioms and, additionally, the axioms of lattice theory. Thus, every model Mof E∪ΘCis finite. The second one, there exists a natural translation Πof these LC-equations into formulas in the FOL language so that if Eis a set of equations characterizing L(M,C)(so L(M,C)|=E), then M|=Π(E). Definition 1. Let Ebe a LC-theory. We say that Eis a lattice skeleton (l.s.) for a theory Tif Everifies that –There is M|=Tsuch that L(M,C)|=E∪ΘC,and –E∪ΘChas an unique model (modulo isomorphism). Every consistent theory has a lattice skeleton [8]. Roughly speaking, the existence of essentially different lattice skeletons makes difficult to reason with the ontology while the existence of only one would make it easy. Definition 2. Tis called a lattice categorical (l.c.) theory if whatever pair of lattice skeletons for Tare equivalent modulo ΘC. Note that if Tis l.c. and Eis a l.s. of T,thenTΠ(E). Note also that every consistent theory Thas an extension Twhich is lattice categorical: it suffices to consider a model M|=T, and then to find a set Eof equations such that ΘC∪Ehas L(M,C) as only model. The theory T∪Π(E) (and any consistent extension of it) is l.c. Finally, we can give a formalization of robust ontological extension,basedin the categorical extension of the ontology: Definition 3. Given two pairs (T1,E 1),(T2,E 2)we will say that (T2,E 2)is a lattice categorical extension of (T1,E 1)with respect to the sets of concepts C1and C2respectively, if C1⊆C 2and L(T2,C2)is an E1-conservative extension of L(T1,C1). For reasoning with the lattice of concepts it suffices to work with a lattice skeleton, so, to simplify, we suppose throughout that Tis the self l.s. 3.1 Cognitive Support Once formalized the notion of lattice categorical extension, we need to design several functions to advise how to select the best l.c. extension. Assume that Tis a theory, and Lis the lattice defined by Cin some M|=T. From the point of view of ontology designer, such a model Mis the intended model that the ontology attempts to represent. Suppose that Δ={h1,...h n} is the set of facts on C, and the user wants to classify some elements that occur in Δby means of a new concept. We can suppose, to simplify the notation, that every fact explicit in Tbelongs to Δ.LetU(Δ) be the universe determined by Δ;thatis,{a:∃C∈C[C(a)∈Δ]}. Given C∈Cin Δ,weconsider |C|Δ:= |{a:C(a)∈Δ}| and |C|Δ T:= |{a∈U(Δ):T∪Δ|=C(a)}|. Definition 4. The cognitive support of Cwith respect to Δ,Tand L,is supL T,Δ(C):=|{a∈U(Δ):∃i[Ci≤LC∧T∪Δ|=Ci(a)]}| |U(Δ)| This support estimates the number of facts on the concept Centailed by T, normalized by the size of the universe U(Δ). Because of the computational complexity of logical reasoning, it can be hard in general to compute it: we need to seek, by logical entailment, the cone of concepts defined by C. However, this computation is trivial for lattice categorical theories: Proposition 1. If Tis lattice categorical, then supL T,Δ(C)= |C|Δ T |U(Δ)| The proposition holds because if Ci≤LC,thenT|=CiC.Thus,ifT∪Δ|= Ci(a), then T∪Δ|=C(a). From now on, we suppose that Δis compounded by facts on atoms of the lattice of concepts (that is, about the most specific concepts). Note, also, that if Tis l.c., then Lis unique, and we will thus omit the superscript Lin that case. Corollary 1. If J={C1,...,C n}is a Jointly Exhaustive and Pairwise Disjoint (JEPD) set of concepts in L,thensupT,Δ(.)is a probability measure. Proof. It is easily seen that C∈J supL T,Δ(C)=1. The cognitive entropy of Jis CH(J)=− C∈J supT,Δ(C)logsupT,Δ(C). 3.2 Entropy of Ontological Extensions Suppose that the user decides that a set {a1,...,a k}⊆U(Δ) induces a new concept D(provisionally, a notion). Such a notion might not be fully represented by those elements. Also, it is possible that some of them do not belong to the new concept, because of noise in the data. It might also be the case that the concept is constrained by a set Σof axioms introduced by the user. Furthermore it is also possible that T∪Σis not l. c., that is, this theory does not prove the intended lattice induced by C∪{D}. MACE4 provides the collection {L1,...,L m}of the lattices induced by the models of T∪Σ.LetTibe a lattice skeleton for Li (i=1,...,m). Now, we focus our attention on a concrete level of the Ontology, where we intend to insert the new concept. The level will be a JEPD J={C1,...,C k}of the lattice Lverifying that if the new concept Dcontains some of them, JLi D={Ci∈J :Ci≤LiD} =∅ then Ji=(J\JLi D)∪{D}is a JEPD in Li.SinceTiis a l.c. extension of T, the support of Dis easy to achieve: Theorem 1. In above conditions, supTi,Δ(D)=  C∈J Li D supL T,Δ(Ci) To estimate the conditional entropy of the new extension, we consider a natural definition of conditional support: supTi,T,Δ(C|C):=|{a∈U(Δ):T∪Δ|=C(a)∧Ti∪Δ|=C(a)}| |C|Δ T This support allows to estimate the amount of new information produced by the extension by standard methods; through the conditional entropy associated to the two probability measures. The conditional cognitive entropy is : CH(J||Ji)=− C∈J C∈J i supTi,Δ(C|C)logsupTi,Δ(C|C) This sum can be simplified (assuming 0log0 = 0): if C=Cor C, C∈J,then supTi,T,Δ(C|C)logsupTi,T,Δ(C|C)=0 and the following property holds: Proposition 2. In above conditions, supTi,T,Δ(C|C)=|C|Δ T |C|Δ Ti This entropy is similar to Kullback-Leibler distance or relative entropy (see [16]), but using the entailment to classify the elements. It is known that it is minor than the initial entropy. In [13] similar entropies are used, but based on probabilistic assignation. Finally, in order to estimate what is the best extension for our purposes, it is necessary to compute the The Shannon’s diversity index for each Li. This index normalizes the amount of information produced by the extension, and is defined as IH(Ji)=CH(J||Ji) log|Ji| The interpretation of the index is as follows: if we select Liwith minimum IH(Ji), the new information produced by the new concept is minor. This option is the cautious one: the reparation of the source ontology is light and we do not expect big changes in the representation of the intended model. If we select Li with an upper IH(J), the change of the information is more relevant; we select such an extension if we regard as robust the specification of the concept given by Σtogether with the facts. In general, we have to chose the l.c. extension with minor index. Intuitively, in this way we do not change too much the information of the initial ontology. 4AnExample We would like to show a short example in the field of Qualitative Spatial Reasoning (QSR). Region Connection Calculus (RCC) [12] is a well-known mereotopological approach to QSR, that we can consider to be a robust ontology. For RCC, the spatial entities are non-empty regular sets. The primary relation between them is connection,C(x, y), with intended meaning: “the topological closures of xand yintersect”. The basic axioms of RCC are A1:= ∀x[C(x, x)] and A2:= ∀x, y[C(x, y)→C(y,x)] jointly with a set of definitions on the main spatial relations (fig. 1), and other axioms not used here (see [12]). DC(x, y)↔¬C(x, y)(xis disconnected from y) P(x, y)↔∀z[C(z,x)→C(z, y)] (xis part of y) PP(x, y)↔P(x, y)∧¬P(y, x)(xis proper part of y) EQ(x, y)↔P(x, y)∧P(y, x)(xis identical to y) O(x, y)↔∃z[P(z,x)∧P(z, y)] (xoverlaps y) DR(x, y)↔¬O(x, y)(xis discrete from y) PO(x, y)↔O(x, y)∧¬P(x, y)∧¬P(y, x)(xpartially overlaps y) EC(x, y)↔C(x, y)∧¬O(x, y)(xis externally connected to y) TPP(x, y)↔PP(x, y)∧∃z[EC(z, x)∧EC(z, y)] (xis a tangential prop. part of y) NTPP(x, y)↔PP(x, y)∧¬∃z[EC(z, x)∧EC(z, y)] (xis a non-tang. prop. part of y) Fig. 1. Axioms of RCC We have proved (by using MACE4 and OTTER) that the set of formulas E given in the figure 2 categorises under completion the lattice of the RCC-spatial relationships (given in fig. 3). The set of binary relations formed by the eight (JEPD) relations given in figure 3 is denoted by RCC8. If this set is thought to be a calculus, all possible unions of the basic relations are also used. Another interesting calculus is RCC5, based on {DR,PO,PP,PPi,EQ}. ≡CDR PO ¬P¬Pi¬DR DR ≡EC DC NTPP ¬TPP ¬Pi¬DR C ≡OEC TPP ¬Pi¬DR O≡POPPi EQ ¬PPi¬DR Pi ≡EQ PPi TPPi ¬NTPPi¬DR P ≡EQ PP NTPPi ¬DR PPi ≡TPPiNTPPi EC ¬DC PP ≡TPP NTPP Fig. 2. AskeletonforRCC Suppose that if we insert a new spatial uncertain relation Dexpressing “xand yhave a isometric overlapping relation”;thatis,Dcovers partial overlapping PO and extensional equality EQ relationships. That is, proper part is not possible between isometric objects. This is suggested by the study of spatial relationships among identical objects (e.g. the 2-D spatial configuration of a set of coins). Thus, we consider that the new relation Dsatisfies RCC ∪{∀x∀y(PO(x, y)→D(x, y)),∀x∀y(EQ(x, y)→D(x, y))} or, in terms of skeleton, E∪{PO D,EQ D}. MACE4 produces seven l.c. extensions (classified according to their lattices in fig. 4). All these extensions can be mereotopologically interpreted [11]. Suppose that the set that motivates the extension is: Δ:= ⎧ ⎨ ⎩ PO(m1,m 2)EQ(m2,m 3)EQ(m3,m 4)PO(m1,m 3)DC(m4,m 6) DC(m3,m 5)PO(m5,m 1)NTPP(c1,m 3)EC(c2,m 1)TPP(c2,c 5) DC(c1,c 2)TPPi(c5,c 2)NTPP(m2,c 4)DC(m1,c 3)TPP(c1,c 3) In this case, |U(Δ)|= 15, and the basic JEPD is the set J={PO,PP,EQ,PPi, EC,DC}.IneachLi,Jiis a JEPD, so we can assign conditional entropy and CDR O PPi PP PO EQ PPi EC DCNTPPiTPPiTPPNTPP 12345678 910 1211 13 14 15 16 0 a b abababab ab b a a b TPPi(a,b) NTPP(a,b) NTPPi(a,b) EQ(a,b) DC(a,b) EC(a,b) PO(a,b) TPP(a,b) Fig. 3. The lattice of spatial relations of RCC (left) and he relations of RCC8 (right) Shannon’s diversity index to each extension.Thus, T2≡E+∪{D≡POEQ}is the selected l.c. extension because it has the minimum Shannon’s index. On the other hand, the user’s notion might be inconsistent. For instance, if the user’s proposal for Σis {PO D, EQ D,P D, D O}, then there is not any l.c. extension, a fact that we have certified using MACE4 and OTTER. 5 Data-Driven Ontology Revision: Deficient Data Layout In above sections, we have formalized the insertion of a concept that will remain well defined once the appropriate extension is selected. In that case, the computation of entropies is easier than the entropies defined in this section. Now, we aim to extend the ontology in a provisional way because the deficient classification of data induces the insertion of subconcepts for refining the classification of individuals which initially were misclassified1. In this case the new concepts will fall in the bottom level. Therefore, we aim to extend JL, the JEPD set of concepts which are the atoms of the lattice L(T,C). The following definition formalizes the notion of insertion of a concept with certain degree of imprecision as subconcept of a given concept C.Ithastobe determined whether there is a l.c. extension of the ontology with an (atomic) subconcept μC of C. Intuitively, the meaning of μC(a) is “the concept afalls in the concept C, but we do not know any more specific information about a”. Formally, Definition 5. Let (T,E0)be a l.c. core and C∈C. We say that the ontology admits an undefinition at C(TwC) if there is a l.c. extension of T,(T,E), such that 1. Tis l.c. with respect to C∪{μC},(whereμC /∈C). 2. {μC}is an atom in the lattice L=L(T,C∪{μC}). 3. There is not Csuch that μC <LC<LC. 1This approach is inspired in the study presented at Eurocast 2007 [9].