福彩号码查询

学霸学习网 这下你爽了

学霸学习网 这下你爽了

- Deverbal nouns in knowledge representation
- Knowledge representation in machine learning
- Knowledge Representation for Interrogatives in E-HowNet
- Knowledge Representation and Processing in Intelligent Software Measurement System (ISMS)
- A case study in using preference logic grammars for knowledge representation
- 1 Key Concepts in the O-Plan2 Knowledge Based Plan Representation
- Functional Descriptions as a Formalism for Linguistic Knowledge Representation in a Generat
- Controlled Languages for Knowledge Representation in FOL
- Decidable Reasoning in Terminological Knowledge Representation Systems
- Representation of HighlyOEComplex Knowledge in a Database

福彩号码查询 www.edasl.tw Modalities in Knowledge Representation

Ullrich Hustadt and Andreas Nonnengart

Max-Planck-Institut fur Informatik, Im Stadtwald, 66123 Saarbrucken, Germany

Standard knowledge representation systems are supposed to be able to represent either common or individual knowledge about the world. In this paper we propose an extension to such knowledge representation systems which, in a uniform manner, allows to express beliefs of multiple agents as well as knowledge, desire, time and in fact any modality which has a rst-order predicate logic possible world semantics. Since the mid-seventies a variety of knowledge representation systems in the tradition of semantic networks and terminological logics has been proposed. The most famous example is KL-ONE3 which rst appeared in 1977 in R. J.1 Brachman's Ph.D. thesis. Other examples are KRYPTON2, NIKL12, and KRIS . All these systems can be used to represent common or individual knowledge about the world. Recently, terminological logics have been extended to allow the representation of the knowledge or the beliefs of multiple agents in one knowledge base4; 7. In this paper, we investigate such an extension which allows not only to represent either knowledge or beliefs of multiple agents but a huge variety of modal operators for multiple agents. We assume four disjoint alphabets, the primitive concepts C , the primitive roles R, the set M of modal operator names , and the individual objects O. In particular, there is a distinguished subset A of the individual objects, called the set of agents, containing the special agent all which is supposed to denote the union of all the agents in order to be able to express mutual belief. The tuple (O; A; M; C ; R) is called the signature, denoted by . The set of concept terms (or just concepts) and role terms (or just roles) is inductively de ned as follows. Every primitive concept is a concept term and every primitive role is a role term. Now assume that C , C1, and C2 are concepts, R, R1, and R2 are roles, m is a modal operator name, a is an agent's name. Then C1 u C2, :C , 9 R:C , and 3(m;a) C are concept terms, and R1 u R2, R?1 , R C , 2(m;a) R and 3(m;a) R are role terms. Thus we are now able to describe the sentences of our language Mod-ALC which are divided into terminological sentences and assertional sentences. If C1 and C2 are concepts and R1 and R2 are roles then C1 v C2, R1 v R2 are terminological sentences. If C is a concept, R is a role, and O, O1, and O2 are individual objects then

ABSTRACT

1 Introduction

2 Syntax and Semantics for Mod-ALC

