基于单元子句的多元矛盾体分离动态演绎算法及应用

A Multi-Clause Contradiction Separation Dynamic Deduction Algorithm Based on Unit Clauses and Its Application

摘要

矛盾体分离规则，作为一种突破传统二元归结框架的多元演绎方法，为自动推理领域开辟了新的研究内容。为提高多元演绎的证明能力和效率，本文将子句集中的子句分为单元子句与非单元子句，给出单元子句在矛盾体分离规则中的演绎性质，设计了一种单元子句选择策略，能较好地规划单元子句参与多元演绎的顺序；提出一种基于单元子句的多元矛盾体分离动态演绎算法，有效提升了单元子句进行多元演绎的推理能力。将提出的多元演绎算法应用于国际顶尖证明器Eprover3.2和国际知名证明器Prover9中，形成UCSDA_Eprover3.2证明器和UCSDA_P证明器，以2023年和2024年国际证明器竞赛例为测试对象（分别为500个）进行测试，结果表明，UCSDA_Eprover3.2在定理证明能力方面相较于Eprover3.2表现更优，分别多证明了15个和14个定理，且分别能证明Eprover3.2未能证明的17个和15个定理；针对2023年国际证明器竞赛例，UCSDA_P比Prover9多证明定理71个，占Prover9证明总数的53.38%；为进一步验证该算法能有效判定难问题，以TPTP（Thousands of Problems for Theorem Provers）库中rating为1的问题作为测试集，UCSDA_Eprover3.2证明了其他所有证明器未证明的8个定理。

Abstract

The contradiction separation rule, as a multi-clause deduction method that breaks through the traditional binary resolution framework, has opened up new research content for the field of automated reasoning. To enhance the capability and efficiency of multi-clause deduction, this paper categorizes the clauses involved in clauses set into two types: unit clauses and non-unit clauses, and gives the deduction properties of unit clauses in contradiction separation rule and a unit clause selection strategy, which can better plan the order of unit clauses participating in multi-clause deduction. A multi-clause contradiction separation dynamic deduction algorithm based on unit clauses has been proposed, which can effectively enhance the inference capability of unit clauses for multi-clause deduction. The top international prover Eprover3.2 and the famous international prover Prover9 are combined with the proposed multi-clause deduction algorithm, and the two formed provers are called UCSDA_Eprover3.2 and UCSDA_P. Taking the 2023 and 2024 years’ international prover competition problems (with 500 problems for each year) as test objects, we found that, UCSDA_Eprover3.2 exhibits superior theorem-proving performance compared with Eprover3.2, solving 15 and 14 more theorems in two respective test sets. Furthermore, UCSDA_Eprover3.2 proves 17 and 15 theorems that Eprover3.2 fails to prove. For the 2023 international prover competition problems, UCSDA_P has solved 71 theorems more than the original Prover9, accounting for 53.38% of the total number of Prover9 proofs. To further verify that the algorithm can effectively handle difficult problems, the problems with a rating of 1 from the TPTP(Thousands of Problems for Theorem Provers) benchmark database were used as test objects, and UCSDA_Eprover3.2 has solved 8 theorems that were not solved by any other provers.

Graphical abstract

关键词

矛盾体分离规则 / 二元归结 / 自动推理 / 证明器 / 一阶逻辑

Key words

contradiction separation rule / binary resolution / automated reasoning / prover / first-order logic

0　 引 言

一阶逻辑自动定理证明是自动推理分支的核心内容，其实质是利用计算机实现的自动推理方法，对给定的一阶逻辑子句集进行演绎推理，直至推导出空子句，进而判断逻辑公式所表示问题的正确性。与命题逻辑系统相比，一阶逻辑系统具有更强的表达能力，能有效地刻画数学定理及现实事物。因此，深入探究一阶逻辑自动定理证明方法，对提升逻辑推理解决现实问题的能力和效率具有重要的学术意义^[1-2]，这也使其成为国际上备受瞩目且学术界广泛关注的研究热点。

归结原理的提出为定理证明器的发展提供了重要的理论支持，它通过消除两个子句中存在的合一互补对文字，将剩余文字的析取作为演绎新子句^[3]。当两个存在合一互补对文字的单元子句进行归结时，演绎生成空子句，则定理得证。在自动定理证明过程中，二元归结作为基础性推理理论，具有巨大的演绎路径搜索空间，故其归结效率需进一步提升。为了缩减自动定理证明过程中的搜索路径，学者们基于归结原理提出了一系列的归结方法，代表性的有：超归结^[4]、语义归结^[5]、单元归结^[6]、锁归结^[7]、单元结果归结^[8]、锁语义归结^[9]、线性归结^[10]以及冲突归结^[11]等。这些方法通过限定参与演绎的子句或文字，有效缩减了演绎路径的搜索空间。由于每步演绎仅处理两个子句及其之间的一组互补文字，故上述归结方法本质上仍属于二元归结范畴。因此，为了更好地对文字进行消元，有效发挥多子句之间的协同推理能力，研究多元演绎方法及有效的算法具有重要的现实意义。

矛盾体分离规则^[12]突破了二元归结方法的限制，允许多子句动态协同参与，通过构建标准矛盾体的形式对子句进行文字消元，具有多元性、动态性、协同性、导向性及生成的新子句文字少等演绎特点^[13]。在多元演绎理论与方法研究上，文献[14]分析了矛盾体分离演绎的特性，提出了多元演绎中子句和文字的选择方法；文献[15]提出了一种以生成演绎分离式文字数递增为目的的矛盾体分离演绎算法，并提出了子句重构思想，实验表明子句充分性演绎能有效提升多元演绎能力；文献[16]提出了基于命题逻辑的两类特殊标准矛盾体——完全标准矛盾体和最小标准矛盾体的定义和方法，并揭示了其可通过添加新子句或相关文字实现互换的性质；文献[17]提出了一种设定演绎起步子句的矛盾体分离演绎算法，通过引入有效演绎权重和无效演绎权重，利用回溯机制避免无效路径搜索，同时充分发挥子句间的协同演绎能力；文献[18]提出了一种新的多元动态演绎算法，通过设定子句选择、文字选择以及全局阈值等策略，并将其引入自动定理证明演绎框架，以提升系统性能；文献[19]提出了一种计算子句变元活跃度和子句函数项复杂度的方法，利用这两种子句度量值提出了新的子句选择策略并应用于多元矛盾体分离演绎规则；文献[20]提出了一种利用主文字的正负属性优化子句演绎顺序的方法（主文字是指在矛盾体分离规则中用于构建新标准矛盾体的文字，其集合称为主文字集），该方法通过搜寻更多互补对文字优化多元演绎路径；文献[21]提出了一种子句充分性评估方法，该方法基于矛盾体分离规则中子句可重复参与演绎的特性，通过计算重复参与演绎的次数优化演绎路径，从而提升多元动态演绎的能力。

