一阶逻辑定理证明器CSE中矛盾体分离式的简化方法

作     者：吴鑫 陈树伟 姜世攀 WU Xin;CHEN Shuwei;JIANG Shipan

作者机构：西南交通大学数学学院成都611756 系统可信性自动验证国家地方联合工程实验室成都611756 

出 版 物：《计算机科学》 (Computer Science)

年 卷 期：2025年第52卷第5期

页      面：235-240页

学科分类：12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 081104[工学-模式识别与智能系统] 08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金(61976130) 

主　　题：矛盾体分离 矛盾体分离式简化 最简矛盾体分离式 互补信息 证明器 

摘      要：一阶逻辑自动定理证明器能够解决大量形式化后的实际问题,具有重要的应用价值。矛盾体分离演绎发展了自动定理证明领域经典的归结原理,具有更强的证明能力。在基于矛盾体分离规则的自动定理证明器CSE(Contradiction Separation Extension)的基础上,提出一种矛盾体分离式的简化算法,通过优化数据结构,使用指针保存子句间的互补信息,并在此基础上选择实际参与演绎的子句,从而得到最简矛盾体分离式。这种新的简化算法可生成更简短的分离式,进一步利用子句的合一互补性,增强空子句演绎路径的检测能力,提高证明器的效率。实验结果显示,相比CSE,使用此简化算法后的证明器CSE_BSCS能多证明39个测试例,平均证明时间减少了18.64%,在证明能力和效率上均更优。