基于子句综合权重的多元动态演绎算法及应用

Multi-Clause Dynamic Deduction Algorithm and Application Based on Clause Comprehensive Weight

摘要

针对多元演绎如何有效选取子句，通过分析演绎前后项合一能力的变化，提出一种子句影响度的度量方法；通过分析子句影响度、剩余文字个数以及文字演绎能力对多元动态演绎过程的影响，提出一种子句综合权重的子句评估方法，能有效控制矛盾体分离式的文字个数；基于该子句评估方法，提出一种有效选择子句的多元动态演绎算法。将该算法应用到国际顶尖的一阶逻辑自动定理证明器Eprover3.1中，以最新的国际自动定理证明器竞赛例（FOF组）为测试对象，测试结果表明，加入了本文多元动态演绎算法的Eprover3.1比原始Eprover3.1多证明定理18个，且在难问题判定上，证明了8个其他证明器未能证明的定理。

Abstract

To solve the problem of effectively selecting clauses in multi-clause deduction, a measurement method for clause influence degree is proposed by analyzing the changes in unification ability before and after deduction. By analyzing the degree of influence of the clause, the number of remaining literals, and the literal deduction ability in the process of multi-clause dynamic deduction, a clause evaluation method based on the comprehensive weight of the clause is proposed, which can effectively control the number of literals in the contradiction separation clause. A multi-clause dynamic deduction algorithm is proposed to effectively select clauses based on this clause evaluation method.The proposed multi-clause dynamic deduction algorithm was applied to the international top first-order logic automated theorem prover Eprover3.1, taking the latest international automated theorem prover competition problems (FOF division) as the test objects. Eprover3.1 with the proposed multi-clause dynamic deduction algorithm outperformed the original Eprover3.1, which solved 18 more theorems than the original Eprover3.1. Regarding solving complex problems, Eprover3.1 with the proposed multi-clause dynamic deduction algorithm can solve 8 theorems that all other provers cannot solve.

Graphical abstract

关键词

多元演绎 / 子句评估 / 矛盾体分离式 / 一阶逻辑 / 自动定理证明器

Key words

multi-clause deduction / clause evaluation / contradiction separation clause / first-order logic / automated theorem prover

0　 引 言

一阶逻辑自动定理证明作为自动推理的重要分支^[1]，是人工智能领域重要的组成部分，通过对知识库中的规则和事实进行解析和推理，进而得出新的结论，其应用领域涉及程序验证^[2-4]、知识表示^[5-6]和数据查询^[7]等。Robinson^[8]提出了归结原理理论，推动了自动定理证明的发展，其核心为二元归结。Xu等^[9]提出了基于矛盾体分离的动态演绎推理理论，突破了静态的二元归结的限制，使演绎推理从二元静态演绎发展为多元动态演绎。多元演绎理论的提出和发展对自动定理证明研究具有重要的学术意义，为提升自动定理证明能力和效率提供了新的推理机制和演绎方法。

随着领域问题和实际问题越来越复杂，自动定理证明过程也随之变得复杂，在不同的演绎路径下产生的子句数量级差别巨大，因此，合理的子句选择策略以及文字选择策略对提升一阶逻辑自动定理证明器的能力和效率具有重要的意义和作用。学者们为此做了不少研究，曾国艳等^[10]将不同子句选择策略对应子句的不同属性，通过熵权法对子句属性进行客观赋权，在演绎过程中通过多属性决策方法对子句进行排序，得到子句完备序；Liu等^[11]提出通过充分使用二元子句并不断得到新的决策文字；当决策文字集中文字越多，其多元演绎的协同能力就越强；林玲瑜等^[12]对函数项的结构进行分析，通过函数项深度、函数项元数以及共享变元位置对函数项复杂度进行度量，从而得到子句复杂度的计算方法，能有效优化演绎搜索的路径，从而提升演绎的能力；Liu等^[13]在多元演绎中基于子句集中的文字互补情况，提出了一种文字充分使用次数的度量方法，并以此计算得到子句充分使用次数，能有效发挥子句间协同演绎的能力，从而提升多元动态演绎的能力和效率；Xu等^[14]根据多元矛盾体分离演绎规则，通过设定参与演绎的子句条件提出了矛盾体分离线性演绎、矛盾体分离单元演绎和矛盾体分离超演绎的定义和方法,实现了多元矛盾体分离演绎基础算法，该算法能有效提升一阶逻辑自动定理证明器的性能。

上述研究从子句演绎前的角度出发，通过子句属性及文字属性确定子句重复使用次数或者子句参与演绎的优先级，从而提高演绎的协同作用，但未从子句演绎后的角度刻画子句的属性，即不能较精准地控制标准矛盾体的演绎能力以及矛盾体分离式的文字个数，从而影响演绎能力和效率。因此，鉴于多元动态演绎具有多元性、动态性、协同性和可控性的演绎特点^[15]，本文通过刻画多元演绎过程中子句影响度、剩余文字个数对矛盾体分离式影响以及标准矛盾体中文字演绎能力，提出了一种基于子句综合权重的子句评估方法，能较好地提升标准矛盾体的演绎能力以及有效控制矛盾体分离式的文字个数，从而优化多元动态演绎的搜索路径；基于子句综合权重，提出了一种搜索路径由简单到复杂且充分发挥子句协同演绎的多元动态演绎算法，该算法能通过回溯机制优化演绎的搜索路径，进而提升演绎能力和效率，实验表明本文提出的算法能有效应用于一阶逻辑自动定理证明。

1　 基础知识

1.1　一阶逻辑理论

一阶逻辑是一种数理逻辑系统，其逻辑语言常见的基本元素有常元符、变元符、函数符以及谓词符。其中常元符表示固定化对象，常用字母a,b,c等表示；变元符表示具体化对象，常用字母x,y,z等表示；函数符表示对象的特征，常用字母f,g等表示，具有元数的概念，例如f\left(a\right)中的f是一元函数项符号；谓词符表示对象与对象之间的关系，常用字母P,Q等表示，也具有元数的概念，例如P(a)中的P是一元谓词项符号。

定义1 文字^[16]：在一阶逻辑中，若t_{\mathrm{1}},t_{\mathrm{2}},…,t_n是项，P是一个n元谓词符号，则称P\left(t_{\mathrm{1}},\dots ,t_n\right)是一个原子公式，也被称为文字。

定义2 子句^[16]：子句由文字的析取构成，其中不含有文字的子句称为空子句，记做\mathrm{\varnothing }；只含有一个文字的子句称为单元子句。

定义3 替换^[16]：在一阶逻辑中，x_{\mathrm{1}},x_{\mathrm{2}},…,x_n是不同的变元,t_{\mathrm{1}},t_{\mathrm{2}},…,t_n是项，且x_i≠t_i。称\sigma =\{t_{\mathrm{1}}/x_{\mathrm{1}},t_{\mathrm{2}}/x_{\mathrm{2}},\dots ,t_n/x_n\}为替换。

定义4 表达式的例^[16]：在一阶逻辑中，E是项或者E是原子公式，则称E是表达式。设\sigma =\{t_{\mathrm{1}}/x_{\mathrm{1}},t_{\mathrm{2}}/x_{\mathrm{2}},\dots ,t_n/x_n\}为替换。把E中属于\{x_{\mathrm{1}},x_{\mathrm{2}},\dots ,x_n\}的变元x_{i_{\mathrm{1}}},x_{i_{\mathrm{2}}},…,x_{i_k}分别用t_{i_{\mathrm{1}}},t_{i_{\mathrm{2}}},…,t_{i_k}去代换,将所得结果记为E\sigma，称为E经\sigma所得的例，简称表达式E的例。

定义5 合一^[16]：设\left\{E_{\mathrm{1}},E_{\mathrm{2}},\dots ,E_n\right\}是一组表达式，\sigma是一个替换。如果E_{\mathrm{1}}\sigma =E_{\mathrm{2}}\sigma =\dots =E_n\sigma，则称\left\{E_{\mathrm{1}},E_{\mathrm{2}},\dots ,E_n\right\}是可合一。

