【作者】 于洋；

【导师】 陈火旺； 王戟；

【作者基本信息】 国防科学技术大学 ， 计算机科学与技术， 2007， 博士

【摘要】 使用计算机解决应用问题的一般过程可以概括为:对于某个给定领域和目标,应用某种语言为该问题建立可计算的模型。这个过程主要涉及本体论、语言(逻辑)和计算三个领域的理论和技术,其中本体论是核心与起点。本文的工作涉及上述三个方面。一、本体论方面的工作基于对部分整体关系(partof)的分析,提出了整体结构。partof关系因具有特殊的语义以及在本体论中的重要地位而广受关注。本文讨论并分析了使用partof来表示整体的局限性、困难性和复杂性,指出问题的关键所在是没能体现partof的特殊语义。分析表明,partof是in关系的子关系,其特殊语义与本体依赖和整体性有本质的联系。这种特殊语义不能被当前的表示语言以直观的方式来体现和刻画。为克服这一问题引入了整体结构构造,该构造具有很强的本体能力。通过它,整体被表示成结构化的实体,由一系列内在事物按照某种完整性约束组合而成。partof和in关系的特殊语义可以通过整体结构与其内部事物之间的关系来体现。由于整体结构具有天然的模块化性质和局部化语义,因此可以使得知识表示更加自然和简洁。基于整体结构,提出了一种非常一般的角色模型。角色是另一个受到广泛关注的概念,它对于整体结构的定义也是至关重要的。相关研究表明,角色的表示及其语义与对象和上下文有着密切关系。要形式化角色,必须首先形式化上下文。整体结构本质上是上下文,基于它,提出了一个新的角色模型:角色是不同于对象(类)的类型,二者之间必须通过play关系联系;角色总是整体结构的内部事物,其扮演者(对象)必须位于整体结构外部;角色实例存在依赖于扮演者和上下文。该模型为角色概念提供了统一的表示形式,能够体现当前关于角色的几乎所有特征。基于哲学本体论框架,提出了本体论元建模体系结构(OMMA)。在哲学界,本体论至少涉及三个主要组成部分:一组基本范畴的列表、基本范畴的性质以及相互间的关系、用于解释基本范畴的形而上学。三级实例化结构和Peirce三分法以非常抽象的方式体现了这个框架的基本原理。基于它们,提出了OMMA和存在的一般表示模式:后者指明前者在每个级别上的核心任务是通过整体结构建立事物间的依赖关系。OMMA的核心观点是赋予(同一级别事物间的)in关系和(相邻级别事物间的)实例化关系以相同的基础性地位。其可以作为构建形式理论、定义元语言和本体描述语言的指导原则。二、形式化本体描述语言方面的工作基于OMMA,提出了一个新的本体描述语言,可将它视为传统逻辑语言的整体结构扩展。该语言将整体结构看作是基本的语法成分,因此无论是语法上还是语义上都发生了重要改变。语法方面,除了整体结构外,还要求在引用内部事物时,必须明确的指出其所在的整体结构,称这样的概念(实例)为具体概念(实例)。语义方面,单纯的集合论对于整体性和本体依赖的语义解释是不够的。为此,提出了一种新的形式理论,其在集合论的基础上增加了in关系和内涵结构。基于该语言,形式定义了基本范畴之间的本体依赖关系,刻画了Is-A和play等重要关系的性质和约束。特别是,形式地刻画了角色的基本性质和特征。另外,根据对角色实例的两种不同观点,给出了本体描述语言的两种语义解释。将该语言应用于UML静态结构的形式化表示。UML的某些表示不够严格,不能将其直接转化为本文提出的形式化语言表示,因此应首先规范UML静态建模元素的表示。为此,根据本文提出的本体元建模体系结构,提出了一个UML表示的新框架,形式定义了UML的几个基本构造。符合相关约束的UML表示可以直接地转化为本文提出的本体描述语言。另外,该框架的一个副产品是不同视角的模型可以被融合在一起。三、可判定描述逻辑方面的工作描述逻辑(DLs)是当前知识表示特别是本体描述的最为重要的形式体系之一,其强调概念间的包含关系以及描述语言的可判定性。本文用整体结构来扩展描述逻辑,得到表达能力更强同时可判定的描述语言。这个结果主要源于整体结构具有特殊的模型论性质。首先,讨论了描述逻辑的两种关系约束扩展。第一个采用整体结构来表示关系。由于整体结构具有天然的模块性,与同一个关系有关的约束可以被紧凑地组织在一起。这样,多元关系就能以非常自然的方式表达出来,推理效率也会得到提高。第二个用关系的无环约束和有限链约束来扩展DLs。这个扩展可以给出有向无环关系和良建性质的基本约束。两种扩展都是可判定的。基于整数规划分别系统地提出了有和无基数约束(又称CBox)DLs的有限模型推理算法(FMRA)。FMRA对于整体结构的可满足性至关重要。指出无基数约束描述逻辑的FMRA的主要困难所在,提出了受限子类型概念作为对策。基于这一概念,给出了不同DL的FMRA。这些算法与己提出的算法相比更加简单和实用。进一步,证明了基本描述逻辑ALC关于CBox推理是非确定指数完全的。这说明DLs关于CBox推理是一致地困难。讨论了有和无基数约束描述逻辑在FMRA上的关键不同点,为具有基数约束的描述逻辑提出了实用的FMRA。这些算法填补了DLs在FMRA方面的一个空白。最后,提出了描述逻辑的整体结构扩展并给出了推理算法。该算法本质上是无限制模型的场景算法与FMRA的混合,其中,FMRA主要处理整体结构的内部可满足性问题。证明了该扩展的可判定性,展示了该扩展的表达能力。本文的主要贡献可以概括为:一个好的本体论基础对形式理论以及描述语言都有重大影响,而后者又进一步影响了寻找表达能力更强且可判定的受限语言的可能性。本文的研究在本体论、本体描述语言和可判定性语言方面均有所突破。希望本文的工作有助于构建一个更加强大的理论基础,也希望其能为诸如软件工程等领域提供一个更加自然、简单和强大的形式化语言支持。更多还原