上述文献提出了多种基于矛盾体分离规则的子句及文字选择方法，确定参与多元动态演绎的子句优先级顺序，并对子句重复参与演绎的次数进行有效的评估，从而在一定程度上提升了定理证明的能力。然而，这些研究主要聚焦于文字或子句的选择策略，尚未探讨根据子句中文字数量对多元演绎能力的影响，即未有效发挥文字数量较少的子句的演绎能力。文字数量较少的子句参与演绎往往可生成更简短的矛盾体分离式，从而提高多元演绎效率。单元子句文字数量仅为1，在多元演绎框架中展现出了较强的灵活性，但其演绎性质未能充分挖掘与高效利用。具体而言，借助矛盾体分离规则的多元性、动态性以及协同性特征^[22]，单元子句可高效与其他子句互补，快速参与多元演绎，且不会增加矛盾体分离式数量，从而缩短演绎路径，提升演绎效率。这对于深化多元演绎方法的研究，提升自动定理证明的推理能力具有重要意义。

鉴于单元子句在一阶逻辑自动定理证明的特殊性，本文深入分析了单元子句在多元演绎过程中的特殊演绎性质，提出了多元演绎中的单元子句选择策略，并设计了一种基于单元子句的多元矛盾体分离动态演绎算法（Unit Contradiction Separation Deduction Algorithm， UCSDA）。该算法充分发挥了单元子句在多元演绎中的推理能力，同时借助回溯机制提升搜索效率。实验表明，本文算法能提升证明器Eprover3.2^[23]和Prover9^[24]的性能。

1　 基础知识

定义1 子句^[25]：子句是由一个或多个文字构成的析取式。

子句分为三类：空子句（不含文字，记作“\mathrm{\varnothing }”），单元子句（仅含一个文字），非单元子句（含多个文字）。

定义2 互补对文字^[25]：在一阶逻辑中，互补对文字是指一对文字，它们具有相同的项，但其谓词符号相反。

例如文字P_{\mathrm{1}}(x_{\mathrm{1}})和文字\sim P_{\mathrm{1}}(x_{\mathrm{1}})，这两个文字是一组互补对文字。

定义3 替换^[25]：设x_{\mathrm{1}},x_{\mathrm{2}},\cdots ,x_n是不同的变元，t_{\mathrm{1}},t_{\mathrm{2}},\cdots ,t_n是项，且t_i\ne x_i(i=\mathrm{1,2},\cdots ,n)，则称\sigma =\{t_{\mathrm{1}}/x_{\mathrm{1}},t_{\mathrm{2}}/x_{\mathrm{2}},\cdots ,t_n/x_n\}为替换。

设文字P_i=P_{\mathrm{1}}(x_{\mathrm{1}},x_{\mathrm{2}},x_{\mathrm{3}})和Q_j=\sim P_{\mathrm{1}}(a,b,f(b))可以构成一组互补对文字，则替换为\sigma =\{a/x_{\mathrm{1}},b/x_{\mathrm{2}},f(b)/x_{\mathrm{3}}\}。

定义4 合一^[25]：设\{L_{\mathrm{1}},L_{\mathrm{2}},\cdots ,L_n\}是一组文字，\sigma是一个替换，若L_{\mathrm{1}}\sigma =L_{\mathrm{2}}\sigma =\cdots =L_n\sigma，则称\{L_{\mathrm{1}},L_{\mathrm{2}},\cdots ,L_n\}是可合一的。

设一组文字\{L_{\mathrm{1}}=P_{\mathrm{1}}(x_{\mathrm{1}}),L_{\mathrm{2}}=P_{\mathrm{1}}(x_{\mathrm{2}}),L_{\mathrm{3}}=P_{\mathrm{1}}(x_{\mathrm{3}})\}，则文字P_{\mathrm{1}}(x_{\mathrm{1}})、P_{\mathrm{1}}(x_{\mathrm{2}})和P_{\mathrm{1}}(x_{\mathrm{3}})通过替换\sigma =\{x_{\mathrm{1}}/x_{\mathrm{2}},x_{\mathrm{1}}/x_{\mathrm{3}}\}可合一为P_{\mathrm{1}}(x_{\mathrm{1}})。

定义5 归结原理^[3]：设C_{\mathrm{1}}，C_{\mathrm{2}}是两个无公共变量的子句，C_{\mathrm{1}}=P_{\mathrm{1}}\vee \cdots \vee P_m，C_{\mathrm{2}}=Q_{\mathrm{1}}\vee \cdots \vee Q_n，m和n分别代表C_{\mathrm{1}}和C_{\mathrm{2}}子句的文字总数。若P_i与Q_j存在合一互补，记作替换\sigma（可为空替换、变元更名替换、其他项替换），则称R(C_{\mathrm{1}},C_{\mathrm{2}})=(C_{\mathrm{1}}^{\sigma }-P_i^{\sigma })\vee (C_{\mathrm{2}}^{\sigma }-Q_j^{\sigma })为C_{\mathrm{1}}，C_{\mathrm{2}}的归结式，其中，\mathrm{1}\le i\le m，\mathrm{1}\le j\le n。

设子句C_{\mathrm{1}}=P_{\mathrm{1}}(a)\vee P_{\mathrm{2}}(b)和子句C_{\mathrm{2}}=\sim P_{\mathrm{2}}(x_{\mathrm{2}})\vee P_{\mathrm{1}}(f(x_{\mathrm{2}}))进行二元归结，可知P_{\mathrm{2}}(b)与\sim P_{\mathrm{2}}(x_{\mathrm{2}})存在合一互补，替换为\sigma =\{b/x_{\mathrm{2}}\}，则子句C_{\mathrm{1}}替换后为C_{\mathrm{1}}^{\sigma }=P_{\mathrm{1}}(a)\vee P_{\mathrm{2}}(b)，子句C_{\mathrm{2}}替换后为C_{\mathrm{2}}^{\sigma }=\sim P_{\mathrm{2}}(b/x_{\mathrm{2}})\veeP_{\mathrm{1}}(f(b/x_{\mathrm{2}}))，生成的归结式为R(C_{\mathrm{1}},C_{\mathrm{2}})=P_{\mathrm{1}}(a)\vee P_{\mathrm{1}}(f(b))。

归结原理的核心为二元归结，即每个演绎步骤仅限于两个子句，仅消去一组互补对文字，其仍为当前一阶逻辑自动定理证明器采用的核心推理方法，例如Iprover^[26]、Vampire^[27]、Eprover、Prover9等。

定义6 矛盾体分离规则^[12]：设一阶逻辑子句集S=\{C_{\mathrm{1}},C_{\mathrm{2}},\cdots ,C_m\}，下面条件成立时：

1） C_{\mathrm{1}},C_{\mathrm{2}},\cdots ,C_m之间不含相同的变元，若相同，则需对这些变元进行更名。

2） 对子句集中的每个子句C_i，i=\mathrm{1,2},\cdots ,m，一个替换{\sigma }_i应用于C_i（{\sigma }_i可以是空替换）使得C_i相同的文字合并，记作子句C_{{}_i}^{{\sigma }_i}。将C_{{}_i}^{{\sigma }_i}的文字分成不含相同文字的两部分C_{{}_i}^{{\sigma }_i-}（不能为空）和C_{{}_i}^{{\sigma }_i+}（可以为空），其中：对任意(x_{\mathrm{1}},\cdots ,x_m)\in {\displaystyle \prod _{i=\mathrm{1}}^m}{C}_{{}_i}^{{\sigma }_i-}，存在至少一对互补对文字，则称{\wedge }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i-}为标准矛盾体，且称{\vee }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i+}={\mathbb{C}}_m^{\sigma }(C_{\mathrm{1}},\cdots ,C_m)为矛盾体分离式（其中，m表示参与演绎的子句数量，\sigma ={\cup }_{i=\mathrm{1}}^m{\sigma }_i），该演绎方法称为矛盾体分离规则。

