一种用于基于知识系统开发的形式化模型*

LKo是一个将面向对象和逻辑范型相结合，用于基于知识系统的形式化开发模型，其中逻辑对象是集状态、约束、行为、继承于一体的抽象实体．它支持框架、规则、语义网络、黑板等多种知识表示，因而可用来形式地描述基于知识系统的需求规范．在知识获取过程中通过对形式规范反复地修改、验证及确认而形成软件原型．     

公平转换系统规范及其应用*

本文讨论了用于并发系统规范的2种方法；时序逻辑方法和状态自动机方法．由此，本文提出了一种新的规范形式——公平转换系统规范FTSS(fair transition system specification)．此规范方法集成了状态自动机方法和时序逻辑方法的优点，改进了时序逻辑方法通常较复杂、不易理解，特别是它不能用于描述并发系统的局部性质等不足．进一步对FTSS中的每一部分进行了讨论，得到结论；FTSS是机器封闭的，规范过程是相容的且是完全的．一个有丢失传输协议的例子表明作者的方法具有简单、直观、易于理解和便于使用等特点．最后给出了FTSS的一些应用．它为程序验证和并发系统的逐步求精提供了一个统一的框架，已成功地应用于程序验证中．     

多智体系统时态认知规范的模型检测算法

模型检测技术一直以来主要是检验用时态逻辑描述的规范,人们很少注意认知逻辑的模型检测问题,而在分布式系统领域,系统和协议的规范已广泛地采用知识逻辑来描述.着重研讨了时态认知逻辑的模型检测算法.在SMV(symbolic model verifier)模型检测器的基础上,根据知识的语义和集合理论,提出了多种检验知识和公共知识的算法,从而使SMV的检测功能由时态逻辑扩充到时态认知逻辑.这些方法也适用于其他以状态集合作为输出的模型检测方法和工具的功能扩充.     

公平转移系统规范及其应用

本文讨论了用于并发系统规范的２种方法：时序逻辑方法和状态自动机方法，由此，本文提出了一析的规范形式－－公平转换系统规范ＦＴＳＳ（ｆａｉｒ ｔｒａｎｓｉｔｉｏｎ ｓｙｓｔｅｍ ｓｐｅｃｉｆｉｃａｔｉｏｎ），此规范方法集成了状态自动要方法和时序逻辑方法的优点，改进 时序逻辑方法通常较复杂，不易理解，特别唱它不能用于描述并发系统的局限性质等不足，进一步对ＦＴＳＳ中第一部分进行了讨论，是到结论，ＦＴＳＳ是     

基于Petri网的统一知识表示模型

本文讨论知识表示的Ｐｅｔｒｉ网模型。将多种知识分类表示，对于开发具有较宽领域知识的系统具有重要意义。本文从统一的观点出发，在给出了Ｐｅｔｒｉ网的代数规范说明后，将三种主要的知识表示方法分别与Ｐｅｔｒｉ网模型之间建立映射系统，这三种知识表示方法为：逻辑表示法，语义网络和产生式系统。     

多智能体系统时态认知规范高效符号模型检测的算法研究

Clarke和McMillan提出了利用mu演算和OBDDs符号模型检测时态逻辑的方法.这些方法是非常有效的,能用于验证许多具有极大状态空间的实际系统(状态个数可以超过1020).但是,这些方法不能检测知识逻辑.而时态认知逻辑能更精确地描述分布式领域中系统和协议的规范.文章首先讨论了Kripke结构和mu演算的扩展,然后提出了利用扩展mu演算和OBDDs符号模型检测时态认知逻辑的方法.     

多主体系统中对其它主体的研究

多主体系统是当前人工智能研究后一个热点，其中，关于知识和动作的推理是一个重要的课题，文中给出了一种知识表示框架，称为ＲＡＯ逻辑，用来对其它主体研究时表示概念和规则，我们从日常推理中抽象出换位原则的规则（ＰＥＰ），ＰＥＰ是ＲＡＯ是的一条公理模式，并且为主体研究其它主体的一个基本规则，它与知识逻辑中的分离规则和（Ｋ）公理具有相似的形式和作用。     

