计算机应用

作者：曹锋, 杨小玲, 易见兵, 李俊

单位：江西理工大学 信息工程学院，江西 赣州 341000

关键词：定理证明器,二元演绎,超归结,多元演绎,矛盾体分离

基金：国家自然科学基金资助项目(62366017);江西省教育厅科研项目(GJJ200818);赣州市科技计划项目(GZKJ20206030);江西理工大学博士启动基金资助项目(205200100060)

作为当前自动定理证明器中常用的推理机制，传统基于二元演绎超归结方法的推理过程限定每次有且只有2个子句参与演绎，这种分离的演绎步骤导致演绎缺失导向性和预判性，演绎效率有待提升。为了提升演绎效率，在理论上，针对传统的超归结方法引入多元演绎思想，提出矛盾体分离超演绎定义和方法，它具有多元性、动态性和导向性的演绎特性；在算法实现中，考虑子句参与演绎具有多元和协同特性，并灵活设定演绎的条件，提出一种具有回溯机制的矛盾体分离超演绎算法。将所提算法应用于Eprover3.1证明器，以国际自动定理证明器2023年竞赛例和TPTP（Thousands of Problems for Theorem Provers）问题库中难度系数为1的问题作为测试对象，在300 s内，应用所提算法的Eprover3.1证明器比原始Eprover3.1多证明了15个定理；当测试相同数量的定理时，所提算法的平均证明时间缩减了1.326 s，能够证明7个难度系数为1的定理。测试结果表明，所提算法能有效地应用于一阶逻辑自动定理证明，提升自动定理证明器的证明能力和效率。

来源：2024年第10期

《计算机应用》期刊编辑部

查看计算机应用杂志2024年第10期