基于相继式演算和叠加法的一阶逻辑定理证明器设计与实现

发布时间：2021-11-28 18:33

　　随着对计算机系统安全性、可靠性需求的提高,形式化方法得到了更多的重视。定理证明是重要的形式化技术之一,它用于验证数学定理的正确性。定理证明器可以帮助用户以轻松的、可靠的方式对定理进行证明。本文实现了一个一阶逻辑定理证明器,它使用相继式演算作为交互式定理证明的演绎系统,使用叠加法作为自动定理证明的演绎系统。本文首先对一阶逻辑和序理论进行了论述,为接下来介绍演绎系统做了知识的预备。然后分析介绍了相继式演算、归结原理和叠加法这三种演绎系统。接着本文描述了定理证明器中各个模块的功能及联系,然后分别从交互式定理证明、自动定理证明的角度对每个模块的设计和实现进行了介绍。最后以若干用例演示了证明器的功能并以问题集测试了证明器的能力。通过本文实现的定理证明器,用户可以在图形界面上方便的进行交互式定理证明,也可以调用自动定理证明模块尝试自动解决问题,或者通过两者之间的配合解决问题。未来可以在这基础上支持更多的逻辑,提高描述能力,也可以对自动定理证明能力进行加强。 

【文章来源】：浙江大学浙江省 211工程院校 985工程院校 教育部直属院校

【文章页数】：92 页

【学位级别】：硕士

【部分图文】：

图４．５?ｓｕｂｓｔｔ算法伪代码??

?＜Ｔｅｒｎｓ＞??｜?＜Ｔｅｒｍ＞??图４．６?ＧＯＡＬ?Ｐａｒｓｉｎｇ中定义公式和项??４．?３输入环境??输入公理和定理的环境为输入环境。用户可以在界面上增加、删除公式，并??标记公式为公理或者是定理。输入环境的界面如图４．７所示。??Ｆｏｒｍｕｌｉｉ?Ｏｅ：ｅｔｅ?Ｃ！？ａｒ?Ｐｒｏａｆ??〇?■?ｆａｒａｊｉ?＞１?ｆｏｒａｉｉ?ｙ．?？？?＾?ａｘｉｏｎｉ??ｉ．?Ｉ?ｆｏｒａｌｌ?ｘ．?ｆ（ｅ〇?ｓｌ－ｘ?ｈ／ｉ?ｉｘｉｏｍ??〇?ｆｃｒａｌｌ?ｘ．?＾ｉｎ＾（ｘ）ｊ￡）＝＃〇?Ｒｊ?ａｘｔｏｒａ??ｉ？Ｊ?ｆｏｒａｌｌ?ｘ．?ｆ（ｘ?ｉｎｖ（ｘ））＝ｅ〇?．?Ｊ?ｍｏｍ??ｊ?：！??Ｉ?－－■■■■……－————：七．．．．．．．．．．．．．．…丁ｒ．．．－——：：一■—？．．．．．，娜??图４．７输入环境??４０??

４．?３输入环境??输入公理和定理的环境为输入环境。用户可以在界面上增加、删除公式，并??标记公式为公理或者是定理。输入环境的界面如图４．７所示。??Ｆｏｒｍｕｌｉｉ?Ｏｅ：ｅｔｅ?Ｃ！？ａｒ?Ｐｒｏａｆ??〇?■?ｆａｒａｊｉ?＞１?ｆｏｒａｉｉ?ｙ．?？？?＾?ａｘｉｏｎｉ??ｉ．?Ｉ?ｆｏｒａｌｌ?ｘ．?ｆ（ｅ〇?ｓｌ－ｘ?ｈ／ｉ?ｉｘｉｏｍ??〇?ｆｃｒａｌｌ?ｘ．?＾ｉｎ＾（ｘ）ｊ￡）＝＃〇?Ｒｊ?ａｘｔｏｒａ??ｉ？Ｊ?ｆｏｒａｌｌ?ｘ．?ｆ（ｘ?ｉｎｖ（ｘ））＝ｅ〇?．?Ｊ?ｍｏｍ??ｊ?：！??Ｉ?－－■■■■……－————：七．．．．．．．．．．．．．．…丁ｒ．．．－——：：一■—？．．．．．

【参考文献】：
期刊论文
[1]一个用于指针程序验证的自动定理证明器的设计与实现[J]. 王振明,陈意云,王志芳.  小型微型计算机系统. 2010(05)



本文编号：3524935