一个统一的程序验证框架

本文提出了一个简单的方法，其中程序和其性质都由一个逻辑：时序逻辑中的公式表示．文中给出了一个程序的转换模块的定义，提出了时序执行语义的概念．它是一个时序公式，精确地说明了一个程序．将时序逻辑作为规范语言，程序正确性就意味着说明程序的公式蕴含说明性质的公式，其中蕴含即为一般的逻辑蕴含．因此，本文的方法为并发程序的规范及验证提供了一个统一的框架．它允许充分利用现有的用于证明并发系统时序性质的各种完全证明系统．一个缓冲系统的简单例子用来说明本文的方法．此例子表明本文的方法是可行的.     

基于知识的肺癌早期细胞诊断系统

介绍了一个基于知识的肺癌早期细胞病理诊断系统，着重理讨论了该系统中的知识表示形式及与之相配合的基于确定性模式的不确定性方法。该系统能自动从细胞图象中提取出必需的特征事实，并模仿病理专家的诊断逻辑，自动揄出最终结果。     

逻辑—对象知识模型LOKM

知识模型是知识信息处理系统的重要基础,是建立知识系统的主导思想,提供知识表示和操作的形式构架。在近几年研究的基础上,我们提出了逻辑-对象知识模型LOKM。本文主要讨论该模型的知识结构和推理策略。     

状态图到PTL形式规范的转化

本文讨论从状态图到PTL形式规范的转化方法.状态图是描述系统行为的半形式化的图形工具,但缺少精确的形式语义,PTL(投影时序逻辑)是一种具有离散的时间模型的时序逻辑,把状态图转换到PTL后可以使其具有精确的形式语义并能使用形式化验证方法来证明状态图所描述的系统的一些重要性质是否得到满足,同时可把系统的形式描述转换为Tempura程序进行模拟,从而提高系统设计的可信性.     

确认程序规范的软件工具TC及其实现

引言由于软件费用不断上升,对软件质量要求越来越高。软件确认对于提高软件可靠性,保证软件质量是至关重要的。一个程序系統,经过设计、编码之后,该系统是否符合给定的规范,这就要求确认。确认的目的旨在论证程序代码符合程序规范。它是采用各种方式分析和测试来确定代码和规范符合程度。目前采用的确认方法,可以分为二类: 1.验证(verification)从逻辑意义上分析系统,确认系统正确性或查出逻辑错误。主要形式有解     

多智体系统时序认知规范的SPIN模型检测

SPIN模型检测器主要用来检测线性时序逻辑描述的规范,而多智体系统的规范采用时序认知逻辑描述比较方便。本文着重讨论了如何利用SPIN模型检测线性时序认知逻辑的方法,根据局部命题的理论,将模型检测知识算子和公共算子表述的规范规约为模型检测线性时序逻辑的问题,从而使SPIN的检测功能由线性时序逻辑扩充到线性时序认知逻辑。本文通过一个RPC协议分析实例来说明模型检测线性时序认知逻辑的方法。     

面向OWL知识的问答系统Agile

介绍了一个面向OWL知识的问答系统Agile,并重阐述了其在问题规范和知识索引方面的技术方案。为了得到合适的映射单位,Agile系统定义了两个数据结构用于规范问题和OWL本体知识字典,并借助自然语言处理工具和OWL解析工具将两种源知识进行了形式化。实验分析表明:与现有网络问答系统相比,Agile系统能够处理的问题领域和形式更加丰富。     

用语义概念简化知识库系统部件接口

