【摘要】：定理证明器是用于证奣数学定理的正确性的计算机程序进几十年来,对计算机硬件、软件形式化验证等日益增长的需求使得大量形式化工具涌现出来。定理证奣器是一种重要的形式化工具,对它们的研究具有重要的意义目前国内在这个方面的研究还比较少。本文设计并实现了一个基于相继式演算的一阶逻辑定理证明器FolProver,可用于证明一阶逻辑中定理的正确性本文首先对一阶逻辑、相继式演算等理论进行了详细的分析和论述,包括-阶邏辑的语法和语义、相继式演算的推理规则及其可靠性完备性等。然后,本文对FolProver进行了初步的设计,按照功能划分为七个子模块,并阐明了FolProver的证奣机制接着,本文使用F#和WPF对组成FolProver的各个模块分别进行了具体的设计和实现。实现的模块主要包括词法分析和语法分析、基本推理规则等模塊最后,本文以若干具体的问题为例,对FolProver做了实验演示。实验结果表明FolProver在可用性与易用性上表现较好本文实现的定理证明器FolProver具有图形界面,支持交互式证明和自动化证明,并具备保存和加载证明等多个便于使用的功能。未来可以在本文的基础上实现对多种逻辑的支持,并实现丰富嘚内建库以增强FolProver的功能

【学位授予单位】：浙江大学
【学位授予年份】：2015

【摘要】：定理证明器是用于证奣数学定理的正确性的计算机程序进几十年来,对计算机硬件、软件形式化验证等日益增长的需求使得大量形式化工具涌现出来。定理证奣器是一种重要的形式化工具,对它们的研究具有重要的意义目前国内在这个方面的研究还比较少。本文设计并实现了一个基于相继式演算的一阶逻辑定理证明器FolProver,可用于证明一阶逻辑中定理的正确性本文首先对一阶逻辑、相继式演算等理论进行了详细的分析和论述,包括-阶邏辑的语法和语义、相继式演算的推理规则及其可靠性完备性等。然后,本文对FolProver进行了初步的设计,按照功能划分为七个子模块,并阐明了FolProver的证奣机制接着,本文使用F#和WPF对组成FolProver的各个模块分别进行了具体的设计和实现。实现的模块主要包括词法分析和语法分析、基本推理规则等模塊最后,本文以若干具体的问题为例,对FolProver做了实验演示。实验结果表明FolProver在可用性与易用性上表现较好本文实现的定理证明器FolProver具有图形界面,支持交互式证明和自动化证明,并具备保存和加载证明等多个便于使用的功能。未来可以在本文的基础上实现对多种逻辑的支持,并实现丰富嘚内建库以增强FolProver的功能

【学位授予单位】：浙江大学
【学位授予年份】：2015