矛盾体分离单元结果演绎方法及应用

来源：计算机工程与科学杂志2024年第12期北京时间：

作者：曹锋, 谢燏, 易见兵, 李俊

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

摘要：一阶逻辑自动定理证明是人工智能领域重要的研究内容。为提高单元结果归结演绎效率，提出了一种新的基于多元、动态、协同的单元结果演绎方法，称为矛盾体分离单元结果演绎方法，并详细地给出了其演绎定义、演绎方法、演绎的优势分析及算法实现；提出的演绎方法允许多个子句同时参与演绎，且允许多个非单元子句参与1次单元结果演绎，能较好地处理长子句；提出的演绎算法能使用策略选定较优的子句和动态设定变元合一的复杂度，并通过回溯机制优化搜索的演绎路径。以近2年国际一阶逻辑自动定理证明器竞赛例（分别为500个）和TPTP问题库中难度系数为1的问题作为测试对象，加入了矛盾体分离单元结果演绎算法的Eprover和原始Eprover相比分别多证明了10个定理，分别能证明Eprover无法证明的17个定理和13个定理，能证明出9个其他所有证明器都无法证明难度系数为1的定理。实验结果表明，提出的矛盾体分离单元结果演绎方法能有效提高一阶逻辑自动定理证明的效率。

关键词：一阶逻辑,自动定理证明,人工智能,单元结果归结,矛盾体分离规则,

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