相较于二元归结，矛盾体分离规则展现出本质上的差异，其多元演绎特性使得每次演绎可涉及多个子句^[13]，且新子句通过分离标准矛盾体的方式得到。

例1 设一阶逻辑子句集S=\{C_{\mathrm{1}},C_{\mathrm{2}},C_{\mathrm{3}},C_{\mathrm{4}},\}，其中，C_{\mathrm{1}}=P_{\mathrm{1}}(a_{\mathrm{1}})\vee P_{\mathrm{2}}(f_{\mathrm{1}}(a_{\mathrm{2}}),x_{\mathrm{1}})，C_{\mathrm{2}}=P_{\mathrm{2}}(a_{\mathrm{1}},a_{\mathrm{2}})\veeP_{\mathrm{2}}(f_{\mathrm{1}}(a_{\mathrm{2}}),x_{\mathrm{2}})，C_{\mathrm{3}}=P_{\mathrm{1}}(f_{\mathrm{2}}(a_{\mathrm{2}}))\vee \sim P_{\mathrm{2}}(x_{\mathrm{3}},x_{\mathrm{4}})\vee P_{\mathrm{3}}(a_{\mathrm{1}},x_{\mathrm{5}})\vee P_{\mathrm{3}}(x_{\mathrm{3}},a_{\mathrm{3}})\vee \sim P_{\mathrm{1}}(a_{\mathrm{1}})，C_{\mathrm{4}}=P_{\mathrm{1}}(f_{\mathrm{2}}(a_{\mathrm{2}}))\vee \sim P_{\mathrm{2}}(x_{\mathrm{7}},x_{\mathrm{8}})\vee \sim P_{\mathrm{3}}(a_{\mathrm{1}},a_{\mathrm{3}})\vee \sim P_{\mathrm{1}}(x_{\mathrm{6}})。其中，a_{\mathrm{1}},a_{\mathrm{2}},a_{\mathrm{3}}为常元项，f_{\mathrm{1}},f_{\mathrm{2}}为函数项，x_{\mathrm{1}},x_{\mathrm{2}},x_{\mathrm{3}},x_{\mathrm{4}},x_{\mathrm{5}},x_{\mathrm{6}},x_{\mathrm{7}},x_{\mathrm{8}}为变元项。

依次选取C_{\mathrm{1}},C_{\mathrm{2}},C_{\mathrm{3}},C_{\mathrm{4}}参与多元矛盾体分离演绎，得到矛盾体分离式。多元演绎过程如表1所示，分离的标准矛盾体为P_{\mathrm{1}}(a_{\mathrm{1}})\wedge P_{\mathrm{2}}(a_{\mathrm{1}},a_{\mathrm{2}})\wedge (~P_{\mathrm{2}}(a_{\mathrm{1}}/x_{\mathrm{3}},a_{\mathrm{2}}/x_{\mathrm{4}})\vee P_{\mathrm{3}}(a_{\mathrm{1}},a_{\mathrm{3}}/x_{\mathrm{5}})\vee P_{\mathrm{3}}(a_{\mathrm{1}}/x_{\mathrm{3}},a_{\mathrm{3}})\vee ~P_{\mathrm{1}}(a_{\mathrm{1}}))\wedge(~P_{\mathrm{2}}(a_{\mathrm{1}}/x_{\mathrm{7}},a_{\mathrm{2}}/x_{\mathrm{8}})\vee \sim P_{\mathrm{3}}(a_{\mathrm{1}},a_{\mathrm{3}})\vee ~P_{\mathrm{1}}(a_{\mathrm{1}}/x_{\mathrm{6}}))，剩余文字取因子操作后得到的新子句为P_{\mathrm{2}}(f_{\mathrm{1}}(a_{\mathrm{2}}),x_{\mathrm{1}}/x_{\mathrm{2}})\vee P_{\mathrm{1}}(f_{\mathrm{2}}(a_{\mathrm{2}}))。

传统的二元归结方法受到子句数量的限制，其新子句的生成是通过消去两个子句中的互补文字实现的。因此，当原始子句包含较多的文字数时，生成的新子句常保留较多的文字数量。这一特性使得在子句集较大或子句本身较复杂的情况下，演绎效率受到限制。

相比之下，多元矛盾体分离演绎通过构建标准矛盾体，能更好地发挥子句间的协同演绎能力，更准确地反映问题本身的逻辑关系。标准矛盾体由参与演绎的子句共同构成的多个子标准矛盾体组成，其文字规模大于仅由互补对文字所构建的规模。因此，矛盾体分离规则能够更有效地消去多个子标准矛盾体，从而具备更强的文字消元能力，并可能显著提升演绎效率。

2　 单元子句在矛盾体分离规则中的演绎性质及框架

2.1　单元子句在矛盾体分离规则中的演绎性质

一阶逻辑子句集的证明过程为应用一系列推理规则搜索出一条演绎到空子句的演绎路径，即生成的新子句文字数为0。矛盾体分离规则是一种真正意义上的多元动态演绎方法，当参与演绎的子句确定时，构建的标准矛盾体越大，则生成的新子句所含的文字数越少。对于传统的二元演绎方法，若需生成空子句，则需要两个单元子句参与演绎且所含的文字为一组互补对文字；对于多元矛盾体分离演绎，若需演绎生成空子句，也至少需要有一个单元子句参与演绎，且单元子句参与演绎具有较好的文字消元能力。因此，单元子句在一阶逻辑自动定理证明中具有特殊的地位，对子句消元和演绎生成空子句具有重要的作用。

在多元矛盾体分离规则中，单元子句参与演绎具有特殊的演绎性质。

定理1 单元子句多元演绎定理 设一阶逻辑子句集S=\{C_{\mathrm{1}},C_{\mathrm{2}},\cdots ,C_m\}，对任意的子句C_i，i=\mathrm{1,2},\cdots ,m，在已构建的标准矛盾体{\wedge }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i-}中加入单元子句C_j中的文字x_{m+\mathrm{1}}，其新构建的{\wedge }_{i=\mathrm{1}}^{m+\mathrm{1}}{C}_{{}_i}^{{\sigma }_i-}仍为标准矛盾体，且与C_j中的文字加入标准矛盾体{\wedge }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i-}中的顺序无关。