O 2 C and (O1; O2) 2 R are assertional sentences. Moreover, if is a terminological (respectively assertional) sentence and if m is a modal operator name and a is an agent's name then 2(m;a) and 3(m;a) are terminological (respectively assertional) sentences. A set of terminological and assertional sentences is a knowledge base. So far the syntax of Mod-ALC has been described. Now we have to provide its semantics. De nition 1 ( -Structures) As usual we de ne a -structure as a pair (D; I ) which consists of a domain D and an interpretation function I which maps the individual objects to elements of D, primitive concepts to subsets of D and the primitive roles to subsets of D D. De nition 2 (Frames and Interpretations) By a frame F we understand any pair (W ; <) where W is a non-empty set (of worlds) and < = Um2M;a2A <a where m the <a 's are binary relation on W , the so-called accessibility relations between m worlds. By a -interpretation = based on F we understand any tuple (D; F; =loc; ) where D denotes the common domain of all -structures in the range of =loc, F is a frame, and =loc maps worlds to -structures with common domain D which interpret agents' names equally. De nition 3 (Interpretation of Terms) Let = = (D; F; =loc; ) be a -interpretation and let =loc( ) = (D; I ). We de ne the interpretation of terms inductively over their structure: =(C ) = I (C ) if C is a primitive concept =(R) = I (R) if R is a primitive role =(C1 u C2) = =(C1) \ =(C2) =(:C ) = D n =(C ) =(9 R:C ) = fd 2 D j e 2 =(C ) for some e with (d; e)a2 =(R)g =(3(m;a) C ) = fd 2 D j d 2 = ](C ) for some with <m( ; )g =(R1 1u R2) = =(R1) \ =(R2) =(R? ) = f(x; y) 2 D D j (y; x) 2 =(R)g =(R C ) = f(x; y) 2 =(R) j y 2 =(C )g =(2(m;a) R) = f(x; y) j (x; y) 2 = ](R) for all with <a (a; )g m =(3(m;a) R) = f(x; y) j (x; y) 2 = ](R) for some with <m( ; )g where = ] = (D; F; =loc; ). De nition 4 (Satis ability) Let = = (D; F; =loc; ) be a -interpretation. We de ne the satis ability relation j= inductively over the structure of Mod-ALC sentences: = j= C1 v C2 i =(C1) =(C2) = j= R1 v R2 i =(R1) =(R2) = j= x 2 C i I (x) 2 =(C ) = j= (x; y) 2 R i (I (x); I (y)) 2 =(R) = j= 2(m;a) i = ] j= for every with <a ( ; ) m = j= 3(m;a) i = ] j= for some with <a ( ; ) m

are models for then we call a theorem. Any sentence for which no model exists is called unsatis able. Thus, is a theorem i its negation is unsatis able. Let T be a set of Mod-ALC sentences. We say T entails , written T j= , i every model of T is a model of . So far we did not consider any special properties of the given modal operators. Typical axiom schemata which re ect such potential additional properties are listed below. Axiom Schema Property 2(m;a) ) 3(m;a) 8x9y <a (x; y) m 2(m;a) ) 8x <a (x; x) a m ) 2(m;a) 3(m;a) 8x;ay <a (x; y)a) <m(y; x)a m 2(m;a) ) 2(m;a) 2(m;a) 8x; y; z <m(x; y) ^ <m (y; z) ) <m (x; z) 3(m;a) ) 2(m;a) 3(m;a) 8x; y; z <a (x; y) ^ <a (x; z) ) <a (y; z) m m m Table 1: Properties of the accessibility relation Historically, these properties are called D, T , B , 4, and 5 respectively. If we consider modal operators for belief, i.e. 2(believe;a) and 3(believe;a) , then 4 and 5 are axioms of introspection. Intuitively, they say that the agent a has complete insight what his own beliefs are concerned. Property T is one of the major characteristics of modal operators for knowledge, i.e. 2(knows;a) and 3(knows;a), because it enables us to deduce a fact about the real world from an agent's knowledge about the world. De nition 6 Let R be a set of properties of the accessibility relation. An interpretation = is called a R-interpretation if the accessibility relation < of the underlying frame F satis es all properties in R. We say a set of Mod-ALC sentences T entails in all R-interpretations, written T j=R , if all R-interpretations which are models of T are also models of . What is remarkable for the properties from above is that they all are rst-order properties. Therefore it is not too surprising that a translation of modal terminological and modal assertional axioms into rst-order predicate logic can be done very easily.

De nition 5 Let = be an interpretation and let be a Mod-ALC sentence with = j= . Then we call satis able and we call = a model for . If all interpretations

3 Translating Mod-ALC into Classical Logic

There have been a lot of proposals for correct and complete calculi for nonclassical logics | temporal logics11, epistemic logics8, etc. | and terminological logics3; 5. Unfortunately, these calculi require implementations for their respective theorem proving system with hardly a chance to apply results and techniques of the traditional work on automated theorem proving. Therefore, we follow the approach of Ohlbach10 to eliminate modal operators in a way that we get standard rst-order predicate logic formulae that still represent the modal semantics.