定义6 不可满足及满足^[16]：在一阶语言G中,若对任何解释I,都有I(G)=\mathrm{0},则称G不可满足；若存在一个解释使I(G)=\mathrm{1}，则称G可满足。

定义7 二元归结^[17]：给定两个子句C_{\mathrm{1}}和C_{\mathrm{2}}，若C_{\mathrm{1}}中存在文字L_{\mathrm{1}}，C_{\mathrm{2}}中存在文字L_{\mathrm{2}}，且存在替换\sigma，使得L_{\mathrm{1}}\sigma =~L_{\mathrm{2}}\sigma，即存在合一互补对文字L_{\mathrm{1}}和L_{\mathrm{2}}，则替换后C_{\mathrm{1}}和C_{\mathrm{2}}中除L_{\mathrm{1}}和L_{\mathrm{2}}外的剩余文字的析取称为C_{\mathrm{1}}和C_{\mathrm{2}}的归结式，这个过程称为二元归结。

定理1 归结原理的完备性定理^[18]：如果子句集S是不可满足的，则存在从S到空子句\mathrm{\varnothing }的一个二元归结演绎。

1.2　多元动态演绎理论

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

1） C_{\mathrm{1}},C_{\mathrm{2}},\dots ,C_m各子句之间不存在相同的变元（若存在不同的子句有相同的变元，需要做变元更名）。

2） 对任意的子句C_i，i=\mathrm{1,2},\dots ,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+}，其中有：

① C_i^{{\sigma }_i}=C_i^{{\sigma }_i+}\vee C_i^{{\sigma }_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-}，存在互补对文字，\stackrel{m}{\underset{i=\mathrm{1}}{\bigwedge }}{C}_{\mathrm{i}}^{{\mathrm{\sigma }}_{\mathrm{i}}-}称为标准矛盾体（Separated Standard Contradiction, S-SC）。

③ \stackrel{m}{\underset{i=\mathrm{1}}{\bigvee }}{C}_{\mathrm{i}}^{{\mathrm{\sigma }}_{\mathrm{i}}+}={\mathbb{C}}_m^{s\sigma }(C_{\mathrm{1}},\cdots ,{\mathrm{C}}_m)，其中\sigma ={\displaystyle \underset{i=\mathrm{1}}{\overset{m}{\cup }}}{\sigma }_i。

则称{\mathbb{C}}_m^{s\sigma }(C_{\mathrm{1}},\cdots ,C_m)为矛盾体分离式（Standard Contradiction Separation Clause, S-CSC），该演绎方法称为矛盾体分离规则，简称S-CS规则。

1.3　不同子句与文字的选择对演绎的影响

在多元演绎过程中，选取候选子句中子句的顺序以及构建标准矛盾体的文字的不同，对后续多元演绎步骤、演绎结果以及矛盾体分离式的复杂程度起重要影响。

例1 假定一阶逻辑子句集S=\left\{C_{\mathrm{1}},C_{\mathrm{2}},C_{\mathrm{3}},C_{\mathrm{4}},\right.C_{\mathrm{5}},C_{\mathrm{6}},C_{\mathrm{7}},\left.C_{\mathrm{8}}\right\}，其中C_{\mathrm{1}}=P_{\mathrm{1}}(x_{\mathrm{1}},f_{\mathrm{1}}(b))，C_{\mathrm{2}}=P_{\mathrm{2}}(x_{\mathrm{2}},f_{\mathrm{1}}(x_{\mathrm{3}}))，C_{\mathrm{3}}=P_{\mathrm{2}}(x_{\mathrm{4}},x_{\mathrm{5}})\vee P_{\mathrm{3}}(x_{\mathrm{6}},f_{\mathrm{2}}(x_{\mathrm{2}},b))\vee ~P_{\mathrm{4}}(x_{\mathrm{4}},x_{\mathrm{8}})，C_{\mathrm{4}}=~P_{\mathrm{1}}(x_{\mathrm{9}},x_{\mathrm{10}})\vee ~P_{\mathrm{2}}(x_{\mathrm{11}},x_{\mathrm{12}})，C_{\mathrm{5}}=~P_{\mathrm{2}}(x_{\mathrm{13}},x_{\mathrm{14}})\vee ~P_{\mathrm{6}}(x_{\mathrm{15}},x_{\mathrm{16}})\vee ~P_{\mathrm{7}}(x_{\mathrm{17}},x_{\mathrm{18}},f_{\mathrm{1}}(b))，C_{\mathrm{6}}=~P_{\mathrm{1}}(x_{\mathrm{19}},x_{\mathrm{20}})\vee P_{\mathrm{4}}(f_{\mathrm{2}}(x_{\mathrm{19}},a),f_{\mathrm{2}}(x_{\mathrm{21}},b))\vee ~P_{\mathrm{5}}(x_{\mathrm{20}},x_{\mathrm{22}})\vee P_{\mathrm{7}}(x_{\mathrm{23}},x_{\mathrm{24}},f_{\mathrm{2}}(a,b)),C_{\mathrm{7}}=P_{\mathrm{6}}(x_{\mathrm{25}},x_{\mathrm{26}})\vee P_{\mathrm{8}}(f_{\mathrm{1}}(c),x_{\mathrm{27}})，C_{\mathrm{8}}=P_{\mathrm{6}}(a,b)\vee P_{\mathrm{8}}(a,b)。

若选取S中两个单元子句C_{\mathrm{1}}和C_{\mathrm{2}}用于构建标准矛盾体，之后选取子句C_{\mathrm{4}}进行多元演绎，则可以得到矛盾体分离式C_{\mathrm{9}}为空子句，因此得到S不可满足结论，其演绎过程如表1所示。

若选取S中两个单元子句C_{\mathrm{1}}和C_{\mathrm{2}}用于构建标准矛盾体，之后选取子句C_{\mathrm{6}}进行多元演绎，则可以得到矛盾体分离式C_{\mathrm{10}}=P_{\mathrm{4}}(f_{\mathrm{2}}(x_{\mathrm{1}},a),f_{\mathrm{2}}(x_{\mathrm{21}},b))\vee~P_{\mathrm{5}}(x_{\mathrm{20}},x_{\mathrm{22}})\vee P_{\mathrm{7}}(x_{\mathrm{23}},x_{\mathrm{24}},f_{\mathrm{2}}(a,b))，其演绎过程如表2所示。由于在本次多元演绎中，C_{\mathrm{6}}文字个数较多，且仅有一个文字与当前标准矛盾体文字合一互补，因此将过多的文字放入矛盾体分离式中，使矛盾体分离式变得更加的复杂，降低了演绎的效率。

若选取S中两个单元子句C_{\mathrm{1}}和C_{\mathrm{2}}用于构建标准矛盾体，之后选取子句C_{\mathrm{5}}进行多元演绎，则得到矛盾体分离式C_{\mathrm{11}}=~P_{\mathrm{6}}(x_{\mathrm{15}},x_{\mathrm{16}})\vee ~P_{\mathrm{7}}(x_{\mathrm{17}},x_{\mathrm{18}},f_{\mathrm{1}}(b))。若进行下一步的多元演绎，需在文字~P_{\mathrm{6}}(x_{\mathrm{15}},x_{\mathrm{16}})和~P_{\mathrm{7}}(x_{\mathrm{17}},x_{\mathrm{18}},f_{\mathrm{1}}(b))中选择一个文字继续构建标准矛盾体，则存在如下两种情况：

1） 若使用文字~P_{\mathrm{6}}(x_{\mathrm{15}},x_{\mathrm{16}})构建标准矛盾体，~P_{\mathrm{6}}(x_{\mathrm{15}},x_{\mathrm{16}})文字与C_{\mathrm{7}}，C_{\mathrm{8}}两个子句中的文字存在合一互补对，即与更多的文字合一互补能使矛盾体分离式具有较少的文字数。