证 因为{\wedge }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i-}为标准矛盾体，则对任意(x_{\mathrm{1}},\cdots ,x_m)\in {\displaystyle \prod _{i=\mathrm{1}}^m}{C}_{{}_i}^{{\sigma }_i-}一定存在互补对文字。加入单元子句C_j中的文字x_{m+\mathrm{1}}后得{\wedge }_{i=\mathrm{1}}^{m+\mathrm{1}}{C}_{{}_i}^{{\sigma }_i-}，任意(x_{\mathrm{1}},\cdots ,x_m,x_{m+\mathrm{1}})\in {\displaystyle \prod _{i=\mathrm{1}}^{m+\mathrm{1}}}{C}_{{}_i}^{{\sigma }_i-}仍包含原标准矛盾体{\wedge }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i-}中的互补对文字，则{\wedge }_{i=\mathrm{1}}^{m+\mathrm{1}}{C}_{{}_i}^{{\sigma }_i-}为标准矛盾体，且x_{m+\mathrm{1}}插入x_{\mathrm{1}},\cdots ,x_m中任意位置，均不影响其构成标准矛盾体，即满足任意(x_{\mathrm{1}},\cdots ,x_m,x_{m+\mathrm{1}})\in {\displaystyle \prod _{i=\mathrm{1}}^{m+\mathrm{1}}}{C}_{{}_i}^{{\sigma }_i-}存在互补对文字。定理1得证。

注：在标准矛盾体中，加入任意多个子句中的一个或多个文字，其构建后仍为标准矛盾体。

定理2 单元子句多元演绎分离式定理 设一阶逻辑子句集S=\{C_{\mathrm{1}},C_{\mathrm{2}},\cdots ,C_m\}，对任意的子句C_i，i=\mathrm{1,2},\cdots ,m，在已构建的标准矛盾体{\wedge }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i-}中加入单元子句C_j中的文字，其新构建的\mathrm{S}\mathrm{u}\mathrm{m}({\vee }_{i=\mathrm{1}}^{m+\mathrm{1}}{C}_{{}_i}^{{\sigma }_i+})\le \mathrm{S}\mathrm{u}\mathrm{m}({\vee }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i+})，其中Sum代表文字的总和。

证 根据定理1，{\wedge }_{i=\mathrm{1}}^{m+\mathrm{1}}{C}_{{}_i}^{{\sigma }_i-}为标准矛盾体。若单元子句C_j中的文字与{\vee }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i+}中的文字存在合一互补对，则；若单元子句C_j中的文字与{\vee }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i+}中的文字不存在合一互补对，则\mathrm{S}\mathrm{u}\mathrm{m}({\vee }_{i=\mathrm{1}}^{m+\mathrm{1}}{C}_{{}_i}^{{\sigma }_i+})=\mathrm{S}\mathrm{u}\mathrm{m}({\vee }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i+})。定理2得证。

定理3 单元子句集多元演绎定理 设一阶逻辑子句集S=\{C_{\mathrm{1}},C_{\mathrm{2}},\cdots ,C_m\}，对任意的子句C_i，i=\mathrm{1,2},\cdots ,m，将含K个单元子句的单元子句集\{C_j,\cdots ,C_{j+k-\mathrm{1}}\}（其中j\in N^{+}）中的文字x_j,\cdots ,x_{j+k-\mathrm{1}}加入已构建的标准矛盾体{\wedge }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i-}中，其新构建的{\wedge }_{i=\mathrm{1}}^{m+k}{C}_{{}_i}^{{\sigma }_i-}仍为标准矛盾体，且与\{C_j,\cdots ,C_{j+k-\mathrm{1}}\}中的文字加入标准矛盾体{\wedge }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i-}中的顺序无关。

证 因为{\wedge }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i-}为标准矛盾体，则对任意(x_{\mathrm{1}},\cdots ,x_m)\in {\displaystyle \prod _{i=\mathrm{1}}^m}{C}_{{}_i}^{{\sigma }_i-}一定存在互补对文字。将含K个单元子句的单元子句集\{C_j,\cdots ,C_{j+k-\mathrm{1}}\}中的文字x_j,\cdots ,x_{j+k-\mathrm{1}}加入{\wedge }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i-}后得{\wedge }_{i=\mathrm{1}}^{m+k}{C}_{{}_i}^{{\sigma }_i-}，任意(x_{\mathrm{1}},\cdots ,x_m,x_j,\cdots ,x_{j+k-\mathrm{1}})\in {\displaystyle \prod _{i=\mathrm{1}}^{m+k}}{C}_{{}_i}^{{\sigma }_i-}仍包含原标准矛盾体{\wedge }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i-}中的互补对文字，则{\wedge }_{i=\mathrm{1}}^{m+k}{C}_{{}_i}^{{\sigma }_i-}为标准矛盾体，且\{C_j,\cdots ,C_{j+k-\mathrm{1}}\}中的文字x_j,\cdots ,x_{j+k-\mathrm{1}}插入x_{\mathrm{1}},\cdots ,x_m中任意位置，均不影响其构成标准矛盾体，即满足任意(x_{\mathrm{1}},\cdots ,x_m,x_j,\cdots ,x_{j+k-\mathrm{1}})\in {\displaystyle \prod _{i=\mathrm{1}}^{m+k}}{C}_{{}_i}^{{\sigma }_i-}存在互补对文字，定理3得证。

定理4 单元子句集多元演绎分离式定理 设一阶逻辑子句集S=\{C_{\mathrm{1}},C_{\mathrm{2}},\cdots ,C_m\}，对任意的子句C_i，i=\mathrm{1,2},\cdots ,m，在已构建的标准矛盾体{\wedge }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i-}中加入单元子句集\{C_j,\cdots ,C_{j+k-\mathrm{1}}\}（共K个单元子句）中的文字，其新构建的\mathrm{S}\mathrm{u}\mathrm{m}({\vee }_{i=\mathrm{1}}^{m+k}{C}_{{}_i}^{{\sigma }_i+})\le \mathrm{S}\mathrm{u}\mathrm{m}({\vee }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i+})，其中Sum代表文字的总和。

证 根据定理3，{\wedge }_{i=\mathrm{1}}^{m+k}{C}_{{}_i}^{{\sigma }_i-}为标准矛盾体。若单元子句集\{C_j,\cdots ,C_{j+k-\mathrm{1}}\}（共K个单元子句）中的文字与{\vee }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i+}中的文字存在合一互补对，则；若单元子句集\{C_j,\cdots ,C_{j+k-\mathrm{1}}\}（共K个单元子句）中的文字与{\vee }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i+}中的文字不存在合一互补对，则\mathrm{S}\mathrm{u}\mathrm{m}({\vee }_{i=\mathrm{1}}^{m+k}{C}_{{}_i}^{{\sigma }_i+})=\mathrm{S}\mathrm{u}\mathrm{m}({\vee }_{i=\mathrm{1}}^m{C}_{{}_i}^{{\sigma }_i+})；定理4得证。

2.2　基于单元子句的多元矛盾体分离动态演绎框架

在多元矛盾体分离规则中，构建的标准矛盾体越大，其文字消去能力越强，即推理能力越强。根据定理1和定理3，单元子句可灵活参与多元演绎，能有效提升构造的标准矛盾体大小；根据定理2和定理4，单元子句参与演绎不会增加矛盾体分离式的文字总数。因此，充分使用子句集中的单元子句参与多元演绎，能有效提升多元演绎的推理能力。

为了充分发挥子句集中单元子句参与多元矛盾体分离演绎的能力，基于定理1~4，提出了一种基于单元子句的多元矛盾体分离动态演绎框架，在定理证明过程中，该框架将子句集分为单元子句集和非单元子句集，优先选取单元子句集中的单元子句，随后不断选取非单元子句进行多元动态演绎，当生成的矛盾体分离式为单元子句时，则加入单元子句集；当生成的矛盾体分离式为非单元子句时，则加入非单元子句集；当生成的矛盾体分离式为空时，则得出不可满足结论；否则，当达到设定的时间阈值时，演绎结束。

