论文部分内容阅读
木文从人工智能角度阐述了机器定理证明的重要意义,综述了以逻辑方法为重点的定理证明器的一般问题,如搜索策略、化简、语义、抽象、发现相关公理以及它涉及的一般软件工程问题。
机器定理证明中的一般问题
【摘 要】
：
木文从人工智能角度阐述了机器定理证明的重要意义,综述了以逻辑方法为重点的定理证明器的一般问题,如搜索策略、化简、语义、抽象、发现相关公理以及它涉及的一般软件工程问
【机 构】
：
国防科技大学计算机系,国防科技大学计算机系长沙410073,长沙410073
【出 处】
：
计算机科学
【发表日期】
：
1992年5期
【基金项目】
：
八六三计划软件生产自动化课题
其他文献
随着计算机应用的普及和推广,产生了对应用软件的巨大需求,如何开发应用软件系统,已成为解决当前“软件危机”的突出焦点。然而当前普遍采用的以瀑布模型为生存期的结构化分
本文介绍了以分布式知识库系统的大规模知识库管理和结论不一致为出发点的实验系统 DKBS/IDKE 的体系结构、主要功能、进程实现,通讯机制以及进一步要研究的问题。
面向对象数据库主要是用于 CAD/CAM,CASE 等工程设计领域,这些领域为了对多种方案进行比较选择,一般都需要有版本管理的支持。所以尽管文〔7〕中未将版本管理列为面向对象数据库必备的特性,在许多系统,例如:ORION,Iris,02和 ODE 等都具有这种功能。尤其近年来国际、国内关于版本管理方面的工作很多涉及到CAD/CAM,CASE,DB 等诸多领域,使得版本管理逐渐成为一个非常重要的问题
1989年初,《中国科技论文统计与分析》课题组受国家科委委托,开始直接利用我国出版的中文科技期刊作为数据源,对我国科技论文发表情况进行较大规模的统计与分析。下面按字序
八十年代中期,数据库技术和人工智能、辑逻程序设计技术的结合导致了一个新的领域——知识库(演绎数据库)的诞生。为了有效地实现知识库,必须有效地处理由逻辑规则表示的查询
重写技术是处理等式理论的一种有效方法,它已成功地应用到带等词的一阶谓词逻辑中定理的自动证明。本文介绍基于重写的定理证明方法的基本思想,以及几种具体的证明技术,最后
nH-PROLOG,SPRF和N-PROLOG是PROLOG的三种典型扩充，本文介绍了它们之间的异同。这三个系统采用不同方法扩充了PROLOG，但是均使用情况分析法做为非Horn推理机制。尽管它们的出发
七、C-POREL 的编译子系统 NUA和 NOAC-POREL 的用户接口语言是 RDBL,即关系数据库语言的缩写,是一种类 SQL 语言。简言之它包含了 SQL 的功能且格式也类似。RDBL 的编译分为
人工智能与数据库技术是计算机科学的两大重要领域，越来越多的研究成果表明，这两种技术的相互渗透将会给计算机应用带来更广阔的前景，本文简要讨论了人工智能与数据库技术结合的
风力发电机组与中压电网连接，中压电网通常连接有其它波动性负荷，在被测风力发电机组输出端可能引起显著的电压波动，电网特性决定了风力发电机组产生电压波动的程度。为了避免电