描述逻辑εLU概念及术语公理集的表达能力刻画

表达能力和推理复杂性是一个逻辑的两个重要特征,也是一对相互制约的关系.解释之间的互模拟关系是从语义的角度刻画逻辑表达能力的一个有效途径,其代表性的结果是命题模态逻辑表达能力的刻画定理——vanBenthem 刻画定理.给出了描述逻辑εLU（含构造子：原子概念、顶概念、概念交、概念并、完全存在约束）的模拟关系,建立了εLU中概念和术语公理集的表达能力刻画定理,即一阶逻辑公式与ELU中概念和术语公理集等价的充分必要条件.上述结果为寻求表达能力与推理复杂性之间的最佳平衡提供了有效的支持.     

描述逻辑εL循环术语集的混合推理

循环术语集是描述逻辑长期以来的研究难点,它最基本的问题即语义及推理问题没有得到合理的解决.分析了描述逻辑循环术语集的研究现状和存在的问题,在Baader和Brandt的基础上进一步研究了描述逻辑εL循环术语集的混合推理问题.给出了εL的混合循环知识库的语法和语义(包括不动点语义和描述语义).针对εL循环术语集混合推理的需要.提出了TBox-完全的概念,并重新定义了描述图(包括语法描述图和语义描述图).使用描述图之间的模拟关系和TBox-完全概念给出了最大不动点语义和描述语义下εL混合循环知识库的实例检测推理算法,证明了推理算法的正确性,并给出了推理算法的复杂性定理.     

描述逻辑FL0循环术语集的可满足性

循环术语集是描述逻辑长期以来的研究难点,它的最基本的问题即语义及推理问题没有得到合理的解决。分析了描述逻辑循环术语集的研究现状和存在的问题,基于图的互模拟的方法,给出了描述逻辑FL0循环术语集的可满足性条件。结果证明循环术语集的可满足性的推理是多项式复杂的。     

描述逻辑FL-循环术语集的语义及推理

循环术语集是描述逻辑长期以来的研究难点,它的最基本的问题即语义及推理问题没有得到合理的解决.文中分析了描述逻辑循环术语集的研究现状和存在的问题,在Baader的基础上进一步研究了描述逻辑FL~-循环术语集的语义及推理问题.给出了FL~-循环术语集的语法、语义和不动点模型的构造方法.针对FL~-循环术语集的需要,提出了一种新的有限自动机,使用有限自动机给出了不动点语义和描述语义下FL~-循环术语集的可满足性和包含推理算法,证明了推理算法的正确性,并给出了推理算法的复杂性定理.     

带RVM的描述逻辑εL混合循环术语集的语义及推理

分析描述逻辑循环术语集的研究现状和存在的问题,在F.Baader和S.Brandt的基础上进一步研究带RVM的描述逻辑εL混合循环术语集的语义及推理问题.给出带RVM的εL混合循环术语集的语法和语义.针对带RVM的εL混合循环术语集包含推理的需要,提出TBox-完全的概念,并重新定义描述图,使用描述图之间的模拟关系和TBox-完全给出最大不动点语义和描述语义下带RVM的εL混合循环术语集的概念包含推理算法,证明推理算法的正确性,并证明推理算法是多项式时间复杂的.     

基于扩展模糊描述逻辑的软件数值模型

表示复杂的数值关系是软件建模的难点:直接表示复杂的数值关系会导致极高的软件模型推理复杂性。提 出采用模糊函数近似表示复杂数值关系,然后将扩展模糊描述逻辑作为软件模型形式化基础的软件模型建模框架,该 框架包含3个核心问题:软件数值域模糊化、软件数值知识库构造和软件数值模型推理。在软件数值域模糊化方面提 出模糊化方法和保证充分性的近似原则;在软件数值知识库构造方面讨论在模糊概念的基础上生成截集概念、构造声 明和术语公理的步骤和过程;在软件数值模型推理方面研究算法设计优化和分割等算法实现机制。     

描述逻辑εLN 循环术语集的不动点语义及推理

循环术语集是描述逻辑长期以来的研究难点,其最基本的问题即语义及推理问题没有得到合理的解决.分析了描述逻辑循环术语集的研究现状和存在的问题,将Baader 的工作扩展到新的方向.针对更大的描述逻辑系统研究了循环术语集的语义及推理机制,即在描述逻辑εL 的基础上添加数量约束构造算子,提出了描述逻辑εLN,给出了εLN 的语义(包括不动点语义和描述语义).针对εLN 的需要,重新定义了描述图(包括语法描述图和语义描述图).使用描述图之间的模拟关系给出了不动点语义下εLN 循环术语集的可满足性和包含关系推理算法,并证明了推理算法是多项式时间复杂的.     

描述逻辑μALCQO 的语义及推理

循环术语集是描述逻辑长期以来的研究难点,其最基本的问题即语义及推理问题没有得到合理的解决.基于混合分级μ-演算将不动点构造算子引入到含有枚举构造算子的描述逻辑ALCQO 中,提出了一种允许包含循环术语集的描述逻辑μALCQO.给出了μALCQO 的语法、语义和不动点构造算子的性质,证明了μALCQO 的可满足性推理等价于混合分级μ-演算的可满足性推理.基于混合分级μ-演算可满足性推理算法,并利用完全强化自动机给出了μALCQO的可满足性推理算法,以及给出了推理算法正确性证明和复杂性定理.μALCQO为进一步给出同时含有不动点构造算子和枚举构造算子的表达能力强的描述逻辑推理算法提供了理论基础.     

F-SHIQ公理体系及其OWL扩展