【Abstract】 The process applying computer to solve an application problem can be summarized as using language and Ontology to build computable models of the domain for certain purpose. This process involves at least three main fields, namely, Ontology, logic and computation. Among them, Ontology is the kernel and start point. The work of this thesis is divided into three parts according to the three fields.1 The work related to OntologyBased on the detailed discussion and analysis on Part-Whole relationship (partof), this thesis presents the construct named whole structure. Part-Whole relation has caused considerable attention due to its special semantics and important status in Ontology. Firstly, it is shown that the representation of whole with partof is a rather complex, difficult and error-prone task. The main reason is that the special semantics of partof is ignored in these representations. Based on the deep analysis, it is revealed that partof is the specialization of in relation and its special semantics lies in ontological dependence and unity. Further, it is pointed out that this special semantics can not be captured by the current formal languages in a natural way. To overcome this problem, whole structure, a construct with very strong ontology power, is introduced. By it, a whole is represented as a structured thing which is comprised of some internal things. In this kind of representations, the special semantics of partof and in relation can be directly expressed by whole structure and its internal things. Because the whole structure possesses inherent modularity and local semantics, the representation is very natural and simple.Based on the whole structure, a general role model is given. Role is another notion received considerable attention. Furthermore, roles are crucial to the representation of wholes. The related work has shown that role is a very important and fundamental notion and its semantics is tied up with object and context. To formalize the role, we should formalize the context first. Because the whole structure is essentially a formal construct corresponding to context, it can be used to formalize the primary characteristics of roles. The result is a novel role model. In this model, roles are explicitly distinguished from objects but always played by objects; roles are always internal to some whole structure; roles are existentially dependent on their players and contexts they reside in. This model is very simple and general to capture almost all characteristics of roles. Based on the research of Ontology in philosophy, an ontological metamodeling architecture (OMMA) is proposed. In philosophy, Ontology consists of at least three main parts: a list of basic categories, the properties of these categories and the basic relations between them, a metaphysics framework for explaining these categories. There are also two principles, i.e., the three levels instantiation structure and Peirce’s trichotomy reflect some basic ideas underpinning Ontology. Base on these principles, this thesis present OMMA and a general pattern for representing being. This pattern reveals that the main task in the each level of OMMA is to construct the dependence relations among being by whole structure. This architecture serves as the foundation for defining formal theory, ontology language and metalanguage in this thesis.2 The work related to logic languageBased on OMMA, a novel ontology language is presented which can be viewed as the extension of the traditional language with whole structure.In this language, whole structure is an inherent syntax element, and thus the syntax and semantics are both changed greatly. In syntax, it is regulated that when referring internal elements they must be accompanied with their whole structure (context). This kind of concepts (instances) are called concrete concepts (instances). In semantics, set theory alone is not enough. A new formal theory is proposed by extending set theory with in relation and intension structure. In other words, in relation is endowed with the same fundamental status as instantiation.With this language, several important relations such as Is-A, play and ontological dependence are formally defined. Especially, roles are also formally characterized. Further, two kinds of semantics are proposed based on two different views on role instances.This language is applied to the formalization of UML static diagrams. The representation with UML is not strict enough to gain its formal semantics based on the presented language. So, the primary task is to give formal specifications to the main UML modeling elements. For this, a new framework for formalizing UML static diagrams is presented and it can be viewed as a specialization of the proposed OMMA. Further, several basic constructs of UML are formally defined within this framework. Base on them, the representation of UML becomes more strick and they can be easily transformed into the language presented in this thesis. Furthermore, the separated models for modeling different aspects can be fused together in an inherent way. 3 The work related to the extension of Description Logics with whole structureDescription Logics (DLs) are one of the most important knowledge representation formalism. They emphasize on the inclusion relation between concepts and provide sound and complete reasoning services for key reasoning problems. The main work in this part is to present a decidable and more power language by extending DLs with whole structure. This result is attributed to the properties of the model theory resulted from whole structure.Two decidable extensions of DLs with relation restrictions in different ways are given. The first one adopts whole structure to represent relations. Because of the inherent modularity of whole structure, the restrictions related to the same relation can be compactly organized together. By this, n-arity relations can be represented in a natural way and the efficiency of reasoning algorithm can also be improved. The other one extends DLs with acyclic and finite chain relation restrictions, which can capture the constraints of directed acyclic relations and well-founded property. Both of the two extentions are decidable.The second contribution of this part is to establish the finite model reasoning algorithms (FMRA) of DLs with or without cardinality restrictions (called CBox also) respectively based on integer programming. The finite model restriction is crucial to the satisfiability of concepts with whole structure.Based on the detailed analysis, the main difficulty in the FMRA of DLs without cardinality restrictions is pointed out. To tackle it, the notion of qualified subtype is introduced. With this notion, several FMRA in different DLs are presented. They are more simple and practical than the ones proposed in the related work. For the FMRA of DLs with CBox, the analysis of their computation complexities reveals that the reasoning in the basic description logic ALC w.r.t. CBox is NExpTime-complete. This means that the reasoning in DLs w.r.t. CBox is commonly difficult. Further, the key difference on FMRAs between the DLs with CBox and the ones without CBox is analyzed. Several practical algorithms with tight upper bound complexity for the DLs with CBox are presented. To the best of my knowledge, this is the first practical finite model decision procedure for DLs with CBox.At last, this thesis presents a formal language by extending the DL ALCIQ with whole structure. Its sound and complete algorithm is also given. Essentially, this algorithm is a hybrid of tableau algorithm with FMRA where the later is used to decide the satisfiability of whole structure. It is shown that this language can significantly improve the expressivity of DLs.The main contribution of this thesis can be summarized as a good ontology base has great influence on the formal theory and languages, and the later further impact the com-putability of their restricted sublanguages. Several creative contributions are made among three main fields. It is hoped that the results of this thesis can help the establishment of the more powerful foundation, and can also help to provide the more nature, simple and powerful languages for other fields such as software engineering.更多还原