论文部分内容阅读
重写技术是处理等式理论的一种有效方法,它已成功地应用到带等词的一阶谓词逻辑中定理的自动证明。本文介绍基于重写的定理证明方法的基本思想,以及几种具体的证明技术,最后将这类方法与经典的归结证明方法加以比较。
基于重写技术的自动定理证明
【摘 要】
：
重写技术是处理等式理论的一种有效方法,它已成功地应用到带等词的一阶谓词逻辑中定理的自动证明。本文介绍基于重写的定理证明方法的基本思想,以及几种具体的证明技术,最后
【机 构】
：
中国科学院软件研究所北京100080
【出 处】
：
计算机科学
【发表日期】
：
1992年2期
【基金项目】
：
八六三计划资助
其他文献
本文提出了分布式知识库系统中设计知识库和推理机的一些基本思想,并通过介绍实验系统 DKBS/IDKE 中知识处理的方法,对有关的知识表示、存储、管理、编译和推理等问题做了探
一、引言知识库和演绎数据库是近几年数据库界研究的热门课题,其研究正方兴未艾。八十年代中期,LDL 语言和 DATALOG 语言的推出标志着一个研究热潮的到来。从1990年召开的几
<正>一、分析的挑战系统分析既使人振奋也使人沮丧,在所有类型的项目中有三个主要的难题困扰着系统分析员。即：问题空间的理解、人之间的沟通,以及需求不断变化。
在分布式知识库系统中,由于知识的来源不同,求解策略的差异,利用多个知识库协作求解时产生的一个主要问题是:当参与协作求解的各个专家对同一问题得出不同的求解结果时,应如
随着计算机应用的普及和推广,产生了对应用软件的巨大需求,如何开发应用软件系统,已成为解决当前“软件危机”的突出焦点。然而当前普遍采用的以瀑布模型为生存期的结构化分
本文介绍了以分布式知识库系统的大规模知识库管理和结论不一致为出发点的实验系统 DKBS/IDKE 的体系结构、主要功能、进程实现,通讯机制以及进一步要研究的问题。
面向对象数据库主要是用于 CAD/CAM,CASE 等工程设计领域,这些领域为了对多种方案进行比较选择,一般都需要有版本管理的支持。所以尽管文〔7〕中未将版本管理列为面向对象数据库必备的特性,在许多系统,例如:ORION,Iris,02和 ODE 等都具有这种功能。尤其近年来国际、国内关于版本管理方面的工作很多涉及到CAD/CAM,CASE,DB 等诸多领域,使得版本管理逐渐成为一个非常重要的问题
1989年初,《中国科技论文统计与分析》课题组受国家科委委托,开始直接利用我国出版的中文科技期刊作为数据源,对我国科技论文发表情况进行较大规模的统计与分析。下面按字序