2） 若使用文字~P_{\mathrm{7}}(x_{\mathrm{17}},x_{\mathrm{18}},f_{\mathrm{1}}(b))构建标准矛盾体，~P_{\mathrm{7}}(x_{\mathrm{17}},x_{\mathrm{18}},f_{\mathrm{1}}(b))文字与候选子句集\left\{C_{\mathrm{3}},C_{\mathrm{4}},C_{\mathrm{6}},C_{\mathrm{7}},C_{\mathrm{8}}\right\}中子句的文字都不存在合一互补对，即选择文字~P_{\mathrm{7}}(x_{\mathrm{17}},x_{\mathrm{18}},f_{\mathrm{1}}(b))构建的标准矛盾体的演绎能力没有得到提高，且使得矛盾体分离式变得更加复杂，影响后续多元演绎的能力和效率。

综上所述，在多元动态演绎过程中，参与演绎的子句剩余文字个数、用于构建标准矛盾体的文字以及对参与演绎的子句进行消元的文字都对多元演绎的能力和效率起着重要的作用。因此，本文通过子句参与演绎后对当前标准矛盾体的影响程度、剩余文字的个数以及文字演绎能力三个方面来刻画子句的综合度量值，通过此度量值选择较优的子句参与演绎，从而保持多元演绎过程中矛盾体分离式中的文字较少并提升标准矛盾体的演绎能力。

2　 基于项合一能力的子句影响度评估方法

2.1　项合一能力评估方法

在一阶逻辑中，文字中的项分为三类：常元项、变元项以及函数项。这三类项合一有如下形式：

1） 变元项可以与所有项合一。

2） 常元项可以与变元项、相同常元项合一。

3） 函数项可以与变元项、部分不相同函数项以及相同函数项合一，比如函数项f(a)，可以与变元项合一也可以与函数项f(x)合一。

基于上述，通过分析得到变元项的合一能力>函数项的合一能力>常元项的合一能力（>表示大于）。为了方便描述，使用CT表示常元项类、VT表示变元项类、FT表示函数项类。函数项f\left(\mathrm{V}\mathrm{T},\mathrm{C}\mathrm{T},\mathrm{F}\mathrm{T}\right)表示第一个元中项为任意变元项，第二个元中项为任意常元项，第三个元中项为任意函数项。

变元合一能力设置为1，因为变元项可以和任何一个项合一，即变元项自身含有合一能力。常元项合一能力设置为1/3，因为常元项只能与变元项合一，占项三种类型的一种。下面对函数项的合一能力进行重点分析。

定义9 函数项-子项：在一阶逻辑公式中，函数项元中的项称为该函数项的子项。比如函数项f(a_{\mathrm{1}},x_{\mathrm{1}},f(b,x_{\mathrm{2}}))，项a_{\mathrm{1}}、x_{\mathrm{1}}以及f(b,x_{\mathrm{2}})称为函数项f(a,x_{\mathrm{1}},f(b,x_{\mathrm{2}}))的子项，项b以及项x_{\mathrm{2}}称为函数项f(b,x_{\mathrm{2}})的子项。

函数项能与任意变元项合一，因此后续不再过多分析对变元项合一的情况。由于在多元演绎中相同函数项名的函数项元数相同，并且函数项子项变化不会改变元数，因此下面只分析函数项对同名函数项的合一能力，通过分析得出函数项的合一能力设置为该函数项对子句集中其他同名函数项的合一能力乘以1/3，再加上1/3。

函数项对同名函数项的合一能力分析如下：

1） 函数项中不含共享变元

在项f(a_{\mathrm{1}},x_{\mathrm{1}})与项f(x_{\mathrm{2}},a_{\mathrm{2}})中，因为前者可与项f\left(\mathrm{V}\mathrm{T},\mathrm{V}\mathrm{T}\right)、项f\left(\mathrm{V}\mathrm{T},\mathrm{C}\mathrm{T}\right)、项f\left(\mathrm{V}\mathrm{T},\mathrm{F}\mathrm{T}\right)合一，后者可与项f\left(\mathrm{V}\mathrm{T},\mathrm{V}\mathrm{T}\right)、项f\left(\mathrm{C}\mathrm{T},\mathrm{V}\mathrm{T}\right)、项f\left(\mathrm{F}\mathrm{T},\mathrm{V}\mathrm{T}\right)合一，他们都能与二元情况下九种类型中的三种类型合一，因此项f(a_{\mathrm{1}},x_{\mathrm{1}})与项f(x_{\mathrm{2}},a_{\mathrm{2}})合一能力相同，他们对同名函数项的合一能力都为1/3。在项f(a_{\mathrm{1}},x_{\mathrm{1}})与项f(x_{\mathrm{1}},x_{\mathrm{2}})中，前者能与二元情况下的三种类型合一，而后者能与二元情况下九种类型都合一，即能与二元情形下的函数项都合一，则项f(a_{\mathrm{1}},x_{\mathrm{1}})对同名函数项的合一能力是项f(x_{\mathrm{1}},x_{\mathrm{2}})合一能力的1/3。在一个不含共享变元的n元函数项f中，F为子句集中能与f合一的n元同名函数项集合。f不含共享变元，即f各个元中的项是相互独立的，则F占所有n元同名函数项比例为f每个元中项合一能力的乘积。因此不含共享变元函数项，其对同名函数项合一能力为每个元中项合一能力的乘积。

2） 函数项中含有共享变元

① 共享变元在同层

在项f(x_{\mathrm{1}},x_{\mathrm{1}})以及项f(x_{\mathrm{1}},x_{\mathrm{2}})中，项f(x_{\mathrm{1}},x_{\mathrm{2}})对二元同名函数项的合一能力为1，而在项f(x_{\mathrm{1}},x_{\mathrm{1}})中，x_{\mathrm{1}}为共享变元，则与项f(x_{\mathrm{1}},x_{\mathrm{1}})能合一的同名函数项中两个元中的项必定是能合一的。与项f(x_{\mathrm{1}},x_{\mathrm{1}})能合一的同名函数项中两个元中的项有以下关系：

a. 若任一元中的项都不为变元项，则两个元中的项是相同的常元或者是两个能合一的函数项，但这两种情况分别在f\left(\mathrm{C}\mathrm{T},\mathrm{C}\mathrm{T}\right)以及f\left(\mathrm{F}\mathrm{T},\mathrm{F}\mathrm{T}\right)的二元函数项类型下的比例较低，因此本文不考虑。

b. 若有一元中的项为变元项，则另一元中的项不管是哪种类型的项都可合一，因此项f(x_{\mathrm{1}},x_{\mathrm{1}})能与5种类型的二元函数项合一，则项f(x_{\mathrm{1}},x_{\mathrm{1}})对二元函数项的合一能力为5/9。

进一步地，对一个n元函数项f_{\mathrm{2}}，并且这n元中的项都为变元x_{\mathrm{1}}，能与f_{\mathrm{2}}合一的n元同名函数项中必须至少n-\mathrm{1}元中的项都为变元项，则f_{\mathrm{2}}能与\mathrm{2}\times n+\mathrm{1}种类型的n元同名函数项合一，因此f_{\mathrm{2}}对n元同名函数项的合一能力为(\mathrm{2}\times n+\mathrm{1})/{\mathrm{3}}^n。

② 共享变元非同层