3　 单元子句选择策略

在一阶逻辑自动定理判定过程中，由于子句中共享变元的存在，不同的单元子句参与演绎顺序会生成不同的演绎分离式。

例2 设一阶逻辑子句集S=\{C_{\mathrm{1}},C_{\mathrm{2}},C_{\mathrm{3}},C_{\mathrm{4}},\}，C_{\mathrm{1}}=\sim P_{\mathrm{1}}(a_{\mathrm{1}})，C_{\mathrm{2}}=P_{\mathrm{2}}(f_{\mathrm{1}}(a_{\mathrm{2}}))，C_{\mathrm{3}}=P_{\mathrm{3}}(a_{\mathrm{3}})，C_{\mathrm{4}}=P_{\mathrm{1}}(x_{\mathrm{1}})\vee \simP_{\mathrm{2}}(x_{\mathrm{2}})\vee \sim P_{\mathrm{3}}(x_{\mathrm{1}})。其中，a_{\mathrm{1}},a_{\mathrm{2}}为常元项，f_{\mathrm{1}}为函数项，x_{\mathrm{1}},x_{\mathrm{2}}为变元项。

按照单元子句C_{\mathrm{1}},C_{\mathrm{2}},C_{\mathrm{3}}参与演绎顺序，选取非单元子句C_{\mathrm{4}}参与演绎，存在替换\sigma =\{a_{\mathrm{1}}/x_{\mathrm{1}},f_{\mathrm{1}}(a_{\mathrm{2}})/x_{\mathrm{2}}\}，则生成的矛盾体分离式为C_{\mathrm{5}}=\sim P_{\mathrm{3}}(a_{\mathrm{1}})。

按照单元子句C_{\mathrm{2}},C_{\mathrm{3}},C_{\mathrm{1}}参与演绎顺序，选取非单元子句C_{\mathrm{4}}参与演绎，存在替换\sigma =\{f_{\mathrm{1}}(a_{\mathrm{2}})/x_{\mathrm{2}},a_{\mathrm{3}}/x_{\mathrm{1}}\}，则生成的矛盾体分离式为C_{\mathrm{5}}=P_{\mathrm{1}}(a_{\mathrm{3}})。

为了有效提升多元矛盾体分离演绎效率，应使每次的多元动态演绎具有不同的单元子句排列顺序，避免重复路径的搜索。在多元演绎一阶逻辑子句集判定过程中，刻画单元子句不同的属性，通过多属性值确定单元子句参与演绎的顺序，以使得多元演绎搜索不同的演绎路径。

定义7 单元子句静态属性 设一阶逻辑子句集S=\{C_{\mathrm{1}},C_{\mathrm{2}},\cdots ,C_m\}，随着单元子句C_i(i\in \{\mathrm{1,2},\cdots ,m\})参与演绎，C_i保持不变的属性称为单元子句静态属性。

定义8 单元子句动态属性 设一阶逻辑子句集S=\{C_{\mathrm{1}},C_{\mathrm{2}},\cdots ,C_m\}，随着单元子句C_i(i\in \{\mathrm{1,2},\cdots ,m\})参与演绎，C_i发生变化的属性称为单元子句动态属性。

单元子句选择策略通过刻画单元子句的不同属性值并进行组合排序实现，其包含的属性有：

1） 函数项复杂度。函数项复杂度是一阶逻辑自动定理判定过程中增加演绎复杂性的重要因素之一，其计算方法为该单元子句所含的函数项深度总和。为了有效控制多元矛盾体分离演绎过程由简单逐步到复杂，应优先选取函数项复杂度CFC(Clause Function Complexity)小的单元子句参与多元动态演绎。该属性属于单元子句静态属性。

例3 计算单元子句的C_{\mathrm{1}}=\sim P_{\mathrm{1}}(f_{\mathrm{1}}(f_{\mathrm{1}}(f_{\mathrm{1}}(f_{\mathrm{1}}(a_{\mathrm{1}})))))和C_{\mathrm{2}}=P_{\mathrm{2}}(f_{\mathrm{2}}(f_{\mathrm{1}}(f_{\mathrm{1}}(a_{\mathrm{1}}))),f_{\mathrm{1}}(f_{\mathrm{1}}(a_{\mathrm{2}})))的函数项复杂度。

对于单元子句C_{\mathrm{1}}，函数项复杂度\mathrm{C}\mathrm{F}\mathrm{C}(C_{\mathrm{1}})=\mathrm{4}+\mathrm{3}+\mathrm{2}+\mathrm{1}=\mathrm{10}；对于单元子句C_{\mathrm{2}}，函数项复杂度\mathrm{C}\mathrm{F}\mathrm{C}(C_{\mathrm{2}})=\mathrm{3}+\mathrm{2}+\mathrm{1}+\mathrm{2}+\mathrm{1}=\mathrm{9}。

2） 变元活跃度。多元矛盾体分离演绎有效路径搜索不仅需要正确地选择子句参与演绎，同时也需正确地确定演绎的变元替换项，因此，变元项是一阶逻辑自动定理判定的重要逻辑符号。变元活跃度用于刻画单元子句中的变元分布情况，其计算方法为不同变元项总数与变元项总数的比值，其中不含变元的单元子句变元活跃度VA（Variable Activity）为0。该属性为单元子句的静态属性。

例4 计算单元子句的C_{\mathrm{1}}=\sim P_{\mathrm{1}}(a_{\mathrm{1}})、C_{\mathrm{2}}=P_{\mathrm{2}}(f_{\mathrm{1}}(x_{\mathrm{1}}),x_{\mathrm{2}})和C_{\mathrm{3}}=P_{\mathrm{3}}(x_{\mathrm{3}},x_{\mathrm{4}},f_{\mathrm{2}}(x_{\mathrm{3}}),x_{\mathrm{5}})的变元活跃度。

对于单元子句C_{\mathrm{1}}，变元活跃度\mathrm{V}\mathrm{A}(C_{\mathrm{1}})=\mathrm{0}；对于单元子句C_{\mathrm{2}}，变元活跃度\mathrm{V}\mathrm{A}(C_{\mathrm{2}})=\mathrm{2}/\mathrm{2}=\mathrm{1}；对于单元子句C_{\mathrm{3}}，变元活跃度\mathrm{V}\mathrm{A}(C_{\mathrm{3}})=\mathrm{3}/\mathrm{4}。

为了使含有变元项的单元子句较好地参与多元动态演绎，应优先选取变元活跃度高的单元子句。

3） 演绎次数。在一阶逻辑自动定理证明过程中，记录单元子句参与多元动态演绎的有效演绎历史信息非常重要，它是有效规划单元子句参与多元演绎顺序的重要度量值。当该单元子句参与多元演绎一次，该演绎次数属性值加1，该属性值能有效用于指导单元子句公平地参与多元动态演绎。为了有效选择较优的单元子句参与演绎，在设定的时间到达时，通过设定阈值的方式对该属性值重新置初始值。由于定理证明过程中单元子句会被动态地选取参与演绎，因此该属性为单元子句的动态属性。

