若干逻辑自动推理方法研究

发布时间：2023-04-20 22:28

　　自动定理证明(Automated Theorem Proving)或者机器定理证明(MechanicalTheorem Proving)是通过计算机实现定理证明.二十世纪五十年代以来自动定理证明一直是计算机科学的热点之一,在数学、硬件测试与验证、软件生成与验证、协议验证、人工智能方面都得到了成功的应用. 部分实例化方法把一阶问题化为一系列命题逻辑中的可满足性问题来解决一阶逻辑的可满足问题,检查子句集的满足式映射中的阻塞是该方法的关键.论文提出的子句搜索方法在判定子句集可满足性的同时给出了一个模型从而得到满足式映射.格值逻辑的不完全可比性便于描述人类的思维、判断和决策.格值命题逻辑系统LP(X)于1993年建立,目前对LP(X)系统的自动推理研究主要是归结方法,论文讨论了它的tableau方法.常用的逻辑证明方法重点在于判定可满足性而不能给出符合人们阅读习惯的演绎过程.归结方法、语义表方法、相继式方法是定理证明中的常用方法,但是重点在于判定而不是演绎,论文探讨了相干命题逻辑系统R的试探法实现和相干自然推理系统NR的自然推理法实现,生成了类似于手工证明的可读证明.具体而言论文的工作包括以下...

【文章页数】：117 页

【学位级别】：博士

【文章目录】：
摘要
Abstract
第一章 绪论
    1.1 自动推理的发展简史
    1.2 非经典逻辑研究概况
    1.3 论文的选题和主要工作
第二章 一阶子句搜索方法
    2.1 子句搜索方法
    2.2 一阶子句搜索方法
    2.3 本章小结
第三章 格值命题逻辑LP(X)的自动证明
    3.1 基础知识
    3.2 LP(X)的tableau方法
    3.3 LP(X)的直积分解
    3.4 本章小结
第四章 相干命题逻辑R的可读证明
    4.1 试探法自动证明
    4.2 自然推理法自动证明
    4.3 试探法和自然推理法的混合求证
    4.4 本章小结
第五章 总结与展望
参考文献
致谢
攻读博士学位期间发表论文和科研情况



本文编号：3795279