However, if we take a closer look at the results of a straightforward translation of terminological and assertional sentences into rst-order logic we can see quite a big problem. Already simple knowledge bases result in rather huge clause sets where many of the clauses merely express certain informations about accessibilities and role correlations. But we can exploit a property of the language Mod-ALC which is typical for most modal and terminological logics, namely, each accessibility relation symbol or role symbol R occurs either in the form 9x R(: : : ; x) ^ (x) or in the form 8x R(: : : ; x) ) (x). First of all let us de ne what we mean by a functional simulator. De nition 7 (Functional Simulators) Let < be an n-ary relation. A set F< of functions is called a functional simulator for < if for any x1; : : :; xn <(x1; : : :; xn) i there exists a f 2 F< with f (x1; : : : ; xn?1) = xn In particular, if < is total, i.e. for any x1 : : : xn?1 there is a xn such that <(x1; : : : ; xn) then each function in F< is total, too. I.e. a functional simulator for some relation R is a set of functions which is able to take over the responsibilities of R. What a functional simulator is on the meta-level are the simulator axioms on the object level. De nition 8 (Simulator Axioms for Total Predicates) According to De nition 7 we call the two axioms SimR = 8ui; v R(: : : ; ui; : : : ; v) ) 9f : FR f (: : :; ui; : : :) = v 1 SimR = 8ui8f : FR R(: : : ; ui; : : : ; f (: : : ; ui; : : :)) 2 the simulator axioms for the total predicate R. Note that in the case of non-total predicates the de nition of SimR needs to be changed because in this case we have 2 to be able to deal with partial functions instead of total functions. The collection of all axioms SimR, respectively SimR, is called Sim1, respectively Sim2. 1 2 Thus, for any total (serial) accessibility relation or role we can introduce functional simulators. This allows the following approach for the translation of knowledge bases into rst-order predicate logic. First, we transform all concepts and roles which occur in a given knowledge base into negation normal form, i.e. in a form where all negation signs occur solely in front of the primitive concepts. Now we translate the terminological and assertional sentences into rst-order logic formulae using the function ]]. Axiom

2(m;a)M2 : : :Mn 3(m;a)M2 : : : Mn C1 v C2 ]]U R1 v R2 ]]U a 2 A ]]U (a; b) 2 P ]]U

Translation ]]U 8V : <a (U; V ) ) M2 : : : Mn ]]V m ]]U 9V : F<a M2 : : :Mn ]]V (U ) m 8 X : C1 ]]U;X ) C2 ]]U;X 8 X; Y : R1 ]]U;(X;Y ) ) R2 ]]U;(X;Y ) A ]]U;a P ]]U;(a;b)

where the translation of concepts and roles is de ned by:

Term Translation A1 ]]U;X A1(U; X ) :A1 ]]U;X :A1(U; X ) C1 u : : : u Ck ]]U;X C1 ]]U;X ^ : : : ^ Ck ]]U;X 9 R:C ]]U;X 9Y : FR C ]]U;Y (X ) 3(m;a) C ]]U;X 9V : F<a C ]]V (U );X m P ]]U;(X;Y ) P (U; X; Y ) R1 u : : : u Rl ]]U;(X;Y ) R1 ]]U;(X;Y ) ^ : : : ^ Rl ]]U;(X;Y ) R?1 ]]U;(X;Y ) R ]]U;(Y;X ) R C ]]U;(X;Y ) R ]]U;(X;Y ) ^ C ]]U;Y 2(m;a) R ]]U;(X;Y ) 8V : <a (U; V ) ) R ]]V;(X;Y ) m 3(m;a) R ]]U;(X;Y ) 9V : F<a R ]]V (U );(X;Y ) m Thus, given any Mod-ALC -formula , the result of the above translation, ]] is a rst-order predicate logic formula which can easily be transformed into clause normal form with the help of the well-known standard techniques. Note that the clause form of such a translation does not contain any positive occurrence of a role or accessibility relation symbol. This fact can be exploited in a very interesting manner. Since any role or accessibility relation symbol can only occur in the additional axioms we can examine these independently from the translated formula. Nonnengart9 presents extremely good simpli cations for various modal logics. So, for instance, the whole theory for the modal logic KD45 can be simpli ed to the almost trivial unit clause R(U; V (W )). In the following theorem we suppose that we have some simpli cation Sim which can be applied to a set R of formulae expressing the properties of the accessibility relation such that R fSim2g j= ]] i Sim(R) fSim2g j= ]] Theorem 3.1 Let be a Mod-ALC sentence and T a set of Mod-ALC sentences. Let R be a set of formulae which express the properties of the underlying accessibility relation. Then T j=R S i ]] Sim(R) fSim2g j= ]] 2T i ]] is provable from S 2T ]] Sim(R) fSim2g using some theorem prover which is correct and complete for rst-order logic with equality. We presented an approach which allows to reason within modal terminological logics by utilizing an appropriate translation technique into rst-order predicate logic. The main idea behind this method is the functional simulation of accessibility relations and roles by suitable sets of functions. This turns out to have two main advantages: it decreases the size and the number of clauses and it allows signi cant simpli cations on the set of theory clauses.

