检索结果-南通市图书馆

计算机科学 1993年第4期20卷 19-23页

作者：贲可荣陈火旺国防科技大学计算机系长沙410073

本文主要介绍近十年来定理证明器的发展情况,同时讨论了与自动定理证明相关的一些问题。

关键词：定理证明器自动定理证明

在线全文

学校读者我要写书评

暂无评论

自动定理证明中带有等词的连接法

应用科学学报 1994年第3期12卷 246-252页

作者：缪淮扣吴茂康上海科学技术大学

连接法是一种较新的自动定理证明的方法．该文讨论了带有等词的连接法，给出了形式化的定义，证明了带有等词的逻辑公式是ｅｑ有效的当且仅当它有互补复合例的规范矩阵的定理，并设计了带有等词的连接法的有关算法．

关键词：自动定理证明连接法等词

自动定理证明中RUE-NRF单元输入和锁的演绎

在线全文

学校读者我要写书评

暂无评论

吉林大学自然科学学报 1989年第2期 60-66页

作者：刘叙华欧阳继红吉林大学计算机科学系

本文在RUE-NRF推理规则的基础上,定义了RUE-NRF输入归结、RUE-NRF单元归结及RUE-NRF锁归结的概念,证明了RUE-NRF输入反驳与RUE-NRF单元反驳的关系,以及RUE-NRF锁反驳的完备性。

关键词：自动定理证明 RUEE-NRF单元锁归结

在线全文

学校读者我要写书评

暂无评论

支持用户自定义谓词的自动定理证明的研究

小型微型计算机系统 2013年第8期34卷 1781-1786页

作者：汪娟李兆鹏陈意云中国科学技术大学计算机科学与技术学院合肥230026 中国科学技术大学苏州研究院软件安全实验室江苏苏州215123

在先前设计的一个出具证明编译器原型基础上,增加了可用来描述数据结构性质的自定义谓词,对断言语言表达能力方面做了提升.在出具证明编译器的框架内,借助自动定理证明技术,针对自定义谓词的特点,设计了专门的推理规则,由此实现自定义... 详细信息

在先前设计的一个出具证明编译器原型基础上,增加了可用来描述数据结构性质的自定义谓词,对断言语言表达能力方面做了提升.在出具证明编译器的框架内,借助自动定理证明技术,针对自定义谓词的特点,设计了专门的推理规则,由此实现自定义谓词专用的自动定理证明器原型,并将它并入系统原来的自动定理证明器中.该原型可以用来证明操作单链表、二叉树等共享数据结构的程序的性质,其程序规范中可以使用自定义谓词描述数据有序性、链表长度等性质.

关键词：出具证明编译器自定义谓词自动定理证明推理规则

在线全文

学校读者我要写书评

暂无评论

基于重写技术的自动定理证明

计算机科学 1992年第2期19卷 79-80,24页

作者：张健中国科学院软件研究所北京100080

重写技术是处理等式理论的一种有效方法,它已成功地应用到带等词的一阶谓词逻辑中定理的自动证明。本文介绍基于重写的定理证明方法的基本思想,以及几种具体的证明技术,最后将这类方法与经典的归结证明方法加以比较。

关键词：重写技术自动定理证明

在线全文

学校读者我要写书评

暂无评论

自动定理证明中的一个通用证明法

上海大学学报（自然科学版） 1997年第3期3卷 283-288页

作者：吴茂康缪淮扣上海大学计算机工程与科学学院上海

在自动定理证明中，我们发现一个卓有成效的证明方法——多余文字参数法．利用这一方法可以简单便捷地证明许多难以证明的各种推理策略中的完备性问题．本文列举了如何应用这一方法来证明自动定理证明中归结原理的完备性、语义归结的完... 详细信息

在自动定理证明中，我们发现一个卓有成效的证明方法——多余文字参数法．利用这一方法可以简单便捷地证明许多难以证明的各种推理策略中的完备性问题．本文列举了如何应用这一方法来证明自动定理证明中归结原理的完备性、语义归结的完备性、线性归结的完备性以及输入归结和单位归结的等价性问题．事实表明这些原本都是十分棘手的证明问题，由于使用了这一方法而变为十分简单而自然的工作。

关键词：自动定理证明归结原理语义归结计算机证明

在线全文

学校读者我要写书评

暂无评论

一个用于一阶逻辑自动定理证明的新算法

计算机工程与科学 1993年第3期15卷 1-9页

作者：陈勇浩西安交通大学

本文提出一个用于一阶逻辑(FOPC)自动定理证明的并行算法,它基于分治的思想,把原问题子句集S划分成两个独立的子句集S1和S2,并通过并行地证明S_1和S_2的不可满足性。本文首先讨论了子句集的划分问题,引入了导出子句集及划分因子的概念;... 详细信息

本文提出一个用于一阶逻辑(FOPC)自动定理证明的并行算法,它基于分治的思想,把原问题子句集S划分成两个独立的子句集S1和S2,并通过并行地证明S_1和S_2的不可满足性。本文首先讨论了子句集的划分问题,引入了导出子句集及划分因子的概念;然后,在此基础上,提出了FOPC定理证明的并行算法;最后,给出了算法的有效性和完备性证明。文中还讨论了子句集的化简及算法性能评价等问题。