4） 冗余次数。冗余子句处理是一阶逻辑自动定理证明重要的研究内容，其核心在于基于子句的冗余性调整演绎路径搜索策略。在多元动态演绎过程中，若单元子句的参与导致生成冗余新子句，则应减少该单元子句的后续参与。因此，记录单元子句参与多元动态演绎时产生的无效演绎历史（即生成冗余新子句的情况）至关重要，这一指标是规划单元子句参与多元演绎的关键依据。当单元子句参与多元演绎导致生成冗余子句时，其冗余次数属性值加1。该属性值能有效避免单元子句重复触发无效演绎。由于一阶逻辑子句集在演绎过程中会迅速增大，为了使已产生较多无效演绎的单元子句在新的子句集下重新参与演绎，系统会在设定的时间到达时，通过设定阈值的方式将该属性值重置为初始值。这一属性属于单元子句动态属性。

单元子句的选择策略首先对子句集中单元子句的多属性值组合进行排序，随后依次选取排序后的单元子句参与演绎。为了优先选择参与演绎次数较少、产生无效演绎较少、演绎替换较为简单以及含有较简单变元项的单元子句，本文采用的单元子句优先选择顺序如下：演绎次数，冗余次数，函数项复杂度，变元活跃度。优先选择演绎次数较少的单元子句，当单元子句演绎次数相同时，优先选择冗余次数较少的单元子句；当演绎次数与冗余次数都相同时，优先选择函数项复杂度小的单元子句；当演绎次数、冗余次数与函数项复杂度都相同时，优先选择变元活跃度高的单元子句；当上述四个度量值都相同时，优先选择子句编码小的单元子句，即优先选择原始子句集中的单元子句。

4　 本文算法

本文算法以子句集中的单元子句作为多元演绎的核心子句，通过单元子句选择策略依次选择单元子句参与多元演绎，然后在非单元子句集中依次选取演绎次数少且文字总数少的非单元子句参与演绎；在非单元子句参与演绎过程中，评估多元演绎生成的新子句的冗余性；若生成的新子句为冗余子句，则通过回溯机制重新选择新的非单元子句继续参与演绎，若生成的新子句为非冗余子句，则根据生成的新子句是否为单元子句或非单元子句分别加入到对应的子句集中；当演绎生成空子句时，则算法退出，即该一阶逻辑定理被证明；或当设定的判定时间到达时，则算法退出，生成基于单元子句的多元矛盾体分离演绎路径，可用于一阶逻辑自动定理的辅助证明。本文算法的流程如图1所示，具体实现步骤如下：

1） 通过单元子句选择策略在子句集中依次选取单元子句加入单元子句集UnitS（初始为空）中；根据前述非单元子句选择方法在子句集中依次选取非单元子句加入到非单元子句集NUnitS（初始为空）中；设定演绎算法框架。

2） 依次选取单元子句集UnitS中所有的单元子句，用于步骤4）的多元矛盾体分离动态演绎。

3） 依次选取非单元子句集NUnitS中的非单元子句，用于步骤4）的多元矛盾体分离动态演绎。

4） 在演绎过程中，标准矛盾体由所选子句中的文字依据矛盾体分离规则构建而成，其剩余文字的析取被用于形成矛盾体分离式R，即演绎生成新子句（创建新子句的子句、文字及项空间）。

5） 若R为空子句，该定理被证明，得出不可满足结论，算法转到步骤9）；若R不为空子句，则判断R的冗余性，若R为包含冗余子句或恒真子句，则参与当前候选子句协同演绎的单元子句冗余次数加1，通过回溯机制回退到当前演绎的上一个非单元子句参与的已完成的演绎步骤，再进行后续的演绎，其实现见如下回溯机制的处理。

回溯机制包括：清除参与本次演绎的子句中变元替换项；清除本次演绎标准矛盾体新增的文字；清除矛盾体分离式中新增的文字；清除演绎搜索路径表中新增的文字；标记当前选择的候选子句，在本次多元演绎中将不再被选取，算法转到步骤8）。

6） 若R为非冗余子句，则获得一条多元演绎搜索路径。此时，当前参与多元演绎的单元子句和非单元子句演绎次数分别加1；记录当前多元演绎产生替换的变元项；记录当前候选子句参与的多元演绎搜索路径。若R为单元子句，则计算R的函数项复杂度和变元活跃度，设定演绎次数和冗余次数的初始值，并将其加入对应位置的单元子句集中；若R为非单元子句，则初始化R的演绎次数，并将其加入到对应的非单元子句集中。最后，使用R对剩余子句集进行冗余子句处理。

7） 若达到预设的时间限制，则算法均转到步骤9）。否则，算法转到步骤3）。

8） 若NUnitS中所有非单元子句均已参与演绎，则算法均转到步骤9）；否则，算法转到步骤3）。

9） 算法结束，结束本次多元动态演绎。清除本次多元演绎所有变元项的替换项，清除矛盾体分离式和标准矛盾体列表，开始下一次新的多元动态演绎。

算法几点说明：

a) 单元子句的演绎顺序由第3节单元子句选择策略确定，该策略旨在避免重复路径的搜索，提升多元矛盾体分离演绎能力和效率。

b) 在算法执行前，通过遍历原始子句集计算单元子句的函数项复杂度和变元活跃度，并初始化演绎次数和冗余次数（值分别为0）。

c) 若子句集中不存在单元子句，则通过文字数较少的子句两两进行二元演绎，直至生成单元子句。

5　 实验

5.1　实验准备

为验证本文算法的有效性，将其应用至Eprover3.2和Prover9证明器中，记作UCSDA_Eprover3.2证明器和UCSDA_P证明器。本文分别将近两年国际定理证明器竞赛例作为问题集，每组500个，每个问题的测试时间为标准时间300 s，在一台计算机（Ubuntu 18.04.3 LTS，64位操作系统，配备Intel@ Xeon(R)W-2123 CPU@.60GHZx 8处理器及32 GB内存）进行对比测试。为了进一步评估UCSDA_Eprover3.2的推理能力，本文将测试范围扩大至TPTP（Thousands of Problems for Theorem Provers）问题库中难度系数为1且未被其他自动定理证明器证明的定理。

5.2　实验分析

5.2.1　UCSDA_Eprover3.2证明2023年国际竞赛例判定情况

1） UCSDA_Eprover3.2与Eprover3.2性能比较

图2呈现了UCSDA_Eprover3.2与Eprover3.2测试2023年竞赛例的性能对比。UCSDA_Eprover3.2证明了411个定理，相较于Eprover3.2多证明出15个定理。根据散点图的数据分析，在前120 s内，UCSDA_Eprover3.2与Eprover3.2的散点几乎重叠，但在120 s之后，UCSDA_Eprover3.2的散点数量明显多于Eprover3.2，定理证明的数量有所提升，这表明加入本文算法的UCSDA_Eprover3.2证明器的定理证明能力得到了有效的提升。

2） UCSDA_Eprover3.2证明Eprover3.2无法判定的定理分析

