Towards Agent-Oriented Knowledge Base Maintenance for Description Logic ALCN Stanislav Ustymenko1 and Daniel G. Schwartz2 Meritus University, School of Information Technology, 1 30 Knowledge Park Drive (Suite 301), Fredericton, New Brunswick, Canada E3C 2R2 , sustymenko@meritusu.ca 2 Department of Computer Science, Florida State University, Tallahassee, Florida, USA schwartz@cs.fsu.edu Abstract formulation, belief revision postulates are stated in terms of Artificial agents functioning in the Semantic Web are to be potentially infinite belief sets (although work has been done capable of getting knowledge from diverse sources. This to address this issue). We believe that belief revision is a implies the capability to continuously update their mature paradigm that can be valuable source for important knowledge bases. New stream reasoning concepts make this insight. However, there is a need for formal approaches that need even more pressing. Semantic Web ontologies are address the practical challenges more directly. commonly represented using description logic knowledge New research direction under the tentative title “stream bases. We propose an agent architecture with such features, reasoning” [6] emerged within the Semantic Web utilizing a Dynamic Reasoning System (DRS). This explicitly portrays reasoning as a process taking place in community. It explicitly deals with reasoning over rapidly time and allows for manipulating inconsistent knowledge changing and time-dependent data in a way that can deliver bases. We sketch a procedure for user-directed ontology answers to the user while they are still relevant. Stream debugging. This same mechanism can be used for reasoning is defined as “the new multi-disciplinary approach automated belief revision. We identify important research which will provide the abstractions, foundations, methods, directions that may benefit from this approach. and tools required to integrate data streams and reasoning systems” [7]. Della Valle et al. [5] write: “Stream-reasoning research definitely needs new theoretical investigations that 1 Introduction go beyond data-stream management systems, event-based systems, and complex event processing. Similarly, we must go beyond current existing theoretical frameworks such as The Semantic Web (SW) [4] is a common name of a family belief revision and temporal logic”. Currently, there is no of technologies extending the Web with rich, machine- consensus on a logic formalism appropriate for stream interpretable knowledge. The SW retains the massively reasoning. There is an obvious practical need for such decentralized nature of current World Wide Web, with an formalism to be able to integrate current, description logic- unlimited number of knowledge sources identifiable by based Semantic Web standards. unique URIs. It supports rich metadata annotation, including Dynamic Reasoning Systems (DRS) [17] provide a formal expressive ontology languages. Description Logics (DLs) [2] framework for modeling the reasoning process of an artificial emerged as leading formalism for knowledge representation agent that “explicitly portrays reasoning as an activity that and reasoning on the Semantic Web. takes place in time”. It sidesteps the logical omniscience Once widely implemented, the Semantic Web will support assumption of the classical AGM framework and has means intelligent software agents that will work with massive, of working with inconsistent knowledge bases by keeping decentralized ontologies, while other agents modify them in track of a proposition's derivation path. The DRS framework possibly inconsistent ways. Agents will need a way to absorb has been shown to support non-monotonic reasoning in a new knowledge in a timely fashion, all the while protecting natural way. the consistency of their knowledge bases, or, alternatively, A DRS can be defined for any language. DLs present a be able to draw useful inferences from inconsistent premises. challenge in that they do not have explicit derivation rules. Several approaches have been proposed to model Instead, DLs rely on inference algorithms to accomplish knowledge evolution over time. One of the most well- common reasoning tasks. One of the basic tasks is checking researched formalisms is belief revision [9, 10], specifically subsumption of concepts. the classic AGM framework [1, 9]. Substantial efforts have The goal of this paper is to present the DRS framework as a been extended to apply this approach to description logics suitable formalism for Semantic Web reasoning. To this end, [13, 14, 19, 20], and the work is ongoing. However, the we give an instance of DRS capable of building a concept belief revision framework does not explicitly address subsumption hierarchy for a well-known description logic. knowledge evolution in time. Also, in its original We believe it to be an important foundation for research on and individual names to elements of  I . The function belief dynamics for Semantic Web agents. Section 2 of this I paper contains a brief formal introduction to Description . extends to arbitrary concept definition in a rather Logics and the necessary definitions. Section 3 discusses intuitive way (for details, see [2], chapter 2). A concept is Dynamic Reasoning Systems. Section 4 describes a DRS and unsatisfiable if for any interpretation I , C I =∅ . agent reasoning process for deriving explicit subsumption Description Logic knowledge bases consist of two hierarchies from description logic ALCN terminology. Short components: a TBox, a set of statements about concepts, and abstract of this work appears in [20]. Finally, in Section 5, an ABox, a set of assertions about individuals. In general, a we draw some conclusions and discuss directions for future TBox T contains general concept inclusion axioms of the research. form C⊆ D (inclusion axiom). The pair of axioms C⊆ D , D⊆C is abbreviated C≡ D (equality axiom). An interpretation I satisfies an axiom C⊆ D 2 Description Logics if C I ⊆ D I . Interpretation I satisfies a TBox T if it satisfies every axiom in T . Languages for any description logic contain concept names, A definition is an equality axiom with an atomic concept role names, and individual names. Below, we will use on the left hand side. A TBox is a terminology if it consists of uppercase A and B for concept names, uppercase definitions and no concept name is defined more than once. letters R , P for role names, and lowercase x , y , z A concept name is a defined name if it appears on the left for individual names. hand side of the axiom and a base name if it doesn't. A DL languages combine role and concept names into definition is in the extended form if only base concept names concept definitions. Concepts of a description logic AL [16] appear on the right hand side. A terminology is definitorial if are defined as follows: every definition has exactly one extended form (not counting equivalent syntactic variants). In further discussion, we assume that our TBoxes are definitorial terminologies. Under C,D A | (atomic concept) this condition, we can assume, wlog, that definitions contain  | (universal concept) no cycles. An ABox contains assertions regarding individual names. ⊥ | (bottom concept) These include concept assertions C a  and role ¬A | (atomic negation) assertions R a , b. An interpretation I satisfies (or C∩ D | (intersection) is a model of) C a  if a I ∈C I and it satisfies R a , b. if a I , b I ∈ R I . Finally, I satisfies an ∀ R.C | (value restriction) assertion  (or an ABox A ) with respect of a TBox ∃ R. (limited existential T if it is a model of both an assertion (or an ABox) and quantification) the TBox. An ontology of concepts can be expressed using a DL. The More expressive DLs extend AL by the following term ontology is often applied either to a TBox or to a full DL constructs: knowledge base. We will occasionally use ontology in the former sense. Indication Syntax Name U C∪ D union 3 Dynamic Reasoning Systems E ∃ R.C full existential quantification The classical (propositional) notion of belief set [e.g., 9] N n R , n Rnumber restriction models it as an (often infinite) set of formulas of the C full negation underlying logical language. In our view, a belief set should ¬C be finite and should represent the agent’s knowledge and beliefs at a given point in time. Moreover, each formula in The commonly used DL ALCN extends AL with full such a belief set should contain information indicating how if negation and number restriction. In the following sections, was obtained and whether it has been used in subsequent we will restrict ourselves to ALCN. deductions, thereby enabling both backtracking and forward An Interpretation of a DL is a structure I = I , . I  , chaining through reasoning paths for so-called “reason maintenance”. where  I is a nonempty set called domain and . I is To this end, in [17] there was defined the notion of a an interpretation function that maps concept names to dynamic reasoning system (DRS), which explicitly portrays subsets of a domain, role names to subsets of  I × I , reasoning as an activity that takes place in time. This is obtained from the conventional notion of formal logical For a given agent, let us denote the agent’s belief set at system by lending special semantic status to the concept of a time step i by  i . Let  0=∅ . Thus the agent derivation path (i.e., a proof). Introduction of new knowledge initially has no knowledge or beliefs. Then, given  i , for or beliefs into the path occurs in two ways: either new propositions are added in the form of axioms, or some , i≥0 ,  i1 can be obtained in any of the following propositions are derived from earlier ones by means of an ways: inference rule. In either case, the action is regarded as 1. A new formula is received from an outside source, occurring in a discrete time step, and the new proposition is 2. A formula is derived from some formulas in  i labeled with a time stamp (an integer) indicating the step at which this occurred. Moreover, for propositions entered into by means of an inference rule, the path as a result of rule applications, the label additionally 3. A formula in  i has its status changed from on contains a record of which inference rule was used and to off. which propositions were employed as premises. Changing a formula’s status from on to off occurs during a At any given time, the contents of the path is regarded is reason maintenance process that is invoked whenever an being the sum total of the agent’s knowledge and beliefs as insatisfiability, i.e., a definition of the form A≡⊥ is of that time. Thus we here take this path as being the agent’s belief set as of that time. entered into the agent’s belief set. The objective of reason This is to be contrasted with other systems of belief maintenance is to remove this insatisfiability. revision, which assume that the agent additionally knows all This has two phases. First one starts back tracking from the the logical consequences of the basic belief set. Such systems insatisfiability, using the from lists in the formula labels, are said to exhibit “logical omniscience.” For an in-depth looking for the “culprit” formulas that occurred earlier and analysis of this issue, together with a manner of addressing which led to the inconsistency. A decision then must be made it, see the paper by Fagin, Halpern, Moses, and Vardi [8]. to turn the status of at least one of these formulas to “off”. For complete details of the notion of a DRS, please see Then one forward chains from this formula, using the to lists, [S97]. A brief outline is as follows. A labeled formula is to find all formulas whose derivations stemmed from the culprit formula, and likewise turns their status to “off”. This defined as a pair  P ,  where P ∈ L , where will include the inconsistent formula that triggered the reason L is a logical language, and the label  is an ordered maintenance process. 4-tuple (index, from, to, status), where: Which culprit formula to deactivate can be determined by the various culprits’ degrees of belief, to wit, remove the one 1. index is a non-negative integer, the index, that is least believed. In case the culprits are all believed representing the formulas position in the belief set. equally, one can be chosen at random. Alternatively, an agent 2. from is a from list, containing information about can remove the culprit formula that is the least important how the formula came to be entered into the belief according to some reasonable criteria. One such criteria is a set. Either it was received from an outside source cumulative belief level of formulas derived from the culprit. (obtained from some other agent or through This criteria provides a finite version of the AGM epistemic interaction with its environment), in which case the entrenchment relation. from list contains the token rec, or it was derived This model of agent-oriented reasoning reflects that view from some formulas occurring earlier in the belief that, at any given time, the agent’s beliefs may harbor an set, in which case the from list contains the name of inconsistency, but the agent does not become aware of this the derivation rule and the indexes of the formulas unless an inconsistent formula is explicitly entered into its used as premises in the derivation. The types of belief set. formulas that can be received are understood to This, in our opinion, is a realistic model of natural human include both axioms of the propositional calculus reasoning. Humans can comfortably maintain inconsistent and statements about the agents environment beliefs for long periods of time without ever realizing this. (sometimes distinguished as “logical” and But once they become consciously aware of a ”nonlogical” axioms). contradiction, they typically rethink their position and modify 3. to is a to list, containing the indexes of all formulas their beliefs so that the contradiction is removed. in the belief set for which the given formula served as a premise in the indexed formula’s derivations. 4. status is a status indicator, taking values on or off, indicating whether the belief represented by the formula is currently held, i.e., whether the formula may or may not be used in any future derivations. Whenever a formula is initially entered into the belief set, its status is on. 1. Local copy of the ontology, expressed as an ALCN TBox. This ontology consists of ALCN definitions Controller Environment that occur in the derivation path. 2. A subsumption tree of concept names. The latter can be used to support both browsing and user querying on both a TBox and an ABox. The user has a preference for satisfiable ontologies, so the agent has to detect and remove unsatisfiable concepts. Thus, our DRS needs to support 2 types of DL reasoning: DRS 1. Check if a defined concept A is satisfiable 2. Deduce atomic subsumption, that is, a statement of the form A⊆ B , Derivation Derivation path rules where A, B are concept names. To construct the DRS, we first note that if A and B are defined by axioms A≡C , B≡ D , where C, D are concept definition, then A⊆ B iff C ⊆D. Second, note that C⊆ Diff C∪¬ D is unsatisfiable. Fig.1 Reasoning agent employing a Dynamic Reasoning So both our reasoning tasks would require checking System satisfiability of concepts. We are using a generic tableau- based satisfiability algorithm [2, 3]. The reasoning agent (Fig. 1) uses a Dynamic Reasoning Now we can build our dynamic reasoning system. First, We System to reach conclusions that help advance the agent's define the language, L. The symbols of L are the same as the goals. A controller directs DRS behavior to steer it to such conclusions. The controller performs the following actions: symbols of logic ALCN. We use A, B for concept names occurring in the incoming statements and A', B' for the names 1. Receive information from the outside environment. introduced by the agents. The formulas of L are the The information can come from a human user, other following: agents, or be harvested by an agent through sensors. 1. Equivalence statements of the form A≡C , The latter can get information from any external where A is a concept name and C is concept data source. definition. Without loss of generality, we assume all 2. Enter information, as a “nonlogical” axioms concept definitions are in negation normal form, i.e. expressed in language L, into the DRS's inference negation only occurs in front of concept names. path. 2. Atomic subsumption statements of the form 3. Apply an inference rule. 4. Act to remove insatisfiability, by invoking belief A⊆ B , where A, B are concept names. These represent arcs of the subsumption tree the agent is revision procedure described above. building. The agent performs these actions in the order dictated by the 3. TBox assertions C a  , Ra ,b  , where C is a agent's and environment's current state, presumably in a concept, R is a role, and a,b are individual constants manner that would advance its goals. In the following, we 4. Explicit inequality assertions x≠ y , where are constructing an agent that would accept an ontology in x , y are individual names. the form of TBox definitions and construct a subsumption hierarchy of concept names implicit in this ontology. Then we define inference rules. Implicitly, every rule that modifies a concept definition also puts the result into negation normal form. The inference rules will be: 4 Dynamic Reasoning for DL ALCN 1. Substitution: from A≡C and B≡D infer A≡ E , where E is C with all A Dynamic Reasoning System is a model for knowledge occurrences of B replaced by D . For this base and reasoning process for artificial agent that assists a treatment we assume that our TBox does not contain user. We describe an agent that extracts ontological cycles in definitions. By repeatedly applying this knowledge from the Web and uses it to support a user's rule, we obtain an extension of definition for A browsing and querying activities. To this end, an agent that only contain ground concept names on the right maintains two information stores: side. 2. Subsumption test introduction: from A≡C , B≡ D infer A '≡C∩¬D , where A ' is a previously-unused agent-generated { yi ≠ y j∨1i≤ jn1} derive A≡⊥ , concept name. where x , y 1,. .. , y n1 are individual names, 3. From A≡C , B≡ D and A '≡⊥ , provided R is a role name and n0 . that name A ' was introduced using rule 2 with A≡C , B≡ D as premises, derive A⊆ B . Finally, rule 14 derives a subsumption axiom, using reduction to unsatisfiability: The following rules 4-10 are added to enable tableau- based consistency checks. These are derived from the 14. From A≡C , B≡D , A1≡C ∪¬D transformation rules listed in [2], p. 81. Individual names and A 1 ≡⊥ , derive A⊆ B x , y , z , ... are unique names generated by the agent. All TBox statements are derived from the same ABox A Dynamic Reasoning System based on language L and rules statement (that is undergoing satisfiability check) 1-14 is capable of supporting an agent that builds an explicit subsumption hierarchy. We will now describe a controller A≡C 0 : that can achieve this goal. An agent starts with an empty derivation path and empty 4. From A≡C 0 , infer C o  x 0  , if no ABox subsumption hierarchy. It will receive TBox definitions from statements were inferred from A≡C 0 . the user. To start the hierarchy, before receiving the first 5. From A≡C 0 and C 1∩C 2  x , infer axiom, the controller will enter a root concept, R≡ , as a first formula in the derivation path and R as a root node C 1  x  and C 2  x  , if any one of them is in the hierarchy. not yet inferred. Upon entering a new axiom of the form A≡C , the 6. From A≡C 0 and C 1∪C 2  x  , infer controller will perform the following actions: C 1  x  or C 2  x  , if neither of them is inferred yet. 1. Derive an expanded definition of A by repeatedly employing Rule 1 until the right side of 7. From A≡C 0 and ∃R.C  x  , infer the resulting definition contains no defined concept C  y  and R x , y , where y is a new names. generated name, if no z exists such that 2. Test satisfiability of A using Rules 4-13. If it is C  z  and R x , z  are already derived. unsatisfiable, flag it for a belief revision procedure 8. From A≡C 0 , ∀ R.C  x  and 3. Expand all (extended) definitions that depend on using Rule 1. Test the affected concepts' R x , y infer C  y  , if not already satisfiability, flagging for a belief revision process if derived. unsatisfiable. Update the hierarchy of concepts 9. From A≡C 0 and n R x  , infer affected by this step, testing subsumption by using R x , y1  , ... , R x , y n  and ( y i≠ y j , Rules 2-14. and R x , y , unless 4. Place A into its appropriate place in the R x , z 1 ,... , R x , z n  are already inferred. subsumption hierarchy, using Rules 2-14 to test subsumption with definitions of concept names 10. From A≡C 0 and n R x  , if already there. R x , y1  , ... , R x , y n1 are in the To test satisfiability by employing Rules 3-13, an agent derivation path and y i≠ y j is not in the path for follows a tableau-based algorithm. Details of the appropriate some i≠ j : replace all occurrences of y i algorithm, with discussion of termination and complexity, with y j . can be found in [2]. Rules 6 and 10 are non-deterministic: for a given ABox, they The following rules 11-13 detect inconsistency in TBoxes can be applied in finitely many different ways, leading to built using rules 4-10. As above, TBox statements are finitely many ABox'es. The concept is satisfiable if at least derived from A≡⊥ : one such ABox is consistent. Each ABox is a branch in the satisfiablilty algorithm. The controller may handle branches 11. From A≡C 0 and ⊥  x , derive A≡⊥ , by setting the belief status of statements on inactive branches where x is any individual name. to off. In practice, it may be useful to remove such statements 12. From A≡C 0 , A1  x  and ¬ A1  x , from the path to save space. We did not specify the details of modifying subsumption derive A≡⊥ , where x is any individual hierarchy on steps 3 and 4. In principle, the controller may name and A1 is any concept name. simply search the existing hierarchy starting at the root, 13. From A≡C 0 , n R x  , set testing the concept in question's subsumption with each node. {R x , y i ∨1in1} and This is a natural and decidable procedure that will result in set the correct hierarchy. Studying the complexity of such an algorithm and exploring possible optimizations is a task left References for future research. In case an unsatisfiable concept is detected, an agent will generate and display to the user the list of definitions that 1. Alchourrŏn, C.E., Gȁrdenfors, P., Makinson, D.: On the logic of lead to it. The user will have a choice to delete and modify theory change: partial meet contraction and revision functions, one of them. Methods for assisting the user or for achieving Journal of Symbolic Logic, 50, 2 (1985) this task without user interaction can be developed, based on 2. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel- research in ontology debugging and belief revision for Schneider. P. (eds.): The Description Logic Handbook, description logics [12, 13, 14, 21]. Developing such Cambridge University Press (2003) 3. Baader, F., Sattler, S.: Expressive number restrictions in algorithms is another task left for future research. Description Logics. J. of Logic and Computation, 9(3):319–350 (1999) 4. Bernes-Lee, T., Hendler, J., Lassila, O.: The Semantic Web. 5 Conclusions and Further Research Scientific American (2001) 5. Della Valle, E., Ceri, S., van Hamelern, F., Fensel, D.: It's a streaming world! Reasoning upon rapidly changing information. In the present work, we argued for the suitability of Dynamic Intelligent Systems vol.24 no.6, pp. 83-89 (2009a) Reasoning Systems [17, 18] as formalism for agent 6. Della Valle, E., Ceri, S., Fensel, D, van Hamelern, F., Studer, reasoning on the Semantic Web. To this end, we presented a R.: (Eds.): Proc. 1st International Workshop on Stream limited but realistic example of a DRS for performing a Reasoning , CEUR vol. 466 (2009) common reasoning task on a Description Logic ontology. 7. Della Valle, E., Ceri, S., Braga, D., Celino, I., Frensel, D., van We sketched a procedure for user-directed ontology Harmelen, F., . Unel, G., Research chapters in stream reasoning, In: Proc. 1st International Workshop on Stream debugging. This same mechanism can be used for automated Reasoning , CEUR vol. 466 (2009) belief revision. 8. Fagin, R., Halpern, J., Moses, Y., Vardi, M. Reasoning about Research in reasoning dynamics for the Semantic Web knowledge, MIT Press, Cambridge, MA, 1995 is a major part of the overall Semantic Web effort. The 9. Gȁrdenfors, P.: Knowledge in Flux: Modeling the Dynamics of problem has been approached from belief revision [14], Epistemic States, MIT Press/Bradford Books, Cambridge, MA ontology debugging [12], and now stream reasoning [6] (1988). perspectives. We believe the present approach has the 10. Gȁrdenfors, P., ed.: Belief Revision, Cambridge University potential to contribute to all these efforts. Press, NewYork (1992) There are several directions for future research. First, the 11. Hamilton, A.G., Logic for Mathematicians, Revised Edition , Cambridge University Press (1988). agent presented needs to be described in greater detail. 12. Parsia, B., Sirin, E., Kalyanpur, A.:Debugging OWL Procedures need to be fleshed out, and potential performance ontologies, in Proc. 14th International World Wide Web problems need to be identified and addressed. Complexity Conference (WWW'05), Chiba, Japan, May 10-14, 2005. ACM issues need to be discussed. There is also a possibility to use Press 2005 data stored in the derivation path to speed up new reasoning. 13. Ribeiro, M. M., Wassermann, R.: First Steps Towards Revising For example, incremental algorithms can be designed to Ontologies, In: Proc. 2nd Workshop on Ontologies and their utilize and extend existing derivation paths when a concept Applications, CEUR Workshop Proc. Vol. 166 (2006) gets updated through incorporating new definitions. 14. Ribeiro, M. M., Wassermann, R.: Base Revision in Description The agent can also be extended to support more varied Logics - Preliminary Results, In: International Workshop on Ontology Dynamics (IWOD) (2007) reasoning. It can be modified to accept more kinds of input, 15. Smolka, G: A feature logic with subsorts. Technical Report 33, including, e. g. , general inclusion axioms and TBox IWBS, IBM Deutschland, P.O. Box 80 08 80 D-7000 Stuttgart assertions. A facility to deal with user queries on an ABox 80, Germany (1988) needs to be added. The agent can be used as a model to build 16. Schmidt-Schauß, M., Smolka. G.: Attributive concept DRSs capable of dealing with Semantic Web standards and descriptions with complements. Artificial Intelligence, 48(1):1– more realistic scenarios (reasoning in the presence of loops 26, (1991) and redefinitions of concepts). On the other hand, less 17. Schwartz, D. G.: Dynamic reasoning with qualified syllogisms, expressive DLs can be investigated, in hope that they may Artificial Intelligence, 93(1-2) (1997) 103-167. 18. Schwartz, D.G.: Formal Specifications for a Document guarantee moderate computational complexity. Management Assistant, In: Proc. International Conference on Finally, the DRS formalism can be used to investigate Systems, Computing Sciences and Software Engineering (2009) belief revision techniques. Variants on the AGM 19. Qi, G., Liu, W., Bell, D. A.: Knowledge Base Revision in framework's rationality postulates can be constructed for a Description Logics, In Proc. European Conference on Logics in finite DRS case, both in general and specifically for Artificial Intelligence (Jelia'06), Springer Verlag (2006) description logics. Feasible algorithms adhering to these 20. Ustymenko, S., Schwartz, D.G., Dynamic Reasoning for principles need to be constructed. Finally, these postulates Description Logic Terminologies. Canadian Conference on AI and algorithms can be applied to interesting practical cases, 2010: 340-343 such as reasoning with multi sourced information that takes 21. Zhuang, Z. Q., and Pagnucco, M.: Belief Contraction in the Description Logic EL, In: 22nd Int. Workshop on Description into account different degrees of the agent's belief and trust Logics (DL 2009), CEUR Workshop Proc. Vol. 477 ( 2009) between agents.