在项f(x_{\mathrm{1}},f(x_{\mathrm{1}}))中，第一个x_{\mathrm{1}}为第一层，第二个x_{\mathrm{1}}为第二层，若能与二元函数项f合一，则对f(x_{\mathrm{1}},f(x_{\mathrm{1}}))低层共享变元x_{\mathrm{1}}，项f相同元中项所对应项为变元项，此时第二个项为单独用项f(x_{\mathrm{1}})能合一的项，不用考虑共享的影响。进一步地，在一个n元含共享变元的函数项f_{\mathrm{1}}中，F_{\mathrm{1}}为能与f_{\mathrm{1}}合一的n元同名函数项集合，F_{\mathrm{1}}中对应f_{\mathrm{1}}中低层共享变元位置上的项类型应全为变元项，之后f_{\mathrm{1}}中高层的共享变元就不需考虑之前低层共享变元的影响，最终可得到结论：在一个n元函数项f_{\mathrm{3}}中，F_{\mathrm{3}}为能与项f_{\mathrm{3}}合一的n元同名函数项集合，则项f_{\mathrm{3}}中共享变元项x_{\mathrm{1}}有以下情形：

a. x_{\mathrm{1}}是项f_{\mathrm{3}}的子项，若x_{\mathrm{1}}为最高层，则按照同层共享变元处理；若不为最高层，则F_{\mathrm{3}}对应f_{\mathrm{3}}中子项为x_{\mathrm{1}}的位置上的项类型应全为变元项。

b. x_{\mathrm{1}}不是f_{\mathrm{3}}的子项，则x_{\mathrm{1}}被f_{\mathrm{3}}子项中函数项包含，若此函数项为f_{\mathrm{4}}，则只需要考虑f_{\mathrm{4}}存在共享变元x_{\mathrm{1}}时的合一能力，此时仍应按照情形a、情形b对f_{\mathrm{4}}进行分析。

综上，将函数项子项相同变元看作一个整体，则这个整体合一能力为：