随着计算机和Internet的快速发展,语义网和描述逻辑在人工智能等领域扮演着越来越重要的角色。但在日常生活中,越来越多不确定的、不完整的知识需要解决,而现存的OWL只能表述确定的完整的概念和关系。为了能够表示和推理模糊知识,给出了一个基于描述逻辑SHIQ的全新的模糊描述逻辑公理体系——F-SHIQ公理体系,并以此公理体系为基础,扩展了OWL本体语言,能够描述和推理模糊知识。该文首先给出了系统详细的定义、公理、定理以及定理的证明;然后详述了如何用FSRL,即基于F-SHIQ的OWL扩展,来表示和推理模糊信息;最后通过一个例子来检验扩展语言的应用效果。     

描述逻辑μALCIO的语义及推理

循环术语集是描述逻辑长期以来的研究难点,它的最基本的问题即语义及推理问题没有得到合理的解决.分析了描述逻辑循环术语集的研究现状和存在的问题,基于混合μ-演算将不动点构造算子引入到含有枚举构造算子的描述逻辑ALCIO中,提出了一种允许包含循环术语集的描述逻辑μALCIO.给出了μALCIO的语法和语义,证明了μALCIO的可满足性推理等价于混合μ-演算的可满足性推理,并利用树自动机理论给出了μALCIO的可满足性推理算法以及给出了推理算法正确性证明和复杂性定理.     

Expressiveness and complexity of graph logic

We investigate the complexity and expressive power of a spatial logic for reasoning about graphs. This logic was previously introduced by Cardelli, Gardner and Ghelli, and provides the simplest setting in which to explore such results for spatial logics. We study several forms of the logic: the logic with and without recursion, and with either an exponential or a linear version of the basic composition operator. We study the combined complexity and the expressive power of the four combinations. We prove that, without recursion, the linear and exponential versions of the logic correspond to significant fragments of first-order (FO) and monadic second-order (MSO) Logics; the two versions are actually equivalent to FO and MSO on graphs representing strings. However, when the two versions are enriched with μ-style recursion, their expressive power is sharply increased.Both are able to express PSPACE-complete problems, although their combined complexity and data complexity still belong to PSPACE.     

A Branching Time Temporal Framework for Quantitative Reasoning

Temporal logics such as Computation Tree Logic (CTL) and Linear Temporal Logic (LTL) have become popular for specifying temporal properties over a wide variety of planning and verification problems. In this paper we work towards building a generalized framework for automated reasoning based on temporal logics. We present a powerful extension of CTL with first-order quantification over the set of reachable states for reasoning about extremal properties of weighted labeled transition systems in general. The proposed logic, which we call Weighted Quantified Computation Tree Logic (WQCTL), captures the essential elements common to the domain of planning and verification problems and can thereby be used as an effective specification language in both domains. We show that in spite of the rich, expressive power of the logic, we are able to evaluate WQCTL formulas in time polynomial in the size of the state space times the length of the formula. Wepresent experimental results on the WQCTL verifier.     

Query Answering for OWL-DL with rules

Both OWL-DL and function-free Horn rules are decidable fragments of first-order logic with interesting, yet orthogonal expressive power. A combination of OWL-DL and rules is desirable for the Semantic Web; however, it might easily lead to the undecidability of interesting reasoning problems. Here, we present a decidable such combination where rules are required to be DL-safe: each variable in the rule is required to occur in a non-DL-atom in the rule body. We discuss the expressive power of such a combination and present an algorithm for query answering in the related logic extended with DL-safe rules, based on a reduction to disjunctive programs.     

Converting untyped formulas to typed ones

We observe that every first-order logic formula over the untyped version of some many-sorted vocabulary is equivalent to a union of many-sorted formulas over that vocabulary. This result has as direct corollary a theorem by Hull and Su on the expressive power of active-domain quantification in the relational calculus. Received: 1 April 1998     

A Guarded Fragment for Abstract State Machines

Abstract State Machines (ASMs) provide a formal method for transparent design and specification of complex dynamic systems. They combine advantages of informal and formal methods. Applications of this method motivate a number of computability and decidability problems connected to ASMs. Such problems result for example from the area of verifying properties of ASMs. Their high expressive power leads rather directly to undecidability respectively uncomputability results for most interesting problems in the case of unrestricted ASMs. Consequently, it is rather natural to ask whether there exist expressive classes of ASMs for which we can prove positive decidability and computability results. In this work, we introduce such a class of ASMs. The concept is similar to the one of the guarded fragment of first-order logic. We analyze the expressive power of this class and prove that it is stronger than Datalog LITE and the guarded fragment of first-order fixed point logic. Some decidability and computability results have been proven in earlier works.     

强表达描述逻辑本体的后继式公理定位研究

公理定位能够挖掘描述逻辑中可解释的缺陷,并为逻辑蕴含结果寻找隐藏的理由,因此在描述逻辑研究中引起了广泛的关注.平衡描述逻辑表达能力和推理机求解效率问题一直是公理定位研究的重点内容.本文基于一种后继式判定算法,从白盒和黑盒两个角度将其用于公理定位.白盒方法利用修正的后继式规则（即定位规则）来追踪推理的具体过程,并引入定位公式的概念建立子句的布尔公式标签与逻辑蕴含的所有极小公理集之间的对应关系.黑盒方法则直接调用基于未修正的后继式规则的推理机,并进一步利用碰集树方法求得逻辑蕴含的所有理由.最后,基于这样的两种面向强表达描述逻辑本体的公理定位算法设计推理工具,从理论和实验两方面验证其可行性,并与已有的推理工具比较求解性能.