4 Conclusion and Further Work

Until now, we have only worked out the optimization for those modalities which have a simple possible world semantics. If the interaction of multiple modalities requires the more complex neighbourhood semantics, we have to rely on the straightforward translation which will result in a rather large number of clauses. Looking for optimizations for this case is part of future work. 1. F. Baader and B. Hollunder, KRIS : Knowledge Representation and Inference System | System Description |. Technical Memo DFKI-TM-90-03 (Deutsches Forschungszentrum fur Kunstliche Intelligenz, Saarbrucken, 1990). 2. R. J. Brachman, V. P. Gilbert, and H. J. Levesque, An Essential Hybrid Reasoning System: Knowledge and Symbol Level Accounts of krypton. In Proceedings of the Ninth IJCAI, pp. 532{539. 3. R. J. Brachman and J. G. Schmolze, An Overview of the klone Knowledge Representation System. Cognitive Science 9 2 (1985), pp. 171{216. 4. F. M. Donini, M. Lenzerini, D. Nardi, A. Schaerf, and W. Nutt, Adding Epistemic Operators to Concept Languages. In Proceedings of the KR'92, eds. B. Nebel, C. Rich, and W. Swartout (Morgan Kaufmann, 1992), pp. 342{353. 5. B. Hollunder and W. Nutt, Subsumption Algorithms for Concept Languages. Research Report DFKI-RR-90-04 (Deutsches Forschungszentrum fur Kunstliche Intelligenz, Saarbrucken, 1990). 6. U. Hustadt, A. Nonnengart, R. Schmidt, and J. Timm, MOTEL User Manual. Internal report MPI-I-92-236 (Max-Planck-Institute for Computer Science, Saarbrucken, 1992). 7. A. Kobsa, Towards Inferences in BGP-MS: Combining Modal Logic and Partition Hierarchies for User Modeling (Preliminary Report). In Proceedings of the Third International Workshop on User Modeling (1992). 8. R. C. Moore, Autoepistemic Logic. In Non-Standard Logics for Automated Reasoning, eds. Ph. Smets, E. H. Mamdani, D. Dubois, and H. Prade (Academic Press, London, 1988) 9. A. Nonnengart, First-Order Modal Logic Theorem Proving and Standard PROLOG. Internal report MPI-I-92-228 (Max-Planck-Institute for Computer Science, Saarbrucken, 1992). 10. H. J. Ohlbach, A Resolution Calculus for Modal Logics. PhD thesis (Universitat Kaiserslautern, 1988). 11. N. Rescher and A. Urquhart, Temporal Logic (Springer, Berlin, 1971). 12. J. G. Schmolze, The Language and Semantics of nikl. Technical Report 89{4 (Department of Computer Science, Tufts University, Medford, MA, 1989).

References

All rights reserved Powered by 福彩号码查询 福彩号码查询 www.edasl.tw

copyright ©right 2010-2021。

文档资料库内容来自网络，如有侵犯请联系客服。[email protected]

copyright ©right 2010-2021。

文档资料库内容来自网络，如有侵犯请联系客服。[email protected]