关键词：一阶逻辑自动定理证明算法

解决自动定理证明器在程序验证中两点能力不足的办法

在线全文

学校读者我要写书评

暂无评论

解决自动定理证明器在程序验证中两点能力不足的办法

作者：郝爔中国科学技术大学

学位级别：硕士

当今社会,计算机安全问题的严峻形势使得人们迫切需要高可信软件。形式化验证方法是提高软件可信度的一种可靠的方法,其中基于演绎推理的的方法更是近些年来的研究热点。本实验室基于演绎推理方法设计并实现了一种形式化程序验证的工具... 详细信息

当今社会,计算机安全问题的严峻形势使得人们迫切需要高可信软件。形式化验证方法是提高软件可信度的一种可靠的方法,其中基于演绎推理的的方法更是近些年来的研究热点。本实验室基于演绎推理方法设计并实现了一种形式化程序验证的工具——面向PointerC的程序验证原型系统(简称原型系统)。它是一个源码级的程序验证工具,其特色是先通过形状分析得到指针之间的关系,然后根据Hoare逻辑的扩展对程序进行演绎推理并生成验证条件,最后交给自动定理证明器证明。然而自动定理证明器对于本原型系统来说具有两点能力不足,第一点是无法进行归纳证明,第二点是无法自动发现全称量词彼此之间的联系。本文针对这两个问题,在实验室原有的工作基础上对原型系统的功能进行改进。本文的主要贡献如下：第一,设计并实现对程序员提供的性质定理的自动归纳证明。为了提高断言语言的表达能力,原型系统引入自定义归纳谓词。程序员有时在编写程序代码的过程中,会利用到递归定义谓词的归纳性质。同时,由于自动定理证明器在证明验证条件的过程中无法推导出这些归纳性质,程序员需要给出相关的性质定理辅助自动定理证明器证明。为了保证性质定理的正确性,本文给出了对性质定理先进行分析后进行结构归纳的方法,实现了性质定理的自动证明。第二,改进了带有全称量词断言的程序验证功能。当验证条件中包含全称量词断言时,自动定理证明器会因为无法发现多个全称量词彼此之间的关系而证明失败。本文提供了一种结合形状图对全称量词断言分组的思路,并且依据这种思路对验证条件中出现的全称量词进行处理,从而使得原型系统可以通过验证条件中包含多个全称量词断言的程序的验证。本文对原型系统进行扩展后,解决了当前原型系统中因为自动定理证明器两点能力不足带来的问题。保证了程序员提供的性质定理的正确性,不仅使得之前所有操作易变数据结构的程序实例的验证结果更加可靠,还使得原型系统可以验证包含多个全称量词断言的程序。

关键词：形式验证形状图逻辑结构归纳自动定理证明全称量词断言

自动定理证明中含有等词的Horn集上的输入半锁反驳

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

科学通报 1987年第8期32卷 628-630页

作者：吴茂康上海科技大学计算机系

本文的主要结果是文献[1]的推广。众所周知,等词(equality)由于它的自反性、对称性、可传性以及替换性,它在谓词演算中有着特殊的地位。这样的特殊性也反映在自动定理证明中,一个含有等词的E不可满足子句集,在各种反驳策略中,除了使用... 详细信息

本文的主要结果是文献[1]的推广。众所周知,等词(equality)由于它的自反性、对称性、可传性以及替换性,它在谓词演算中有着特殊的地位。这样的特殊性也反映在自动定理证明中,一个含有等词的E不可满足子句集,在各种反驳策略中,除了使用归结原理(resolution)以外,还必须使用调解(paramodulation)这一推理规则。尽管如此,我们仍然可以把不含等词的不可满足子句集上的许多性质和证明技术,推广到含有等词的不可满足子句集上去。例如在文献[2]的第八章中,就有相应的输入调解、单位调解和线性调解等等。

关键词：自动定理证明 Horn 等词

分析技术自动化基础——逻辑方程和自动定理证明

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

通信学报 1981年第2期 17-25页

作者：吴士珑

在本文中将未知变量引入到逻辑推理的过程,使分析技术进入了自动化的范畴。分析技术的自动化是人工智能的一个重要组成部分。本文提出的一个论点是:对未来的人工智能机器(机器人),关键的问题不是在于我们给机器规定了什么叫它去执行,... 详细信息

在本文中将未知变量引入到逻辑推理的过程,使分析技术进入了自动化的范畴。分析技术的自动化是人工智能的一个重要组成部分。本文提出的一个论点是:对未来的人工智能机器(机器人),关键的问题不是在于我们给机器规定了什么叫它去执行,而是要求机器人在任意未知的环境条件下,为了达到某一个目标——结论,如何去寻找为实现这个目标的途径——前提。机器人要是具有这种能力,就必须能按照客观的环境条件和已经学得的知识进行分析,判定为达到这个目标尚缺少几项前提,并寻找这些前提是否存在。上述过程可称之为分析技术自动化,可以通过分析逻辑方程的解集中的特殊形式的解来达到。

关键词：逻辑方程解法方程式方程方程的解自动定理证明机器人人工智能