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

Simplification Method for Contradiction Separation Clause in First-order Logic Automated Theorem Prover CSE

作　　者：吴鑫 陈树伟 姜世攀 WU Xin;CHEN Shuwei;JIANG Shipan(School of Mathematics,Southwest Jiaotong University,Chengdu 611756,China;National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,Chengdu 611756,China)

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

出　　处：《计算机科学》2025年第5期235-240,共6页Computer Science

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

摘　　要：一阶逻辑自动定理证明器能够解决大量形式化后的实际问题,具有重要的应用价值。矛盾体分离演绎发展了自动定理证明领域经典的归结原理,具有更强的证明能力。在基于矛盾体分离规则的自动定理证明器CSE(Contradiction Separation Extension)的基础上,提出一种矛盾体分离式的简化算法,通过优化数据结构,使用指针保存子句间的互补信息,并在此基础上选择实际参与演绎的子句,从而得到最简矛盾体分离式。这种新的简化算法可生成更简短的分离式,进一步利用子句的合一互补性,增强空子句演绎路径的检测能力,提高证明器的效率。实验结果显示,相比CSE,使用此简化算法后的证明器CSE_BSCS能多证明39个测试例,平均证明时间减少了18.64%,在证明能力和效率上均更优。First-order logic automated theorem proving has the capacity to resolve a multitude of practical problems after formalization,and thus holds considerable practical value.As an advancement in automated theorem proving,contradiction separation deduction extends the classical resolution principle and exhibits enhanced proving capability.In this paper,a simplified algorithm for contradiction separation is proposed and theoretically proven based on the Contradiction Separation Extension(CSE)prover,which follows the rule of contradiction separation.The proposed algorithm enhances efficiency via data structure optimization,utilizing pointers to store complementary information between clauses.This information is then employed to select the clauses that are involved in deductions,thereby achieving the separation clause simplification.This approach produces shorter separation clauses while leveraging the unification complementarity of clauses to strengthen the detection capability of empty clause derivation paths,ultimately improving prover efficiency.Experimental results demonstrate that the enhanced prover CSE_BSCS with this simplification algorithm solves 39 additional test cases compared to the original CSE,with an 18.64%reduction in average proving time.These improvements confirm the superior performance of CSE_BSCS in both proving capability and efficiency over CSE.

关 键 词：矛盾体分离 矛盾体分离式简化 最简矛盾体分离式 互补信息 证明器 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]