\mathrm{V}\mathrm{U}\mathrm{A}(x)=\left\{\begin{array}{ll}\frac{\mathrm{1}}{{\mathrm{3}}^n},& x\mathrm{不是}\mathrm{此变}\mathrm{元的}\mathrm{最高}\mathrm{层}\\ \frac{\mathrm{2}\times n+\mathrm{1}}{{\mathrm{3}}^n},& x\mathrm{是此}\mathrm{变元}\mathrm{的最}\mathrm{高层}\end{array}\right.（1）

其中，VUA(Variable Unification Ability)表示变元整体的合一能力，x表示变元项，n表示整体中变元项x的个数，（1）式同样适用于非共享变元项合一能力。

这样各个不同的整体与其他子项之间独立，因此n元函数项对同名函数项的合一能力为各个整体合一能力以及单独项的乘积。

综上，项的合一能力（Term Unification Ability, TUA）公式如下：

\mathrm{T}\mathrm{U}\mathrm{A}(t)=\left\{\begin{array}{ll}\mathrm{1},& t\in \mathrm{C}\mathrm{T}\\ \frac{\mathrm{1}}{\mathrm{3}},& t\in \mathrm{V}\mathrm{T}\\ \frac{\mathrm{1}}{\mathrm{3}}+\frac{\prod _{t_i\notin \mathrm{V}\mathrm{T}}\mathrm{T}\mathrm{U}\mathrm{A}(t_i)\times \prod _{t_j\in \mathrm{V}\mathrm{T}}\mathrm{V}\mathrm{U}\mathrm{A}(t_j)}{\mathrm{3}},& t\in \mathrm{F}\mathrm{T}\end{array}\right.（2）

其中，\prod _{t_i\notin VT}TUA(t_i)表示函数项t的子项中不为变元项的t_i合一能力的乘积，\prod _{t_j\in VT}VUA(t_j)表示函数项t的子项中为变元项的t_j合一能力的乘积。

例2 设有函数项为f_{\mathrm{2}}(a,x_{\mathrm{3}},x_{\mathrm{3}},f_{\mathrm{3}}(x_{\mathrm{3}},x_{\mathrm{4}}))，计算项的合一能力。

f_{\mathrm{2}}(a,x_{\mathrm{3}},x_{\mathrm{3}},f_{\mathrm{3}}(x_{\mathrm{3}},x_{\mathrm{4}}))的树状图如图1所示（图中箭头所指为函数项的子项）。将所求函数项f_{\mathrm{2}}(a,x_{\mathrm{3}},x_{\mathrm{3}},f_{\mathrm{3}}(x_{\mathrm{3}},x_{\mathrm{4}}))作为树状图的第0层，其子项为该函数项的下一层；子项a、x_{\mathrm{3}}、x_{\mathrm{3}}以及f_{\mathrm{3}}(x_{\mathrm{3}},x_{\mathrm{4}})在第1层中，其中变元项x_{\mathrm{3}}、x_{\mathrm{3}}相同，因此将第1层这两个项x_{\mathrm{3}}看作一个整体。由于在第2层中也含有项x_{\mathrm{3}}，即第1层项x_{\mathrm{3}}并非为最高层，因此第1层x_{\mathrm{3}}整体的合一能力\mathrm{V}\mathrm{U}\mathrm{A}(x_{\mathrm{3}})=\mathrm{1}/\mathrm{9}；则之后第一层中x_{\mathrm{3}}与函数项f_{\mathrm{3}}(x_{\mathrm{3}},x_{\mathrm{4}})无关联，在函数项f_{\mathrm{3}}(x_{\mathrm{3}},x_{\mathrm{4}})中，由于其子项x_{\mathrm{3}}、x_{\mathrm{4}}不相同，因此\mathrm{T}\mathrm{U}\mathrm{A}(f_{\mathrm{3}}(x_{\mathrm{3}},x_{\mathrm{4}}))=\mathrm{1}/\mathrm{3}+\mathrm{1}/\mathrm{3}\times \mathrm{1}\times \mathrm{1}=\mathrm{2}/\mathrm{3}。综上，\mathrm{T}\mathrm{U}\mathrm{A}(f_{\mathrm{2}}(a,x_{\mathrm{3}},x_{\mathrm{3}},f_{\mathrm{3}}(x_{\mathrm{3}},x_{\mathrm{4}})))=\mathrm{1}/\mathrm{3}+\mathrm{1}/\mathrm{3}\times \mathrm{1}/\mathrm{9}\times \mathrm{2}/\mathrm{3}\times \mathrm{1}/\mathrm{3}=\mathrm{83}/\mathrm{243}。

2.2　基于项合一能力的项影响度评估方法

定义10 项影响度（Term Influence Degree，TID）：设有两个项分别为t_{\mathrm{1}}和t_{\mathrm{2}}，且t_{\mathrm{1}}与t_{\mathrm{2}}可合一，当发生合一后项t_{\mathrm{1}}被替换为t_{\mathrm{3}}，称项t_{\mathrm{1}}合一能力减去项t_{\mathrm{3}}合一能力的值为合一后对项t_{\mathrm{1}}的影响度。

在一阶逻辑中，两个文字合一互补后，替换关系中项双方至少有一方为变元项，因此项影响度存在以下结论：

1） 在替换关系中，若项t的合一能力小于等于与其合一项t_i的合一能力，则项t的合一能力并不会改变，即项t的影响度为0。例如项t为常元项,项t_i则为变元项；项t为函数项,项t_i则为变元项；项t为变元项,项t_i为变元项，都不会影响项t的合一能力。

2） 在替换关系中，若项t的合一能力大于其合一项t_i的合一能力，在替换关系中，只有当项t为变元项时才会出现这种情形，而项t_i只能为常元项以及函数项，则有以下两种情形：

a. 项t_i为常元项

由于项t_i为常元项，则变元项t将被替换为常元项t_i，即之后项t只能与变元项以及与其相同的常元项合一，使此项的合一能力下降。

b. 项t_i为函数项

由于项t_i为函数项，则变元项t将被替换为函数项t_i，即之后项t只能与变元项以及与函数项合一，使项t的合一能力下降。

t的项影响度公式如（3）式，用来度量项t与项t_i合一后对项t合一能力的影响。

\mathrm{T}\mathrm{I}\mathrm{D}(t,t_i)=\left\{\begin{array}{ll}\mathrm{0},& \mathrm{T}\mathrm{U}\mathrm{A}(t)\le \mathrm{T}\mathrm{U}\mathrm{A}(t_i)\\ \mathrm{1}-\mathrm{T}\mathrm{U}\mathrm{A}(t_i),& \mathrm{T}\mathrm{U}\mathrm{A}(t)>\mathrm{T}\mathrm{U}\mathrm{A}(t_i)\end{array}\right.（3）

2.3　子句影响度的评估方法

定义11 决策文字集^[13]：在标准矛盾体构建过程中，已参与演绎子句存在一个文字对候选子句C_i^{{\sigma }_i}起演绎作用，即将C_i^{{\sigma }_i}划分为C_i^{{\sigma }_i-}和C_i^{{\sigma }_i+}两部分，则将该文字称为决策文字，称标准矛盾体各个子句中的决策文字所组成的集合为决策文字集。

定义12 演绎文字：假设存在一个子句C，存在一个替换关系\sigma（\sigma可以为空）使得C中的文字能与决策文字集D中文字合一互补，称C中通过\sigma替换与D中文字合一互补后的文字为演绎文字。

定义13 子句影响度（Clause Influence Degree，CID）：用来刻画子句演绎后，决策文字集中项替换对标准矛盾体的影响程度。

在多元演绎过程中，选择一个候选子句与当前标准矛盾体进行演绎，记此时决策文字集为D_b。若该候选子句存在演绎文字，即每个演绎文字都与决策文字存在一个替换关系，这些替换关系最终导致决策文字集为D_b中文字的项发生替换，此时决策文字集为D_e。因此，子句影响度即为决策文字集D_b到决策文字集为D_e中所有替换项影响度之和。

子句C演绎后对标准矛盾体演绎能力的影响度公式如下：

\mathrm{C}\mathrm{I}\mathrm{D}(C)=\sum _{t\in \sigma }TID(t,t_i)（4）

其中，\sigma表示替换关系，t为决策文字集中发生替换的项，t_i为与t合一的项。

3　 子句综合权重

除了上述标准矛盾体中项替换对多元演绎路径产生影响外，剩余文字个数以及继续加入标准矛盾体文字消元能力同样能对多元演绎路径产生影响。

3.1　剩余文字数对多元演绎的影响

一般地，在归结演绎过程中，含文字数少的子句参与演绎往往具有较高的演绎效率，这是因为演绎生成的分离式往往也含有较少的文字数。因此在矛盾体分离演绎过程中，每次演绎结束，都希望矛盾体分离式文字数缓慢增加，即每次演绎子句剩余文字数都尽可能少，从而提高多元演绎的效率。本文使用\mathrm{R}\mathrm{L}\mathrm{N}(Remaining Literals Numbers)表示候选子句与标准矛盾体演绎后剩余文字的个数。

3.2　基于合一互补文字个数的文字演绎能力评估方法

除剩余文字数外，标准矛盾体演绎能力同样可以影响多元演绎效率。在多元演绎中，为了提高标准矛盾体的演绎能力，期望决策文字都能在后续的演绎中与更多文字合一互补，从而减少矛盾体分离式中文字个数，提高演绎效率。文字演绎能力体现在候选子句集中能与此文字合一互补文字个数，互补文字个数越大，则表明候选子句参与演绎时加入到标准矛盾体中的文字数量越多，减少了加入矛盾体分离式的文字个数，从而提高多元演绎的效率，因此将此个数作为文字演绎能力的度量值。

文字演绎能力的度量值如（5）式所示：

\mathrm{L}\mathrm{D}\mathrm{A}(P)=a（5）

其中，a为文字P与候选子句集中文字合一互补对个数。

子句演绎之后可能存在多个剩余文字，需要在这些剩余文字选取最大文字演绎能力的文字加入标准矛盾体，从而较好提升标准矛盾体文字消元能力，因此最大剩余文字演绎能力（Maximum Remaining Literals Deductive Ability，MRLDA）可表示为：

\mathrm{M}\mathrm{R}\mathrm{L}\mathrm{D}\mathrm{A}(C)=\mathrm{m}\mathrm{a}\mathrm{x}(\mathrm{L}\mathrm{D}\mathrm{A}(P_i))（6）

其中，P_i为子句C演绎后的剩余文字。

3.3　子句综合权重的度量

在多元演绎过程中，选择合适子句参与演绎至关重要，子句影响度过大将导致标准矛盾体消元能力急剧下降，增加矛盾体分离式文字个数；剩余文字过多将导致矛盾体分离式变得复杂；决策文字的演绎能力过低在后续演绎中将只能与少量候选子句集中文字合一互补，增加矛盾体分离式文字个数。因此需要综合考虑。

定义14 子句综合权重（Clause Comprehensive Weight，CCW）：在多元演绎过程中，用来刻画在子句影响度、剩余文字的个数以及决策文字的演绎能力多因素下子句的度量值。

子句C的子句综合权重公式如下：

\mathrm{C}\mathrm{C}\mathrm{W}(C)=\left\{\begin{array}{ll}\mathrm{10}\mathrm{000},& \mathrm{R}\mathrm{L}\mathrm{N}(C)=\mathrm{0}\\ \mathrm{5}\mathrm{000},& \mathrm{R}\mathrm{L}\mathrm{N}(C)=\mathrm{1}\\ \frac{\mathrm{M}\mathrm{R}\mathrm{L}\mathrm{D}\mathrm{A}(C)}{\mathrm{R}\mathrm{L}\mathrm{N}(C)\times {\mathrm{2}}^{\mathrm{C}\mathrm{I}\mathrm{D}(C)}},& \mathrm{R}\mathrm{L}\mathrm{N}(C)>\mathrm{1}\end{array}\right.（7）

子句集规模绝大多数情况下小于5 000，当\mathrm{R}\mathrm{L}\mathrm{N}(C)>\mathrm{1}时，又因为{\mathrm{2}}^{\mathrm{C}\mathrm{I}\mathrm{D}(C)}\ge \mathrm{1}，则。因此，根据（7）式，可优先选择剩余文字为0的候选子句，其次选择剩余文字为1的候选子句，最后选择剩余文字大于1的候选子句。

例3 设假定一阶逻辑子句集S=\left\{C_{\mathrm{1}},C_{\mathrm{2}},C_{\mathrm{3}},\right.\left.C_{\mathrm{4}}\right\}，其中C_{\mathrm{1}}=P_{\mathrm{1}}(x_{\mathrm{1}},f_{\mathrm{1}}(b))，C_{\mathrm{2}}=~P_{\mathrm{2}}(x_{\mathrm{2}},f_{\mathrm{1}}(x_{\mathrm{3}})),C_{\mathrm{3}}=P_{\mathrm{2}}(x_{\mathrm{4}},f_{\mathrm{1}}(b))\vee P_{\mathrm{3}}(x_{\mathrm{6}},f_{\mathrm{2}}(x_{\mathrm{6}},b))\vee P_{\mathrm{4}}(x_{\mathrm{5}},x_{\mathrm{7}}),C_{\mathrm{4}}=~P_{\mathrm{1}}(x_{\mathrm{8}},x_{\mathrm{9}})\vee P_{\mathrm{2}}(x_{\mathrm{10}},x_{\mathrm{8}})\vee ~P_{\mathrm{3}}(x_{\mathrm{11}},x_{\mathrm{12}})\vee P_{\mathrm{4}}(a,x_{\mathrm{13}})。

选取S中两个单元子句C_{\mathrm{1}}和C_{\mathrm{2}}构建标准矛盾体，并将这两个单元子句中的文字放入决策文字集中，此时原始决策集D=\{P_{\mathrm{1}}(x_{\mathrm{1}},f_{\mathrm{1}}(b)),~P_{\mathrm{2}}(x_{\mathrm{2}},f_{\mathrm{1}}(x_{\mathrm{3}}))\}，候选子句集为\left\{C_{\mathrm{3}},C_{\mathrm{4}}\right\}。

计算C_{\mathrm{4}}的子句综合权重值：

第一步：C_{\mathrm{4}}中文字~P_{\mathrm{1}}(x_{\mathrm{8}},x_{\mathrm{9}})与决策文字集中文字P_{\mathrm{1}}(x_{\mathrm{1}},f_{\mathrm{1}}(b))合一互补，存在替换关系{\sigma }_{\mathrm{1}}=\{x_{\mathrm{8}}/x_{\mathrm{1}},f_{\mathrm{1}}(b)/x_{\mathrm{9}}\}，决策文字集中文字P_{\mathrm{1}}(x_{\mathrm{1}},f_{\mathrm{1}}(b))被替换为P_{\mathrm{1}}(x_{\mathrm{8}},f_{\mathrm{1}}(b))，此时决策文字集D_{\mathrm{1}}=\{P_{\mathrm{1}}(x_{\mathrm{8}},f_{\mathrm{1}}(b)),~P_{\mathrm{2}}(x_{\mathrm{2}},f_{\mathrm{1}}(x_{\mathrm{3}}))\}。

第二步：C_{\mathrm{4}}中文字P_{\mathrm{2}}(x_{\mathrm{10}},x_{\mathrm{8}})与决策文字集中文字~P_{\mathrm{2}}(x_{\mathrm{2}},f_{\mathrm{1}}(x_{\mathrm{3}}))合一互补，存在替换关系{\sigma }_{\mathrm{2}}=\{x_{\mathrm{10}}/x_{\mathrm{2}},f_{\mathrm{1}}(x_{\mathrm{3}})/x_{\mathrm{8}}\}，决策文字集中文字~P_{\mathrm{2}}(x_{\mathrm{2}},f_{\mathrm{1}}(x_{\mathrm{3}}))被替换为~P_{\mathrm{2}}(x_{\mathrm{10}},f_{\mathrm{1}}(x_{\mathrm{3}}))，由于第一步后，决策文字P_{\mathrm{1}}(x_{\mathrm{8}},f_{\mathrm{1}}(b))也含有x_{\mathrm{8}}，因此被替换为P_{\mathrm{1}}(f_{\mathrm{1}}(x_{\mathrm{3}}),f_{\mathrm{1}}(b))，此时决策文字集D_{\mathrm{2}}=\{P_{\mathrm{1}}(f_{\mathrm{1}}(x_{\mathrm{3}}),f_{\mathrm{1}}(b)),~P_{\mathrm{2}}(x_{\mathrm{10}},f_{\mathrm{1}}(x_{\mathrm{3}}))\}。

第三步：C_{\mathrm{4}}剩余两个文字~P_{\mathrm{3}}(x_{\mathrm{11}},x_{\mathrm{12}})、P_{\mathrm{4}}(a,x_{\mathrm{13}})都不能和决策文字集D_{\mathrm{2}}中的文字合一互补，因此剩余文字个数为2，即\mathrm{R}\mathrm{L}\mathrm{N}(C_{\mathrm{4}})=\mathrm{2}，比较初始决策文字集D与最终决策文字集D_{\mathrm{2}},得到决策文字集的替换\sigma =\{f_{\mathrm{1}}(x_{\mathrm{3}})/x_{\mathrm{1}},x_{\mathrm{10}}/x_{\mathrm{2}}\}。

第四步：根据\sigma计算子句影响度，\mathrm{C}\mathrm{I}\mathrm{D}(C_{\mathrm{4}})=\mathrm{T}\mathrm{I}\mathrm{D}(x_{\mathrm{1}},f_{\mathrm{1}}(x_{\mathrm{3}}))+\mathrm{T}\mathrm{I}\mathrm{D}(x_{\mathrm{2}},x_{\mathrm{10}})，由于项x_{\mathrm{1}}合一能力大于项f_{\mathrm{1}}(x_{\mathrm{3}})，因此\mathrm{T}\mathrm{I}\mathrm{D}(x_{\mathrm{1}},f_{\mathrm{1}}(x_{\mathrm{3}}))=\mathrm{1}-\mathrm{2}/\mathrm{3}=\mathrm{1}/\mathrm{3}；由于x_{\mathrm{2}}与x_{\mathrm{10}}合一能力相同，因此\mathrm{T}\mathrm{I}\mathrm{D}(x_{\mathrm{2}},x_{\mathrm{10}})=\mathrm{0}；因此\mathrm{C}\mathrm{I}\mathrm{D}(C_{\mathrm{4}})=\mathrm{1}/\mathrm{3}+\mathrm{0}=\mathrm{1}/\mathrm{3}。

第五步：计算最大剩余文字演绎能力，已知C_{\mathrm{4}}剩余文字为~P_{\mathrm{3}}(x_{\mathrm{11}},x_{\mathrm{12}})、P_{\mathrm{4}}(a,x_{\mathrm{13}})。剩余文字~P_{\mathrm{3}}(x_{\mathrm{11}},x_{\mathrm{12}})能与候选子句集\left\{C_{\mathrm{3}}\right\}中一个文字P_{\mathrm{3}}(x_{\mathrm{6}},f_{\mathrm{2}}(x_{\mathrm{6}},b))合一互补，因此\mathrm{L}\mathrm{D}\mathrm{A}(~P_{\mathrm{3}}(x_{\mathrm{11}},x_{\mathrm{12}}))=\mathrm{1}；剩余文字P_{\mathrm{4}}(a,x_{\mathrm{13}})在候选子句集\left\{C_{\mathrm{3}}\right\}中不存在文字与其合一互补，因此\mathrm{L}\mathrm{D}\mathrm{A}(P_{\mathrm{4}}(a,x_{\mathrm{13}}))=\mathrm{0}，所以\mathrm{M}\mathrm{R}\mathrm{L}\mathrm{D}\mathrm{A}(C_{\mathrm{4}})=\mathrm{1}；

第六步：计算子句综合权重值，因为\mathrm{R}\mathrm{L}\mathrm{N}(C_{\mathrm{4}})=\mathrm{2}，因此\mathrm{C}\mathrm{C}\mathrm{W}(C_{\mathrm{4}})=\frac{\mathrm{1}}{\mathrm{2}\times {\mathrm{2}}^{\mathrm{1}/\mathrm{3}}}={\mathrm{2}}^{-\mathrm{4}/\mathrm{3}}。

例4 设假定一阶逻辑子句集S=\left\{C_{\mathrm{1}},C_{\mathrm{2}},C_{\mathrm{3}},C_{\mathrm{4}},C_{\mathrm{5}},C_{\mathrm{6}}\right\}，其中C_{\mathrm{1}}=P_{\mathrm{1}}(x_{\mathrm{1}})，C_{\mathrm{2}}=P_{\mathrm{2}}(x_{\mathrm{2}})，C_{\mathrm{3}}=~P_{\mathrm{1}}(f_{\mathrm{1}}(x_{\mathrm{3}}))\vee P_{\mathrm{4}}(x_{\mathrm{4}}),C_{\mathrm{4}}=~P_{\mathrm{2}}(x_{\mathrm{5}})\vee P_{\mathrm{3}}(a)，C_{\mathrm{5}}=~P_{\mathrm{1}}(f_{\mathrm{1}}(a))\vee ~P_{\mathrm{4}}(f_{\mathrm{2}}(x_{\mathrm{6}},a))\vee P_{\mathrm{5}}(x_{\mathrm{6}})，C_{\mathrm{6}}=~P_{\mathrm{2}}(x_{\mathrm{7}})\vee ~P_{\mathrm{3}}(x_{\mathrm{8}})\vee ~P_{\mathrm{4}}(f_{\mathrm{2}}(x_{\mathrm{8}},x_{\mathrm{9}}))。

选取S中两个单元子句C_{\mathrm{1}}和C_{\mathrm{2}}构建标准矛盾体，并将这两个单元子句中的文字放入决策文字集中此时原始决策文字集D=\{P_{\mathrm{1}}(x_{\mathrm{1}}),P_{\mathrm{2}}(x_{\mathrm{2}})\},候选子句集为S_{\mathrm{1}}=\left\{C_{\mathrm{3}},C_{\mathrm{4}},C_{\mathrm{5}},C_{\mathrm{6}}\right\}。

根据（7）式计算可以得到，\mathrm{C}\mathrm{C}\mathrm{W}(C_{\mathrm{3}})=\mathrm{5}\mathrm{000}，\mathrm{C}\mathrm{C}\mathrm{W}(C_{\mathrm{4}})=\mathrm{5}\mathrm{000}，\mathrm{C}\mathrm{C}\mathrm{W}(C_{\mathrm{5}})={\mathrm{2}}^{-\mathrm{14}/\mathrm{9}}，\mathrm{C}\mathrm{C}\mathrm{W}(C_{\mathrm{6}})={\mathrm{2}}^{-\mathrm{1}}。本文优先选择子句综合权重大的子句参与演绎，但\mathrm{C}\mathrm{C}\mathrm{W}(C_{\mathrm{3}})=\mathrm{C}\mathrm{C}\mathrm{W}(C_{\mathrm{4}})，此时再比较子句影响度，优先选择较子句影响度小的子句。因为\mathrm{C}\mathrm{I}\mathrm{D}(C_{\mathrm{3}})=\mathrm{1}/\mathrm{3}、\mathrm{C}\mathrm{I}\mathrm{D}(C_{\mathrm{4}})=\mathrm{0}，所以演绎顺序为C_{\mathrm{4}}、C_{\mathrm{3}}、C_{\mathrm{6}}、C_{\mathrm{5}}，如表3所示。使用文献[12]的方法计算，C_{\mathrm{3}}的子句复杂度为101，C_{\mathrm{4}}的子句复杂度为0，C_{\mathrm{5}}的子句复杂度为206，C_{\mathrm{6}}的子句复杂度为305。由于优先选择子句复杂度小的子句参与演绎，因此演绎顺序为C_{\mathrm{4}}、C_{\mathrm{3}}、C_{\mathrm{5}}、C_{\mathrm{6}}，如表4所示。对比表3和表4，使用文献[12]方法需要选取4个候选子句参与演绎得到空子句，而本文方法只需要选取3个候选子句参与演绎就得到空子句。

文献[12]方法中子句复杂度为子句函数项复杂度以及子句函数项深度复杂度之和。子句函数项复杂度通过对共享变元在子句不同文字中出现的次数（同一个文字中出现多次记作一次）进行计算。子句函数项深度复杂度通过对含非共享变元函数项深度以及含常元函数项深度计算并最终得到子句复杂度。这种方法能较好地使决策文字集中文字的变元项由简单逐渐转变为复杂，且较好地保证矛盾体分离式结构简单，但只是对候选子句内部属性的度量，并没有考虑标准矛盾体对子句的影响，即标准矛盾体的演绎能力存在进一步的提升空间。而在本文方法中，通过刻画项对其他项的合一情况得到项的合一能力，通过对剩余文字进行分析，尽量生成较少文字的矛盾体分离式，从而使矛盾体分离式简单，并将最大剩余文字演绎能力的文字加入决策文字集中，较好地提升了标准矛盾体演绎能力，提高了演绎效率。

4　 基于子句综合权重的多元动态演绎算法

基于上述提出的子句综合权重以及文字演绎能力的度量方法，本文提出了一种基于子句综合权重的多元动态演绎算法，通过起始标准矛盾体得到子句综合权重从而对子句演绎顺序进行排序，同时根据文字演绎能力确定继续加入标准矛盾体的文字，旨在使得标准矛盾体保持较好地消元能力、矛盾体分离式含有更少的文字，从而提升多元演绎能力。算法伪代码描述如算法1。

子句综合权重的多元动态演绎算法的几点说明：

1） 回溯过程作如下处理：

① 清除本次演绎步骤所产生的变元替换项。

② 对本次演绎步骤产生的演绎子句清除演绎标识符。

③ 清除本次演绎步骤记录的演绎路径。

④ 在标准矛盾体中清除本次演绎步骤添加的文字（来自当前演绎子句），恢复矛盾体分离式的文字列表。

2） 算法第23行，矛盾体分离式R有效判断：

① 矛盾体分离式为恒真式，演绎无效。

② 矛盾体分离式为冗余子句，演绎无效。

③ 矛盾体分离式含纯文字，演绎无效。

④ 矛盾体分离式不满足自定义限制条件，演绎无效。

不满足以上四点为有效。

3） 算法第25行，演绎结束条件判断，满足以下5点任一点，演绎结束：

① 矛盾体分离式为空。

② 达到设定的演绎子句总数阈值。

③ 候选子句集中的子句已用完。

④ 达到设定的运行时间阈值。

⑤ 达到设定的内存剩余阈值。

5　 实验及结果分析

5.1　实验准备

当前国际先进的证明器主要有：常年国际竞赛冠军证明器Vampire^[19]、亚军证明器Eprover^[20]，以及著名证明器CSE_E^[21]等。为充分体现本文算法的有效性，将本文算法应用于国际先进证明器Eprover3.1证明器中，即将多元动态演绎搜索路径经过有效筛选后加入到Eprover3.1证明器中作为定理辅助证明，记作CCW_Eprover(Comprehensive Clause Weight_Eprover)证明器，并与原始证明器Eprover3.1进行实验对比。选取2023年CASC-29 FOF组^[22]竞赛例作为实验数据集，共包含500个定理，测试的环境为Intel@ Xeon(R)W-2123 CPU @3.60 GHz X8处理器，32 GB内存，操作系统为Ubuntu 18.04.3 LTS，64位，每个定理的判定时间为标准时间300 s。两组实验在相同的硬件环境下进行测试并获取数据。

5.2　CCW_Eprover证明2023年国际竞赛例判定情况

图2为CCW_Eprover证明器与Eprover3.1证明器对2023年国际竞赛例的定理证明性能对比图，由图2可知，Eprover 3.1证明器能够证明出397个定理，CCW_Eprover证明出定理415个，比Eprover3.1多证明出18个定理。在同一时间（水平线），CCW_Eprover曲线几乎在Eprover3.1右边或与Eprover3.1重合，即CCW_Eprover相比Eprover3.1具有较好地证明效率。实验结果表明加入本文提出的多元动态演绎算法的CCW_Eprover证明器的定理证明能力有了较好地提升。

为进一步验证CCW_Eprover证明器的有效性，对各证明器证明相同的397个定理的平均耗时进行了分析，Eprover3.1证明定理的平均耗时为13.674 s，而CCW_Eprover证明定理的平均耗时为11.870 s，CCW_Eprover证明器在时间效率方面有较好地提升。

CCW_Eprover证明器能够证明Eprover3.1证明器未证明103个定理中的19个定理，占未证明定理总数的18.45%，这19个定理证明情况如表5所示，平均难度系数为0.77，平均证明时间为254.852 s。在证明的19个定理中，子句个数大于200的有15个，占总数的78.95%；文字总数大于600的有17个，占总数的89.47%；变元项个数大于900的有11个，占总数的57.89%；子句最大文字数大于10的有13个，占总数的68.42%。由于CCW_Eprover证明器加入了本文提出的基于子句综合权重的多元动态演绎算法，具有多元性、协同性的特点，每个演绎步骤允许多个子句参与演绎，以分离标准矛盾体的形式同时处理多个文字，所以能较好地处理子句个数较大以及文字总数较大的定理，并且能较好地处理不同子句集下变元项对演绎的影响以及对不同剩余文字的候选子句评估其优先级，能通过回溯机制选择较优子句参与演绎并较好地保持标准矛盾体的演绎能力，较好地处理一些变元项较多以及子句中较多文字的定理。实验表明本文算法能有效提升一阶逻辑自动定理证明器的能力。

将CCW_Eprover证明器与加入文献[12]方法的mcs_Eprover证明器进行对比，如表6所示。针对2021年竞赛例，CCW_Eprover证明器比mcs_Eprover证明器多证明定理3个，其中证明出相同定理个数为393个。CCW_Eprover证明这393个定理平均证明时间为24.91 s，相比mcs_Eprover平均证明时间缩短3.13 s，时间效率方面有较好地提升。针对2023年竞赛例，CCW_Eprover证明器比mcs_Eprover证明器多证明定理8个，其中证明出相同定理个数为402个，其证明效率相当。表6中数据表明，CCW_Eprover证明器在定理证明能力上优于mcs_Eprover证明器，进一步说明本文提出的子句综合权重的多元动态演绎方法能较好地应用于一阶逻辑自动定理证明。

5.3　CCW_Eprover证明难度系数为1的定理判定情况

为了进一步评估基于子句综合权重的多元动态演绎算法的适用性，对CCW_Eprover在TPTP（Thousands of Problems for Theorem Provers）自动定理证明系统的定理测试库中难度系数为1的定理(TPTP库中最难的定理)上进行了测试，表7列出了由CCW_Eprover证明的10个难度系数为1的定理，其中8个定理是国际上其他所有证明器未证明的定理。

CCW_Eprover证明器证明出10个定理，这些定理的平均证明时间为197.696 s，时间效率令人满意。由表7可知，定理SWV276-1的子句个数超过2 000个，文字总数超过6 000个，变元项个数超过6 000个，子句最大文字数超过7个；定理SEU410+3子句个数、文字总数以及变元项个数都超过10 000，子句最大文字数高达123个，其余的8个定理子句个数平均为224个，文字总数平均为456个，变元项个数平均为422个，子句最大文字数平均为6个，即本文提出的基于子句综合权重的多元动态演绎算法能较好地处理子句个数较大、文字总数较大的定理、变元项较多以及子句最大文字数较大的定理。实验结果表明，CCW_Eprover可以证明出一些难度系数为1的问题，并且具有高效性。因此，本文提出的方法及算法可以提升先进的证明器，以证明一些未被解决的难题。

6　 结 语

本文基于多元动态演绎具有多元性、动态性和协同性的演绎特点，通过对标准矛盾体演绎前后合一能力的变化进行分析得到子句影响度，继而对子句影响度、剩余文字以及文字演绎能力三个因素对多元动态演绎过程进行分析，通过这三个因素对子句进行综合度量。基于该子句评估方法，提出了一种多元动态演绎算法，能提升多元动态演绎过程中标准矛盾体的演绎能力。为了验证本文提出的基于子句综合权重的多元动态演绎算法有效性，将该算法应用于国际顶尖一阶逻辑证明器Eprover3.1中进行实验，实验结果表明，加入本文算法能够有效提升Eprover3.1证明能力，提升后的Eprover3.1能证明一些原始Eprover3.1不能证明的定理。

由于一阶逻辑中子句演绎具有复杂性，其定理判定搜索路径是无限的，且候选子句集中并非所有候选子句都对搜索证明过程起作用，同时，候选子句中文字参与演绎顺序不同，也会影响定理证明结果，因此在本文基础上加入有效候选子句评估方法、文字演绎排序方法是下一步的研究内容。此外，自动定理证明具有广泛的应用前景，如程序验证等，未来还可以探讨加入本文方法的自动定理证明器在程序验证上的应用。

参考文献

[1] ROBINSON A， VORONKOV A. Handbook of Auto-mated Reasoning：Volume 1［M］.Amsterdam： Gulf Professional Publishing，2001.

[2] KOVÁCS L. Symbolic computation and automated reasoning for program analysis［C］//International Conference on Integrated Formal Methods. Cham： Springer， 2016： 20-27. DOI： 10.1007/978-3-319-33693-0_2 .

[3] O'HEARN P W. Incorrectness logic［J］. Proceedings of the ACM on Programming Languages， 4（POPL）：1-32（Article No.10）， DOI： 10.1145/3371078 .

[4] REGER G， VORONKOV A. Induction in saturation-based proof search［C］//International Conference on Automated Deduction. Cham： Springer， 2019： 477-494. DOI： 10.1007/978-3-030-29436-6_28 .

[5] BELLOMARINI L， BENEDETTO D， GOTTLOB G， et al. Vadalog： A modern architecture for automated reasoning with large knowledge graphs［J］. Information Systems， 2022， 105： 101528. DOI： 10.1016/j.is.2020.101528 .

[6] QUARESMA P. Automatic deduction in an AI geometry book［C］//International Conference on Artificial Intelligence and Symbolic Computation. Cham： Springer， 2018： 221-226. DOI： 10.1007/978-3-319-99957-9_16 .

[7] TAMMET T， JÄRV P， VERREV M， et al. An experimental pipeline for automated reasoning in natural language （short paper）［C］//International Conference on Automated Deduction. Cham： Springer， 2023： 509-521. DOI： 10.1007/978-3-031-38499-8_29 .

[8] 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 .

[9] XU Y， LIU J， CHEN S W， et al. A novel generalization of resolution principle for automated deduction［C］//Uncertainty Modelling in Knowledge Engineering and Decision Making. Roubaix： WORLD SCIENTIFIC， 2016： 483-488. DOI： 10.1142/9789813146976_0078 .

[10] 曾国艳，徐扬，陈树伟，等.基于多属性决策的一阶逻辑子句选择方法［J］.西南交通大学学报， 2025， 60（1）： 185-193.

[11] ZENG G Y， XU Y， CHEN S W， et al. First-Order Logic Clause Selection Method Based on Multi-Criteria Decision Making［J］. Journal of Southwest Jiaotong University，22025， 60（1）： 185-193 （Ch）.

[12] LIU P Y， CHEN S W， LIU J， et al. An efficient contradiction separation based automated deduction algorithm for enhancing reasoning capability［J］. Knowledge‒Based Systems， 2023， 261： 110217. DOI： 10.1016/j.knosys.2022.110217 .

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

[14] LIN L Y， CAO F， YI J B， et al. Multi-clause dynamic deduction algorithm and application based on clause activity and complexity［J］. Computer Engineering & Science， 2023， 45（12）： 2256-2264 （Ch）.

[15] LIU P Y， XU Y， LIU J， et al. Fully reusing clause deduction algorithm based on standard contradiction separation rule［J］. Information Sciences， 2023， 622： 337-356. DOI： 10.1016/j.ins.2022.11.128 .

[16] 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 .

[17] 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 .

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

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

[20] 刘叙华. 基于归结方法的自动推理［M］. 北京： 科学出版社， 1994.

[21] LIU X H. Automatic reasoning based on resolution method［M］. Beijing： Science Press， 1994（Ch）.

[22] WOS L， ROBINSON G A， CARSON D F. Efficiency and completeness of the set of support strategy in theorem proving［J］. Journal of the ACM， 12（4）： 536-541. DOI： 10.1145/321296.321302 .

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

[24] SCHULZ S. System description： E 1.8［C］//International Conference on Logic for Programming Artificial Intelligence and Reasoning. Berlin： Springer， 2013： 735-743. DOI： 10.1007/978-3-642-45221-5_49 .

[25] 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 .

[26] SUTCLIFFE G， DESHARNAIS M. The 11th IJCAR automated theorem proving system competition–CASC-J11［J］. AI Communications， 2023， 36（2）： 73-91. DOI： 10.3233/AIC-220244 .

基金资助

国家自然科学基金(62366017)

国家自然科学基金(62066018)

江西省教育厅项目(GJJ200818)

江西省教育厅项目(GJJ210828)

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

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