针对2023年国际竞赛例，UCSDA_Eprover3.2能够证明Eprover3.2未证明的17个定理，占Eprover3.2未证明定理总数的16.35%，这17个定理证明情况如表2所示。由表2可知，平均证明时间为258.12 s，平均难度系数达到0.78，表明UCSDA_Eprover3.2在证明较难问题上具有较好的能力和效率。在证明的17个定理中，平均函数项数量为201.12，平均子句数达到522.82，其中有10个定理的变元总数超过800。以上实验数据表明，UCSDA_Eprover3.2证明器能较好地判定较大规模的子句集且含较多变元项的一阶逻辑问题。需要指出的是，UCSDA_Eprover3.2能够证明17个Eprover3.2无法证明的定理，而Eprover3.2仅能证明UCSDA_Eprover3.2未能证明的2个定理。由此可见，UCSDA_Eprover3.2的证明能力优于Eprover3.2。

5.2.2　UCSDA_Eprover3.2证明2024年国际竞赛例判定情况

1） UCSDA_Eprover3.2与Eprover3.2性能比较

图3呈现了UCSDA_Eprover3.2与Eprover3.2测试2024年竞赛例的性能对比。Eprover3.2证明了377个定理，平均用时12.239 3 s；UCSDA_Eprover3.2证明了391个定理，相较于Eprover3.2多证明了14个定理；在证明相同数量（377个）定理时，UCSDA_Eprover3.2平均用时11.703 8 s，比Eprover3.2的平均证明时间节省了0.535 5 s。通过上述实验数据可得，本文提出的算法，在定理证明效率方面表现出一定的优势，并能有效提升证明器的证明能力。

2） UCSDA_Eprover3.2证明Eprover3.2无法判定的定理分析

在Eprover3.2未证明的123个定理中，UCSDA_Eprover3.2证明了15个定理（判定情况如表3所示），占Eprover3.2未证明定理总数的12.195%，平均证明时间为220.44 s，平均难度系数达到0.79，平均函数项数量为252.4，平均子句数达到772.07，平均变元个数为1 900。定理ITP006+5的变元个数达到15 531，难度系数为0.91，子句数量为4 453，函数项个数超过1 200，证明时间为285.45 s。值得注意的是，UCSDA_Eprover3.2能证明15个Eprover3.2未能证明的定理，而Eprover3.2只能证明UCSDA_Eprover3.2未能证明的1个定理。以上实验数据表明，UCSDA_Eprover3.2证明器能较好地判定较大规模的子句集且含较多变元项的一阶逻辑问题。

5.2.3　UCSDA_P证明2023年国际竞赛例判定情况

1） UCSDA_P与Prover9性能比较

图4呈现了UCSDA_P与Prover9测试2023年竞赛例的性能对比，UCSDA_P证明了204个定理，Prover9证明了133个定理，即UCSDA_P相比Prover9多证明了71个定理，占Prover9证明定理总数的53.38%，表明该算法能较好地提升Prover9的定理证明能力。相比Prover9，UCSDA_P加入了多元矛盾体分离演绎，因此能有效提升单元子句的推理能力，通过回溯机制搜索较优的多元演绎路径。

2） UCSDA_P证明Prover9无法判定的定理分析

为深入分析UCSDA_P在定理证明能力上的优势，本文对其与Prover9的定理情况进行对比分析。实验结果表明，UCSDA_P证明的204个定理中，有99个未被Prover9证明，其分别占UCSDA_P和Prover9证明总数的48.53%与74.44%。因此，本文提出的算法能有效搜索Prover9未被搜索到的有效路径，从而使得UCSDA_P证明器具有更强的定理证明能力。

图5为UCSDA_P证明器证明Prover9无法判定的99个定理的难度系数图。由图5可知，这些定理难度系数介于0.21和0.85之间。在UCSDA_P证明Prover9无法判定的这99个定理中，有44个定理的难度系数大于0.5，占这99个定理总数的44.44%；有15个定理的难度系数达到0.7及以上，占99个定理总数的15.15%。实验表明，UCSDA_P证明器不仅能有效判定较为复杂的定理，还具有较高的证明效率，因此，本文算法具有较强的演绎推理能力。

5.2.4　UCSDA_Eprover3.2对难度系数为1的定理的实验分析

为了进一步评估本文算法（UCSDA）在未证明问题领域的判定有效性，对TPTP库中rating为1的问题进行了测试，测试判定结果如表4所示。结果显示，UCSDA_Eprover3.2证明了8个其他证明器均未能证明的定理。这些定理平均子句个数高达2 522.75，平均文字个数达到17 563.13，平均函数项个数为434.38，平均证明时间为170.40 s。定理SEU410+3包含19 045个子句，文字数量达到138 191个，并且含2 902个函数项，证明时间仅为189.85 s。实验结果表明，本文算法能高效搜索出这些难问题的有效证明路径，使得UCSDA_Eprover3.2证明器在证明高难度逻辑问题上表现出较好的有效性。

6　 结 语

针对当前一阶逻辑自动定理证明器仍然依赖于二元演绎方法的问题，基于单元子句在一阶逻辑定理证明过程中的特殊性质，本文提出了单元子句在多元演绎中构建标准矛盾体的演绎性质，给出了多元演绎中的单元子句选择策略，以优化其参与演绎的顺序，并提出了一种基于单元子句的多元矛盾体分离动态演绎算法，该算法能有效提升单元子句的演绎推理能力，并搜索较优演绎路径。为验证该算法的有效性和实用性，将其应用于Eprover3.2和Prover9中，实验表明，改进后的证明器UCSDA_Eprover3.2和UCSDA_P在定理证明能力上均有较好的提升，并证明了8个TPTP库中此前未被证明的难度系数为1的定理，验证了该算法在一阶逻辑自动定理证明中的有效性。

在多元动态演绎过程中，不同的非单元子句参与多元演绎的顺序具有不同的搜索路径，对多元演绎定理证明能力具有重要的影响。因此，进一步完善与优化非单元子句选择策略是下一步研究的重点内容。与此同时，单元子句在多元演绎中具有较好的演绎特性，应充分发挥其推理能力。因此，研究较多单元子句充分参与多元动态演绎以提升自动定理证明能力仍是下一步研究的重点内容。

参考文献

[1] SIMIĆ D， MARIĆ F， BOUTRY P. Formalization of the poincaré disc model of hyperbolic geometry［J］. Journal of Automated Reasoning， 2021， 65（1）： 31-73. DOI：10.1007/s10817-020-09551-2 .

[2] 曹钦翔， 詹博华， 赵永望. 定理证明理论与应用专题前言［J］. 软件学报， 2022， 33（6）： 2113-2114. DOI： 10.13328/j.cnki.jos.006582 .

[3] CAO Q X， ZHAN B H， ZHAO Y W. Special topic on theorem proving： Theory and applications Preface［J］. Journal of Software， 2022， 33（6）： 2113-2114. DOI： 10.13328/j.cnki.jos.006582（Ch ）.

[4] ROBINSON J A. A machine-oriented logic based on the resolution principle［J］. Journal of the ACM， 1965， 12（1）： 23-41. DOI：10.1145/321250.321253 .

[5] ROBINSON J A. Automatic deduction with hyper-resolution［J］. International Journal of Computing & Mathematics， 1965， 1（3）： 227-234. DOI：10.1007/978-3-642-81952-0_27 .

[6] SLAGLE J R. Automatic theorem proving with renamable and semantic resolution［J］. Journal of the ACM， 1967， 14（4）： 687-697. DOI：10.1145/321420.321428 .

