基于相继式演算的一阶逻辑定理证明器设计与实现
发布时间：2021-10-07 00:01
定理证明器是用于证明数学定理的正确性的计算机程序。进几十年来,对计算机硬件、软件形式化验证等日益增长的需求使得大量形式化工具涌现出来。定理证明器是一种重要的形式化工具,对它们的研究具有重要的意义。目前国内在这个方面的研究还比较少。本文设计并实现了一个基于相继式演算的一阶逻辑定理证明器FolProver,可用于证明一阶逻辑中定理的正确性。本文首先对一阶逻辑、相继式演算等理论进行了详细的分析和论述,包括-阶逻辑的语法和语义、相继式演算的推理规则及其可靠性完备性等。然后,本文对FolProver进行了初步的设计,按照功能划分为七个子模块,并阐明了FolProver的证明机制。接着,本文使用F#和WPF对组成FolProver的各个模块分别进行了具体的设计和实现。实现的模块主要包括词法分析和语法分析、基本推理规则等模块。最后,本文以若干具体的问题为例,对FolProver做了实验演示。实验结果表明FolProver在可用性与易用性上表现较好。本文实现的定理证明器FolProver具有图形界面,支持交互式证明和自动化证明,并具备保存和加载证明等多个便于使用的功能。未来可以在本文的基础上实现对多种...
【文章来源】：浙江大学浙江省 211工程院校 985工程院校 教育部直属院校
【文章页数】：90 页
【学位级别】：硕士
【部分图文】：
图４．１１定理证明器ＦｏｌＰｒｏｖｅｒ的用户界面设计??回到Ｆ护源代码中，可Ｗ吏用Ａｐｐｌｉｃａｔｉｏｎ类的ＬｏａｄＣｏｍｐｏｎｅｎｔ方法加载Ｘａｍｌ??文件，并使用巧ｎｄＮａｍｅ方法提取Ｘａｍｌ中的控件
进行可视化操作（比如剪除证明树中的某棵子树）。在Ｐｒｏｏｆ?Ｔｒｅｅ?Ｖｉｅｗ中显示证??明树需要在底层有数据作支撑。??证明树类型定义如图４．１２所示：??ｔｙｐｅ?Ｔｒｅｅ?二??：Ｎｏｄ？?ｏｆ?Ｓｅｑｕｅｎｔ；參?ｓｔｒｉａ賓?ｒｅｆ?療?ｌｉｓｔ＜Ｔｒ０巧＞?ｒｅｆ??ｉ?Ｅｍｐｔｙ?ｏｆ?泛ｔｒｉｎ沒??團４．１２证明树的实现??其中，Ｎｏｄｅ是证明树中的结点。Ｓｅｑｕｅｎｔ类型的参数为结点中的目标相继式，??ｓｔｒｉｎｇ?ｒｅｆ类型的参数为应用在相继式上的推理规则的名称，ｌｉｓｔ＜Ｔｒｅｅ＞?ｒｅｆ类型的??参数为该结点所有的子树。Ｅｍｐｔｙ表示空树。??除了定义证明树类型，还需要实现如下函数；??？为证明树中的指定叶子结点插入子树（当执行一条推理规则生成新的目??标相继式时调用）??？遍历证明树，获取所有的叶子结点，即获取当前所有待证明的目标相继??式??？删除证明树中Ｗ给定相继式为根的子树??？在证明树中搜索某个给定的目标相继式??在Ｐｒｏｖｅｒ模块中，定义一个Ｔｒｅｅ类型的变量ｃｕｒｒＰｒｏｏｆＴｒｅｅ表示当前的证明??树。当开始一个新的证明时，初始化ｃｕｒｒＰｒｏｏｆＴｒｅｅ；当在某个待证明的目标相继??式上应用指定的推理规则时，则更新ｃｕｒｒＰｒｏｏｆＴｒｅｅ。当要剪除证明树中Ｗ给定相??继式为根的某棵子树时
称一个集合Ｓ是循环的（ｃｉｒｃｕｌａｒ），如果Ｓ是另外一个集合ｙ是Ｓ的儿索。直观上米看，所有的集合都是非循环集合（ｎｏｎｃｉｒｃｕ选择一些非循环集合构成一个新的集合。但是，并不存在这样构成的集合。??逻辑无法表示集合的概念，这里仍然选捧使用谓词来表示上述．ｖ）表示Ｘ是的一个元素，其中Ｘ和ｙ均为集合。＂不存在一成的集合＂可＾＾＾形式化表示为：??－ｉ（３ｙＶｘ（Ｍ（ｘ，ｙ）?＾?－ｉ（３ｚＭ（ｘ，?ｚ）?Ａ?Ｍ（ｚ，?ｘ））））?公使用ＦｏｌＰｒｏｖｅｒ来证明这个定理。按照ＦｏｌＰｒｏｖｅｒ的文法约定，－ｉ（３ｙ．?Ｖｘ．?（Ｍ（ｘ，ｙ）?－ｉ（３ｚ．?Ｍ（ｘ，ｚ）八?Ｍ（ｚ，?ｘ）Ｗ）??目前实现的自动化证明策略，ＦｏｌＰｒｏｖｅｒ无法在有限的时间内对化证明，但是可Ｗ交互式地采用更灵活的策略逐步完成对该定每一步使用的推理规则如图５．２所示：??
【参考文献】：
期刊论文
[1]INCAPS:一个交互式计算机辅助定理证明系统[J]. 黎仁蔚. 计算机学报. 1989(12)
博士论文
[1]用于指针逻辑的自动定理证明器的设计与实现[D]. 王振明.中国科学技术大学 2009
本文编号：3420991
【文章来源】：浙江大学浙江省 211工程院校 985工程院校 教育部直属院校
【文章页数】：90 页
【学位级别】：硕士
【部分图文】：
图４．１１定理证明器ＦｏｌＰｒｏｖｅｒ的用户界面设计??回到Ｆ护源代码中，可Ｗ吏用Ａｐｐｌｉｃａｔｉｏｎ类的ＬｏａｄＣｏｍｐｏｎｅｎｔ方法加载Ｘａｍｌ??文件，并使用巧ｎｄＮａｍｅ方法提取Ｘａｍｌ中的控件
进行可视化操作（比如剪除证明树中的某棵子树）。在Ｐｒｏｏｆ?Ｔｒｅｅ?Ｖｉｅｗ中显示证??明树需要在底层有数据作支撑。??证明树类型定义如图４．１２所示：??ｔｙｐｅ?Ｔｒｅｅ?二??：Ｎｏｄ？?ｏｆ?Ｓｅｑｕｅｎｔ；參?ｓｔｒｉａ賓?ｒｅｆ?療?ｌｉｓｔ＜Ｔｒ０巧＞?ｒｅｆ??ｉ?Ｅｍｐｔｙ?ｏｆ?泛ｔｒｉｎ沒??團４．１２证明树的实现??其中，Ｎｏｄｅ是证明树中的结点。Ｓｅｑｕｅｎｔ类型的参数为结点中的目标相继式，??ｓｔｒｉｎｇ?ｒｅｆ类型的参数为应用在相继式上的推理规则的名称，ｌｉｓｔ＜Ｔｒｅｅ＞?ｒｅｆ类型的??参数为该结点所有的子树。Ｅｍｐｔｙ表示空树。??除了定义证明树类型，还需要实现如下函数；??？为证明树中的指定叶子结点插入子树（当执行一条推理规则生成新的目??标相继式时调用）??？遍历证明树，获取所有的叶子结点，即获取当前所有待证明的目标相继??式??？删除证明树中Ｗ给定相继式为根的子树??？在证明树中搜索某个给定的目标相继式??在Ｐｒｏｖｅｒ模块中，定义一个Ｔｒｅｅ类型的变量ｃｕｒｒＰｒｏｏｆＴｒｅｅ表示当前的证明??树。当开始一个新的证明时，初始化ｃｕｒｒＰｒｏｏｆＴｒｅｅ；当在某个待证明的目标相继??式上应用指定的推理规则时，则更新ｃｕｒｒＰｒｏｏｆＴｒｅｅ。当要剪除证明树中Ｗ给定相??继式为根的某棵子树时
称一个集合Ｓ是循环的（ｃｉｒｃｕｌａｒ），如果Ｓ是另外一个集合ｙ是Ｓ的儿索。直观上米看，所有的集合都是非循环集合（ｎｏｎｃｉｒｃｕ选择一些非循环集合构成一个新的集合。但是，并不存在这样构成的集合。??逻辑无法表示集合的概念，这里仍然选捧使用谓词来表示上述．ｖ）表示Ｘ是的一个元素，其中Ｘ和ｙ均为集合。＂不存在一成的集合＂可＾＾＾形式化表示为：??－ｉ（３ｙＶｘ（Ｍ（ｘ，ｙ）?＾?－ｉ（３ｚＭ（ｘ，?ｚ）?Ａ?Ｍ（ｚ，?ｘ））））?公使用ＦｏｌＰｒｏｖｅｒ来证明这个定理。按照ＦｏｌＰｒｏｖｅｒ的文法约定，－ｉ（３ｙ．?Ｖｘ．?（Ｍ（ｘ，ｙ）?－ｉ（３ｚ．?Ｍ（ｘ，ｚ）八?Ｍ（ｚ，?ｘ）Ｗ）??目前实现的自动化证明策略，ＦｏｌＰｒｏｖｅｒ无法在有限的时间内对化证明，但是可Ｗ交互式地采用更灵活的策略逐步完成对该定每一步使用的推理规则如图５．２所示：??
【参考文献】：
期刊论文
[1]INCAPS:一个交互式计算机辅助定理证明系统[J]. 黎仁蔚. 计算机学报. 1989(12)
博士论文
[1]用于指针逻辑的自动定理证明器的设计与实现[D]. 王振明.中国科学技术大学 2009
本文编号：3420991
本文链接：https://www.wllwen.com/shekelunwen/ljx/3420991.html
