自动定理证明相关论文
现年97岁的数学家吴文俊教授依旧精神矍铄，他曾经明确指出：机器的出现延伸了人的体力，而现代计算机的出现则延伸了人的脑力。受技术进......
机器定理证明在数学定理证明、协议验证、软件和硬件的形式化验证等方面发挥出越来越重要的作用。为了提高定理证明器的工作效率和......
随着计算机科学技术的飞速发展,计算机软件的规模日益庞大,调试和维护越来越困难。而另一方面,软件的安全形势严峻,对未受信源提供......
随着计算机学科的迅猛发展，计算机软件正逐渐演化成为人们学习生活中的一个庞大的体系。另一方面，软件的安全形势非常严峻，尤其随着移......
请下载后查看，本文暂不支持在线获取查看简介。
Please download to view, this article does not support online access to view......
一、引言 验证逻辑设计正确性的传统方法是模拟(Simulation),然而随着数字电路规模和功能扩大,模拟方法已不能保证设计的正确性。......
2.3.3 自动定理证明在致力于编制能够证明数学定理和逻辑定理的程序方面明显地存在有三个重要的课题。首先,AI 研究者们的早期工......
本文对从图灵试验的启示到知识工程的兴起这一人工智能及其应用发展的历史阶段进行了回顾。概述了计算机下棋的兴起与困难;机器翻......
本文提出了一种新的对数字电路进行逻辑分析的方法——推理方法。该方法将逻辑分析问题看作是一个自动定理证明问题,即将逻辑电路......
本文以文[1]为基础,继续讨论中介逻辑的自动推理理论,文中给出了中介谓词演算系统MF及MF~*、带等词的中介谓调演算系统ME及ME~*的......
本文及其后续文章将系统地探讨中介逻辑诸子系统的自动推理理论及其实现方式。本文着重讨论中介命题逻辑的自动定理证明理论。文中......
在自动定理证明中，我们发现一个卓有成效的证明方法——多余文字参数法．利用这一方法可以简单便捷地证明许多难以证明的各种推理策略......
摘 要：人工智能是近来研究热点。分别在人工智能界别、角色、赋予人以及制度等方面重点探讨其可能的情感约束作用，以期达到人工智能......
非经典逻辑的研究一直是人工智能领域中非常受人关注的一个研究方向.目前,基于非经典逻辑的自动定理证明系统由于它加速了人工智能......
程序性质的自动验证有时需要验证者提供相关的归纳引理,程序验证的结果可靠与否依赖于验证者所提供的归纳引理正确与否.本文围绕操......
近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助......
在先前设计的一个出具证明编译器原型基础上,增加了可用来描述数据结构性质的自定义谓词,对断言语言表达能力方面做了提升.在出具......
对归结原理的基本概念与推理规则进行了讨论，并在此基础上通过实例探讨了归结推理方法在数学定理证明中的应用。......
在多值逻辑中,含有量词的Tableau方法具有统一的扩展规则,并已通过可靠性和完备性的证明,但是由于扩展后的分枝非常庞大,使机器实......
基于代数和递归函数理论，本文定义了代数递归谓词，代数递归谓词是一类广泛的谓词，基平均数学归纳法，作者给出了证明代数递归谓词永真性......
<正>归纳定理证明是一种难度较大且较有前途的一种自动定理证明方法。较早的归纳定理证明器是Boyer一Moore于1979年提出的BM证明器......
1.引言自动推理作为自动定理证明的扩展,在计算机科学,特别是人工智能领域中占有重要的地位.许多系统,都是以推理系统作为其核心部......
连接法是一种较新的自动定理证明的方法．该文讨论了带有等词的连接法，给出了形式化的定义，证明了带有等词的逻辑公式是ｅｑ有效的当且仅当......
进一步讨论关于正规模态逻辑Ｓ５的自动定理证明理论与方法，给出了正规模态逻辑Ｓ５的表推演系统ＴＳ６，证明了该可靠性与完备性。......
本文给出了一个在自然数的有穷客体域Dk={l，2，…，k}（k≥0）内一阶谓词逻辑公式的k普遍有效性的判定算法。对于只包含一元谓词的公式以及......
目前命题公式的判定方法大都是基于语义的，不能给出演绎过程，而演绎过程是许多推理性应用的重要依据．文中针对命题演算系统L，提出了一......
本文提出一个用于一阶逻辑（FOPC）自动定理证明的并行算法,它基于分治的思想,把原问题子句集S划分成两个独立的子句集S1和S2,并通过并......
本文在RUE-NRF推理规则的基础上,定义了RUE-NRF输入归结、RUE-NRF单元归结及RUE-NRF锁归结的概念,证明了RUE-NRF输入反驳与RUE-NRF......
连接法是自动定理证明中一种较新的证明方法,本文讨论了任意矩阵的连接法,给出了一条用于任意矩阵的一般的简化规则及其正确性的证......
在人类的发展史中，人们发明了各种各样的机器设备来模拟和延伸人的体力活动，那么对于人的智力活动是否也可以用某种装置来模拟和延伸......
<正> 作者根据锁归结(lock resolution)原理用LISP语言编制了完整的框图和程序,并在APPLE Ⅱ机器上实现了对命题逻辑中的定理的证......
...
文中研究了模态逻辑推理的翻译法，即把模态逻辑公式按照一定的规则翻译成经典逻辑公式，再用传统的定理器进行推理，文中指出，该方法在理......
连接法是继归结法以后由Bibel W等人于80年代初提出的一种自动定量证明的方法.本文介绍了一个以PASCAL语言在IBM4361中型机上实现......
在自动定理证明中，我们发现一个卓有成效的证明方法－多余文字参数法。利用这一方法可以简单便捷地证明许多难以证明的各种推理策略中......
回 回 产卜爹仇贱回——回 日E回。”。回祖 一回“。回干 肉果幻中 N_。NH lP7-ewwe--一”＄ MN。W;- __._——————》 砧叫]们......
提出用条件化技术对程序进行预处理的方案，以克服软件模型检测中状态空间爆炸问题。以程序性质公式中蕴涵式的前件作为约束条件，通过......
验证操作易变数据结构的指针程序仍面临很多挑战.数据结构中严重的指针别名显著地复杂化对操作这些结构的程序的推理.为分析和验证......
自动定理证明(又叫机器定理证明、机械化定理证明等)是人工智能研究的一个重要分枝,是数学、计算机科学的交叉学科,我国科学家在这......
归纳法推理是人工智能领域中富有挑战性的研究方向，它是一种难度较大但较有前途径的自动定量证明方法，文章对近年来归纳法推理的主要......