[7] CHANG C L. The unit proof and the input proof in theorem proving［J］. Journal of the ACM， 1970， 17（4）： 698-707. DOI：10.1145/321607.321618 .

[8] BOYER R S. Locking： A restriction of resolution［D］. Austin： The University of Texas at Austin， 1971.

[9] OVERBEEK R， MCCHAREN J， WOS L. Complexity and related enhancements for automated theorem-proving programs［J］. Computers & Mathematics with Applications， 1976， 2（1）： 1-16. DOI：10.1016/0898-1221（76）90002-X .

[10] 刘叙华. 使用引理的锁语义归结原理——LI-归结原理［J］. 吉林大学学报（理学版）， 1979， 17（4）： 129-136.

[11] LIU X H. Lock-semantic resolution principle with lemmas—LI-resolution principle［J］. Journal of Jilin University（Science Edition）， 1979， 17（4）： 129-136 （Ch）.

[12] LOVELAND D W. A linear format for resolution［M］//Automation of Reasoning. Berlin： Springer， 1983： 399-416. DOI：10.1007/978-3-642-81955-1_25 .

[13] SLANEY J， WOLTZENLOGEL PALEO B. Conflict resolution： A first-order resolution calculus with decision literals and conflict-driven clause learning［J］. Journal of Automated Reasoning， 2018， 60（2）： 133-156. DOI：10.1007/s10817-017-9408-6 .

[14] XU Y， LIU J， CHEN S W， et al. Contradiction separation based dynamic multi-clause synergized automated deduction［J］. Information Sciences， 2018， 462： 93-113. DOI：10.1016/j.ins.2018.04.086 .

[15] XU Y， CHEN S W， LIU J， et al. Distinctive features of the contradiction separation based dynamic automated deduction［C］//Data Science and Knowledge Engineering for Sensing Decision Support. Belfast： WORLD SCIENTIFIC， 2018： 725-732. DOI： 10.1142/9789813273238_0092 .

[16] CAO F， XU Y， LIU J， et al. CSE_E 1.0： An integrated automated theorem prover for first-order logic［J］. Symmetry， 2019， 11（9）： 1142. DOI：10.3390/sym11091142 .

[17] CAO F， XU Y， CHEN S W， et al. A contradiction separation dynamic deduction algorithm based on optimized proof search［J］. International Journal of Computational Intelligence Systems， 2019， 12（2）： 1245-1254. DOI：10.2991/ijcis.d.191022.002 .

[18] 唐雷明， 白沐尘， 何星星， 等. 基于命题逻辑的完全标准矛盾体及最小标准矛盾体［J］. 计算机科学， 2020， 47（S2）： 83-85. DOI： 10.11896/jsjkx.200400072 .

[19] TANG L M， BAI M C， HE X X， et al. Complete contradiction and smallest contradiction based on propositional logic［J］. Computer Science， 2020， 47（S2）： 83-85. DOI： 10.11896/jsjkx.200400072（Ch ）.

[20] 曹锋， 徐扬， 陈树伟， 等. 多元协同演绎在一阶逻辑ATP中的应用［J］. 西南交通大学学报， 2020， 55（2）： 401-408. DOI： 10.3969/j.issn.0258-2724.20180800 .

[21] CAO F， XU Y， CHEN S W， et al. Application of multi-clause synergized deduction in first-order logic automated theorem proving［J］. Journal of Southwest Jiaotong University， 2020， 55（2）： 401-408. DOI： 10.3969/j.issn.0258-2724.20180800（Ch ）.

[22] CAO F， XU Y， LIU J， et al. A multi-clause dynamic deduction algorithm based on standard contradiction separation rule［J］. Information Sciences， 2021， 566： 281-299. DOI：10.1016/j.ins.2021.03.015 .

[23] 林玲瑜， 曹锋， 易见兵， 等. 基于子句活跃度和复杂度的多元动态演绎算法及应用［J］. 计算机工程与科学， 2023， 45（12）： 2256-2264. DOI： 10.3969/j.issn.1007-130X.2023.12.017 .

[24] LIN L Y， CAO F， YI J B， et al. A multi-clause dynamic deduction algorithm based on clause activity and complexity and its application［J］. Computer Engineering & Science， 2023， 45（12）： 2256-2264. DOI： 10.3969/j.issn.1007-130X.2023.12.017（Ch ）.

[25] 曹锋， 杨小玲， 易见兵， 等. 基于子句正负文字的多元演绎算法［J］. 华中科技大学学报（自然科学版）， 2025， 53（5）： 157-163. DOI： 10.13245/j.hust.250191 .

[26] CAO F， YANG X L， YI J B， et al. Multi-clause deduction algorithm based on positive and negative literals in clauses［J］. Journal of Huazhong University of Science and Technology （Natural Science Edition）， 2025， 53（5）： 157-163. DOI： 10.13245/j.hust.250191（Ch ）.

[27] 曹锋， 潘世成， 易见兵， 等. 子句充分性评估的多元动态演绎算法及应用［J］. 华中科技大学学报（自然科学版）， 2024， 52（11）： 153-160. DOI： 10.13245/j.hust.240468 .

[28] CAO F， PAN S C， YI J B， et al. Multi-clause dynamic deduction algorithm based on clause adequacy evaluation and its application［J］. Journal of Huazhong University of Science and Technology （Natural Science Edition）， 2024， 52（11）： 153-160. DOI： 10.13245/j.hust.240468（Ch ）.

[29] CHEN S W， XU Y， LIU J， et al. Clause reusing framework for contradiction separation based automated deduction［C］//Developments of Artificial Intelligence Technologies in Computation and Robotics. Cologne： World Scientific， 2020： 284-291. DOI： 10.1142/9789811223334_0035 .

[30] SCHULZ S， CRUANES S， VUKMIROVIĆ P. Faster， higher， stronger： E 2.3［M］//Automated Deduction — CADE 27. Cham： Springer International Publishing， 2019： 495-507. DOI：10.1007/978-3-030-29436-6_29 .

[31] GROZA A. Getting started with Prover9 and Mace4［M］//Modelling Puzzles in First Order Logic. Cham： Springer International Publishing， 2021： 1-9. DOI：10.1007/978-3-030-62547-4_1 .

[32] 王国俊. 数理逻辑引论与归结原理［M］. 第2版. 北京： 科学出版社， 2006.

[33] WANG G J. Introduction and resolution principle of mathematical logic［M］. 2nd Ed. Beijing： Science Press， 2006（Ch）.

[34] KOROVIN K， STICKSEL C. iProver-eq： An instantiation-based theorem prover with equality［M］//Automated Reasoning. Berlin： Springer， 2010： 196-202. DOI：10.1007/978-3-642-14203-1_17 .

[35] KOVÁCS L， VORONKOV A. First-order theorem proving and vampire［C］//Computer Aided Verification. Berlin： Springer， 2013： 1-35. DOI：10.1007/978-3-642-39799-8_1 .

基金资助

国家自然科学基金(62366017)

国家自然科学基金(62066018)

江西省教育厅科学技术研究项目(GJJ200818)

江西省教育厅科学技术研究项目(GJJ210828)

赣州市科技计划项目(GZKJ20206030)

江西理工大学博士启动基金(205200100060)