现今,有许多人正在着手研制知识库系统(Knowledge base sys-tem.KBSs)的各个部件,如: (a)研制存贮大量简单事实的新硬件 (b))研制高速执行象PROLOG和LISP语言的机器 (c)设计自动维护语义完整性和演绎求解的算法 (d)适合于时间、可信度、非单值性推理和其他不能由古典真值函数谓词逻辑所实现的知识处理的逻辑系统 (e)研制支持以正规形式存贮知识的多用户视图的方法 (f)自然语言和知识库系统接口的研究己取得某些进展但由于许多原因,如各个部件中使用的不同术语和不同的知识表示形式等等,使这些部件的集成成为很大的问题。一个解决的方法是标识一个各部件可共同使用的语义概念集合并且用这个集合来表示各个部件所处理的知识类型。一个语义概念的例子是逻辑非(Not),某些知识表示,如古典逻辑中所用的知识表示能够处理逻辑非;而在一般的数据库中却不能表示逻辑非,在假定封闭域(Closed-world)的情况下逻辑非用省缺表示。应该选择一组可实用的而不是适合哲学上争论的语义概念。在这篇文章中我们将直观地定义一个概念集,并说明这个概念集在KBSs部件中如何应用。     

GAL的OLMC工作状态研究

可编程器件，尤其是通过阵列逻辑是一种可由用户编程组态赋于其一定逻辑功能的数字电路器件，通用阵列逻辑（GAL）中的核心电路是输出逻辑宏单元OLMC，它的各种各样组态形式的实现是由结构控制中的SYN，AC（0），AC1（n)来控制的，8个OLMC的不同组态形式就可构成不同的数学系统。     

基于标记Büchi自动机的时态描述逻辑ALC-LTL模型检测

时态描述逻辑将描述逻辑的刻画能力引入到命题时态逻辑中,适合于在语义Web环境下对相关系统的时态性质进行刻画.为了对这些时态性质进行高效的验证,在ALC-LTL的基础上研究了时态描述逻辑的模型检测问题.一方面,使用时态描述逻辑ALC-LTL公式来表示待验证的时态规范;另一方面,在对系统建模时借助描述逻辑ALC对领域知识进行刻画.针对上述扩展后得到的模型检测问题,提出了基于自动机的ALC-LTL模型检测算法.模型检测算法由3个阶段组成:首先将时态规范的否定形式和系统模型分别构造成标记büchi自动机;接下来构造这两个自动机的乘积自动机,并将关于ALC的推理机制融入到乘积自动机的构造过程中;最后对该乘积自动机进行判空检测.与LTL模型检测相比,时态描述逻辑ALC-LTL的模型检测引入了描述逻辑的刻画和推理机制,可以在语义Web环境下对语义Web服务等复杂系统的时态性质进行刻画和验证.     

智能计算中的热点问题

1 引言人工神经网络研究热潮的再度兴起有其客观的历史背景。50年代以来,以符号机制为代表的经典人工智能形式体系取得了巨大的成功.80年代,当人们对过去30年的成就与问题进行反思时,却不得不承认,智能系统如何从环境中自主学习的问题事实上并未很好地解决。从逻辑的角度讲,以演绎逻辑为基础的算法体系可以发现新的定理,却无法发现新的定律。换句话说,基于符号推理的经典人工智能形式体系在机器定理证明方面的成功和在规则提取方面的失败同属必然。事实上,早在50年代,那些热衷于研究知识发现内在逻辑的人们就已经隐约地意识到,归纳逻辑、尤其是不完全归纳逻辑是通往知识发现的合理途径。Rosenblatt[1957]提出了感知机     

混合投影时序逻辑与混合系统的形式化验证

为了描述混合系统的性质和行为，10多年来，各种时序逻辑，如Hybrid Temporal Logic等相继出现。这些时序逻辑适用于刻画混合系统的性质和规范，但不适宜表示描述系统的实现模型。本文定义了一个混合投影时序逻辑（Hybrid Projection Temporal Logic，简称HPTL），既能刻画混合系统的性质，又能表示混合系统的实现。这样，混合系统的验证就可以很方便地在统一的数学模型框架下进行。同时，给出了HPTL的基本的逻辑等价式系统和一个用HPTL进行混合系统验证的实例。     

基于数据库的燃煤锅炉事故诊断专家系统的设计与实现

采用MS SQL Server7．0设计知识库，Visual Basic 6．0编程实现了燃煤锅炉事故诊断专家系统。本系统知识表示采用了基于概率逻辑的产生式规则形式，并用数据库的方法存储管理知识库。推理机采用规则值的方法，并应用主观Bayes理论建立了不确定性推理模型。实现了一种较为理想的不精确推理。