基于矛盾体分离的多元冲突演绎方法及应用

A Multi-Clause Conflict Deduction Method Based on Contradiction Separation and Its Application

摘要

基于二元归结的冲突演绎方法在每个演绎步骤只处理两个子句，其寻求冲突的演绎效率有待提升。提出了一种基于矛盾体分离的多元冲突演绎方法，给出了矛盾体分离多元冲突演绎的定义、学习子句的生成方法、演绎可靠性证明、演绎特点、演绎方法的优势分析以及虚子句的选取方法。在寻求冲突的演绎过程中，每个演绎步骤能处理多个子句，使演绎更容易产生冲突，更容易处理长子句，进而提升了冲突演绎的效率。实验结果表明，矛盾体分离多元冲突演绎方法具有较好的推理能力，比二元冲突演绎方法证明的定理更多，且定理证明所消耗的平均时间更少，加入矛盾体分离多元冲突演绎的Eprover证明器具有较好的搜索证明效率，能有效应用于一阶逻辑自动定理证明，解决难度等级较高的一阶逻辑问题。

Abstract

The conflict deduction method based on binary resolution handles only two clauses in each deduction step, and its efficiency in seeking conflict deduction needs improvement. We propose a multi-clause conflict deduction method based on contradiction separation, and the definition of contradiction separation multi-clause conflict deduction, methods of generation learning clauses, the proof of deduction soundness, its deduction characteristics, advantages analysis of the deduction method, and the selection method of weak clause are given. In the deduction process of seeking conflict, the proposed conflict deduction method allows multiple (two or more) clauses to be involved in each deduction step, which makes it easier to generate conflicts and handle clauses with many literals, thus improving the efficiency of conflict deduction. The experimental results show that the contradiction separation multi-clause conflict deduction method has better reasoning capability, and solves more theorems with the less average proof time than the binary conflict deduction method. The Eprover equipped with our contradiction separation multi-clause conflict deduction method shows high efficiency in search and proof task, making it well-suited for automated theorem proving in first-order logic, particularly for complex problems.

Graphical abstract

关键词

二元归结 / 冲突演绎 / 矛盾体分离 / 学习子句 / 证明器

Key words

binary resolution / conflict deduction / contradiction separation / learning clauses / prover

0　 引 言

自动推理可以通过应用计算机和逻辑推理技术对逻辑公式进行一系列的有效推理，从而更加准确地对公式属性进行判定。这是人工智能领域的一个重要研究课题，其主要内容包括求解命题逻辑公式以及一阶逻辑自动定理证明^[1~3]。一阶逻辑自动定理证明主要思想是利用计算机技术将一阶逻辑定理（含前提与结论）转换为子句集形式，并采用各种推理规则进行一系列的逻辑推理，当推理生成空子句时，该定理得以证明^[4]。一阶逻辑系统比命题逻辑系统具有更强的形式化表达能力，它由谓词符、变元、常数、函数符和逻辑连接词组成，可以更加有效地表达复杂的概念和问题。由于其强大的形式化表达能力，一阶逻辑自动定理证明技术已被普遍应用于解决现实中的各种问题^[5]。

目前，一阶逻辑自动定理证明器主要使用二元归结演绎^[6]和矛盾体分离演绎^[7]方法。矛盾体分离演绎突破了二元归结每个演绎步骤只有两个子句参与演绎的局限性，是一种多元动态演绎方法。相较于二元归结，该演绎方法的每个演绎步骤允许两个及以上的多个子句参与演绎，能够充分发挥子句集中多子句间的协同演绎作用。学者们在此基础上提出了充分复用决策文字的矛盾体分离演绎算法^[8]和多元矛盾体分离协同演绎算法^[9]，实验结果表明，矛盾体分离演绎能够有效应用于一阶逻辑自动定理证明。矛盾体分离演绎具有较强的演绎灵活性，其在演绎路径的高效搜索上仍具有提升空间。因此，高性能的矛盾体分离演绎方法及算法是多元动态演绎研究的关键问题，对提升一阶逻辑自动定理证明能力具有重要意义。

基于二元归结的冲突演绎^[10]是近年来自动推理方法上重要的理论创新，由于该演绎方法每个演绎步骤只能处理两个子句，不能很好地发挥子句之间的协同演绎关系，在处理长子句时效率不高，一定程度上降低了学习子句的生成效率。因此，本文基于矛盾体分离演绎具有多元性、导向性、动态性、协同性^[7，9]等特点，提出了基于矛盾体分离的多元冲突演绎方法，并证明了其可靠性。该方法能发挥多个子句间的动态协同演绎能力，有效提升长子句参与冲突演绎的演绎效率，进而提升了学习子句的生成效率；同时，还具有起步文字灵活性演绎和学习子句生成简单的特点，为一阶逻辑自动定理证明提供了新的科学、可靠方法。

1　 相关知识

一阶逻辑是现代数理逻辑的基础，是一种形式化的语言，用于描述关于对象和关系的命题。一阶逻辑的基本元素包括变元、常元、函数、谓词、析取等^[11，12]。

变元是一种占位符，表示一个未知的对象，常用x、y、z等字母表示。常元则表示一个确定的对象，常用a、b、c等字母表示。谓词则表示两个或多个对象之间的关系，如P(x,y)可以表示对象x与y之间的大于、等于等关系。析取是一种逻辑运算，表示“或”的关系。例如，P(x)\vee Q(x)表示x满足P或者Q中的至少一个条件。在一阶逻辑中，还可以进行变元替换。例如，P(x)中的x可以替换成a，从而得到新的命题P(a)。

一阶逻辑为描述关于对象和关系的命题提供了基础，可用于构造命题、推导定理、进行知识表示和自动推理等。在计算机科学、人工智能等领域都有广泛的应用^[13]。

定义1 归结原理-二元归结^[6，14] 设C_{\mathrm{1}}和C_{\mathrm{2}}是两个无公共变元的子句，C_{\mathrm{1}}=P_{\mathrm{1}}\vee P_{\mathrm{2}}\vee \cdots \vee P_m，C_{\mathrm{2}}=Q_{\mathrm{1}}\vee Q_{\mathrm{2}}\vee \cdots \vee Q_m。若P_{\mathrm{1}}与Q_{\mathrm{1}}存在合一互补（记作\sigma，其中包括有空替换，变元更名替换），则称R(C_{\mathrm{1}},C_{\mathrm{2}})=(C_{\mathrm{1}}^{\mathrm{\sigma }}-P_{\mathrm{1}}^{\mathrm{\sigma }})\vee (C_{\mathrm{2}}^{\mathrm{\sigma }}-Q_{\mathrm{1}}^{\mathrm{\sigma }})为C_{\mathrm{1}}与C_{\mathrm{2}}的二元归结式。

定义2 决策文字 设子句集S=\{C_{\mathrm{1}},C_{\mathrm{2}},\dots ,C_m\}，其中C_i=P_{\mathrm{1}}\vee P_{\mathrm{2}}\vee \cdots \vee P_m，i=\{\mathrm{1,2},\dots ,m\}。子句C_i有文字集合Q_i=\{P_{\mathrm{1}},P_{\mathrm{2}},\dots ,P_m\}，则子句集S有文字集合L=\{Q_{\mathrm{1}},\dots ,Q_i,\dots ,Q_m\}，将集合L中用于单元传播的文字称为决策文字。

例如，在子句C_{\mathrm{1}}=P_{\mathrm{1}}\left(x\right)\vee P_{\mathrm{2}}\left(y\right)和C_{\mathrm{2}}=~P_{\mathrm{1}}\left(a\right)\vee ~P_{\mathrm{2}}\left(b\right)中，文字集合L=\{P_{\mathrm{1}}(x),P_{\mathrm{2}}(y),~P_{\mathrm{1}}(a),~P_{\mathrm{2}}(b)\}，决策文字可以是P_{\mathrm{1}}\left(x\right)或~P_{\mathrm{2}}\left(b\right)。

定义3 二元冲突演绎^[10] 在进行二元归结的过程中，选取一个决策文字，使用该决策文字与子句集中的其他子句按照单元传播的方式进行演绎，当演绎生成空子句时，取与决策文字或替换后的决策文字的否定形式的析取（相同文字合并）作为生成的学习子句，该二元归结过程称为二元冲突演绎。

例1^[10] 设有一阶逻辑子句集S=\{C_{\mathrm{1}},C_{\mathrm{2}},C_{\mathrm{3}},C_{\mathrm{4}}\}，C_{\mathrm{1}}=P(x_{\mathrm{1}})\vee Q，C_{\mathrm{2}}=P(x_{\mathrm{2}})\vee ~Q，C_{\mathrm{3}}=~P(a)\vee Q，C_{\mathrm{4}}=~P(b)\vee ~Q。其中a、b为常元项，x、y为变元项，若采用二元冲突演绎方法，则演绎过程如图1所示。

若选取含变元项的决策文字P(x_{\mathrm{1}})对子句C_{\mathrm{3}}、C_{\mathrm{4}}进行二元冲突演绎，此时需要进行替换，其中替换项\sigma =(a/x_{\mathrm{1}},b/x_{\mathrm{1}})，演绎得到空子句后生成学习子句C_{\mathrm{5}}=~P(a)\vee ~P(b)。

若选取不含变元项的决策文字~P(a)对子句C_{\mathrm{1}}、C_{\mathrm{2}}进行二元冲突演绎，其中替换项\sigma =(a/x_{\mathrm{1}},a/x_{\mathrm{2}})，演绎得到空子句后生成学习子句C_{\mathrm{6}}=P(a)。

分析该二元冲突演绎过程可得出：

(1) 一次演绎生成学习子句的过程需要进行多次二元归结，每个子句参与演绎时只消去一个文字，长子句参与演绎往往需要较多的演绎步骤，导致生成学习子句的效率不高，不易产生冲突。

(2) 演绎过程中寻找冲突的演绎步骤相对独立，缺乏整体性，在算法设计层面不利于发挥子句之间的演绎协同性。

定义4 矛盾体分离规则^[7，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^{{\mathrm{\sigma }}_i}。将C_i^{{\mathrm{\sigma }}_i}的文字分成两个部分C_i^{{\sigma }_i+}和C_i^{{\sigma }_i-}，其中有：

1) 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+}可以为空。

2) 对任意(x_{\mathrm{1}},\dots ,x_m)\in {\displaystyle \prod _{i=\mathrm{1}}^m}{C}_i^{{\sigma }_i-}，存在互补对文字，\stackrel{m}{\underset{i=\mathrm{1}}{\bigwedge }}{C}_i^{{\mathrm{\sigma }}_i-}称为标准矛盾体（separated standard contradiction,简称S-SC）。

3) \stackrel{m}{\underset{i=\mathrm{1}}{\bigvee }}{C}_i^{{\mathrm{\sigma }}_i+}={\mathit{ℂ}}_m^{s\mathrm{\sigma }}(C_{\mathrm{1}},\dots ,C_m)，其中\sigma ={\displaystyle \underset{i=\mathrm{1}}{\overset{m}{\cup }}}{\sigma }_i。

则称{\mathit{ℂ}}_m^{s\mathrm{\sigma }}\left(C_{\mathrm{1}},C_{\mathrm{2}},\dots ,C_m\right)为矛盾体分离式（standard contradiction separation clause,简称S-CSC），该演绎方法称为标准矛盾体分离推理规则(称为矛盾体分离推理规则，简称S-CS规则）。

2　 矛盾体分离多元冲突演绎

2.1　矛盾体分离多元冲突演绎理论

定义5 虚子句 将决策文字重构为新的单元子句，该新单元子句称为虚子句。例如，在子句C_{\mathrm{1}}=P_{\mathrm{1}}\left(x_{\mathrm{1}}\right)\vee P_{\mathrm{2}}\left(x_{\mathrm{2}}\right)中，重构的虚子句是P_{\mathrm{1}}\left(x_{\mathrm{1}}\right)或P_{\mathrm{2}}\left(x_{\mathrm{2}}\right)。

定义6 矛盾体分离多元冲突演绎 在矛盾体分离演绎过程中，若演绎步骤满足以下条件：

(1) 选取虚子句优先参与矛盾体分离演绎；

(2) 虚子句允许连续参与矛盾体分离演绎；

(3) 除了虚子句外，其他参与演绎的子句均来自于子句集中；

(4) 演绎最终生成的矛盾体分离式为空子句；

则这样的矛盾体分离演绎过程称为矛盾体分离多元冲突演绎。

定义7 矛盾体分离多元冲突演绎学习子句 当演绎步骤满足定义6，取虚子句中的决策文字或替换后的决策文字的否定形式的析取作为（相同文字进行合并）学习子句。该学习子句称为矛盾体分离多元冲突演绎分离式。

图2为矛盾体分离多元冲突演绎步骤图。演绎步骤从选择决策文字重构虚子句开始，至演绎得到空子句结束。其中有虚子句参与矛盾体分离多元冲突演绎得到空子句时生成学习子句，即生成新子句；当学习子句与原始子句进行矛盾体分离多元冲突演绎生成空子句时被判定的定理得证。

例2 设一阶逻辑子句集S=\{C_{\mathrm{1}},C_{\mathrm{2}},C_{\mathrm{3}},C_{\mathrm{4}}\}，C_{\mathrm{1}}=P_{\mathrm{2}}(x_{\mathrm{1}})\vee P_{\mathrm{1}}(a)，C_{\mathrm{2}}=P_{\mathrm{2}}(x_{\mathrm{2}})\vee ~P_{\mathrm{1}}(a)，C_{\mathrm{3}}=~P_{\mathrm{2}}(f(a))\vee P_{\mathrm{1}}(b)，C_{\mathrm{4}}=~P_{\mathrm{2}}(x_{\mathrm{2}})\vee ~P_{\mathrm{1}}(b)。其中a、b为常元项，x_{\mathrm{1}}、x_{\mathrm{2}}为变元项，f(a)为函数项。若采用矛盾体分离多元冲突演绎的方式进行演绎，则有如下步骤：

(1) 从C_{\mathrm{3}}选择文字~P_{\mathrm{2}}(f(a))重构为虚子句C_{\mathrm{3}}^{\mathrm{\text{'}}}=~P_{\mathrm{2}}(f(a))；

(2) 优先使虚子句C_{\mathrm{3}}^{\mathrm{\text{'}}}参与矛盾体分离演绎；

(3) 应用矛盾体分离规则有{\mathit{ℂ}}_m^{s\mathrm{\sigma }}\left(C_{\mathrm{3}}^{\mathrm{\text{'}}},C_{\mathrm{1}},C_{\mathrm{2}}\right)=\mathrm{\varnothing }，其中\sigma =\left(f(a)/x_{\mathrm{1}},f(a)/x_{\mathrm{2}}\right)；

(4) 取虚子句C_{\mathrm{3}}^{\mathrm{\text{'}}}中文字的否定形式，得到文字P_{\mathrm{2}}(f(a))；

在演绎过程中，替换后得到的两个文字均为~P_{\mathrm{2}}(f(a))，合并两个相同的文字，则生成的学习子句C_{\mathrm{5}}=P_{\mathrm{2}}(f(a))。

定理1 矛盾体分离多元冲突演绎定理 设一阶逻辑子句集S=\{C_{\mathrm{1}},C_{\mathrm{2}},\dots ,C_n\}，如果对于任意的i=\mathrm{1,2},\dots ,t：

(1) {\Phi }_i\in S；

(2) 存在及替换{\sigma }_{r_{\mathrm{1}}},{\sigma }_{r_{\mathrm{2}}},\dots ,{\sigma }_{r_{ki}}使{\Phi }_i=R_{ki}({\Phi }_{r_{\mathrm{1}}}^{{\mathrm{\sigma }}_{r_{\mathrm{1}}}},{\Phi }_{r_{\mathrm{2}}}^{{\mathrm{\sigma }}_{r_{\mathrm{2}}}},\dots ,{\Phi }_{r_{ki}}^{{\mathrm{\sigma }}_{r_{ki}}})；

则{\Phi }_{\mathrm{1}},{\Phi }_{\mathrm{2}},\dots ,{\Phi }_t为一阶逻辑中基于矛盾体分离多元冲突演绎方法的从S到子句{\Phi }_t的矛盾体分离多元冲突演绎分离式序列。

定理2 矛盾体分离多元冲突演绎可靠性 设一阶逻辑子句集S=\left\{C_{\mathrm{1}},C_{\mathrm{2}},\dots ,C_m\right\}，{\Phi }_{\mathrm{1}},{\Phi }_{\mathrm{2}},\dots ,{\Phi }_t为基于标准矛盾体分离的多元冲突演绎从S到{\Phi }_t的矛盾体分离多元冲突演绎分离式序列。当{\Phi }_t为空子句，则子句集S不可满足。

证 设一阶逻辑子句集S=\left\{C_{\mathrm{1}},C_{\mathrm{2}},\dots ,C_m\right\}，根据条件有矛盾体分离多元冲突演绎：\stackrel{m}{\underset{i=\mathrm{1}}{\bigvee }}{C}_i^{{\sigma }_i+}={\mathit{ℂ}}_m^{s\sigma }(C_{k_{\mathrm{1}}},\dots ,C_{k_i},C_{k_{i+\mathrm{1}}},\dots ,C_m)为空子句，其中C_{k_{\mathrm{1}}},\dots ,C_{k_i},C_{k_i+\mathrm{1}},\dots ,{\mathrm{C}}_m共m个子句，C_{k_{\mathrm{1}}},\dots ,C_{k_i}为虚子句（虚子句为单元子句，假定有C_{k_{\mathrm{1}}}=P_k,\dots ,C_{k_i}=P_k）,\sigma ={\displaystyle \underset{i=\mathrm{1}}{\overset{m}{\cup }}}{\sigma }_i,则将\stackrel{m}{\underset{i=\mathrm{1}}{\bigvee }}{C}_i^{{\sigma }_i+}={\mathit{ℂ}}_m^{s\sigma }(C_{k_{\mathrm{1}}},\dots ,C_{k_i},C_{k_i+\mathrm{1}},\dots ,C_m)中参与演绎的虚子句进行剥离，则{\mathit{ℂ}}_{m-k_i}^{s\sigma }(C_{k_i+\mathrm{1}},\dots ,{\mathrm{C}}_m)=\stackrel{m}{\underset{j=k_i+\mathrm{1}}{\bigvee }}{C}_j^{{\sigma }_j+}，其中分离的标准矛盾体为\stackrel{m}{\underset{j=k_i+\mathrm{1}}{\bigwedge }}{C}_j^{{\sigma }_j-}，\sigma ={\displaystyle \underset{i=\mathrm{1}}{\overset{m}{\cup }}}{\sigma }_i，即矛盾体分离多元冲突演绎分离式\stackrel{m}{\underset{j=k_i+\mathrm{1}}{\bigvee }}{C}_j^{{\sigma }_j+}符合矛盾体分离规则定义，也为矛盾体分离式。当矛盾体分离多元冲突演绎分离式为空子句时，子句集S不可满足，定理得证。

2.2　学习子句生成过程

对于学习子句的生成过程，虚子句选取的不同会影响演绎生成学习子句的过程，虚子句的选取分三种情况：

(1) 不含有变元的项，即只含常元项；

(2) 含有变元的项且该虚子句可重复使用的；

(3) 含有变元的项但是虚子句不可重复使用的。

例3 设有一阶逻辑子句集S=\{C_{\mathrm{1}},C_{\mathrm{2}},C_{\mathrm{3}},C_{\mathrm{4}},C_{\mathrm{5}},C_{\mathrm{6}}\}，C_{\mathrm{1}}=P_{\mathrm{1}}(x)\vee Q_{\mathrm{1}}(a)，C_{\mathrm{2}}=P_{\mathrm{1}}(y)\vee ~Q_{\mathrm{1}}(a)，C_{\mathrm{3}}=~P_{\mathrm{1}}(a)\vee Q_{\mathrm{1}}\left(f(b)\right)，C_{\mathrm{4}}=~P_{\mathrm{1}}(y)\vee ~Q_{\mathrm{1}}\left(f(b)\right)，C_{\mathrm{5}}=P_{\mathrm{1}}(b)\vee Q_{\mathrm{2}}\left(f(a)\right)，C_{\mathrm{6}}=P_{\mathrm{1}}(y)\vee ~Q_{\mathrm{2}}\left(f(a)\right)。其中a、b为常元项，x、y为变元项，f(a)、f(b)为函数项，若采用矛盾体分离多元冲突演绎的方式进行演绎，则生成学习子句的过程分别如表1至表4所示。

若选取不含变元项的虚子句C_{\mathrm{1}}^{\mathrm{\text{'}}}=~P_{\mathrm{1}}(a)对子句C_{\mathrm{1}}和C_{\mathrm{2}}进行矛盾体分离多元冲突演绎，演绎过程如表1所示，其中替换项\sigma =\left(a/x,a/y\right)，生成学习子句C_{\mathrm{7}}=P_{\mathrm{1}}\left(a\right)。对于不含变元项的虚子句，需要对参与演绎的子句中与虚子句合一文字的变元项做替换，在采用同一个常元项对不同的变元项做替换时，最终生成的学习子句文字相同，可以进行合并，即生成的学习子句是单元子句。

若选取含变元项的虚子句C_{\mathrm{2}}^{\text{'}}=P_{\mathrm{1}}(x)，重复使用C_{\mathrm{2}}^{\mathrm{\text{'}}}对子句C_{\mathrm{3}}和C_{\mathrm{4}}进行矛盾体分离多元冲突演绎，演绎过程如表2所示，分析可知，在C_{\mathrm{3}}和C_{\mathrm{4}}中，与C_{\mathrm{2}}^{\mathrm{\text{'}}}合一互补的文字中，所含常元项不同，若对虚子句执行替换\sigma =(a/x)。此时C_{\mathrm{2}}^{\mathrm{\text{'}}}=P_{\mathrm{1}}(a/x)，无法与C_{\mathrm{4}}中的文字合一互补。因此，可以再使用一次未执行替换的虚子句C_{\mathrm{2}}^{\mathrm{\text{'}}}，替换项\sigma =(b/x)，重复使用虚子句的过程中执行了两次不同的替换，得到含常元项不同的文字，最终演绎生成学习子句C_{\mathrm{8}}=~P_{\mathrm{1}}(a)\vee ~P_{\mathrm{1}}(b)。

若选取含变元项的虚子句C_{\mathrm{3}}^{\mathrm{\text{'}}}=~P_{\mathrm{1}}(x)，不重复使用C_{\mathrm{3}}^{\mathrm{\text{'}}}对子句C_{\mathrm{5}}和C_{\mathrm{6}}进行矛盾体分离多元冲突演绎，演绎过程如表3所示，执行替换\sigma =(b/y)，此时C_{\mathrm{3}}^{\mathrm{\text{'}}}=~P_{\mathrm{2}}(b/y)，不重复使用含变元项的虚子句参与演绎生成学习子句C_{\mathrm{9}}=P_{\mathrm{1}}(b)。

使用生成的学习子句C_{\mathrm{7}}、C_{\mathrm{8}}、C_{\mathrm{9}}进行矛盾体分离多元冲突演绎，生成的演绎分离式为空子句。演绎过程如表4所示。

综上所述，在进行矛盾体分离多元冲突演绎的过程中，首先通过选取子句集中非单元子句所含有的文字作为虚子句。接着，使用该虚子句（虚子句允许重复使用）与子句集中的其他子句进行多元协同演绎直到最终生成的矛盾体分离式为空子句，此时取虚子句中的决策文字或替换后的决策文字的否定形式的析取（相同文字合并）作为生成的学习子句。学习子句的生成是由分离标准矛盾体产生的，其满足矛盾体分离规则。

3　 矛盾体分离多元冲突演绎优势

为进一步说明矛盾体分离多元冲突演绎方法的演绎步骤，本章将基于实例分析的过程阐述二元冲突演绎与矛盾体分离多元冲突演绎的区别，分析矛盾体分离多元冲突演绎的优势。

例4 设有一阶逻辑子句集S=\{C_{\mathrm{1}},C_{\mathrm{2}},C_{\mathrm{3}},C_{\mathrm{4}}\}，C_{\mathrm{1}}=P_{\mathrm{1}}(x_{\mathrm{1}})\vee P_{\mathrm{2}}(a)，C_{\mathrm{2}}=P_{\mathrm{1}}(x_{\mathrm{2}})\vee~P_{\mathrm{2}}(a)，C_{\mathrm{3}}=~P_{\mathrm{1}}(a)\vee P_{\mathrm{2}}(a)，C_{\mathrm{4}}=~P_{\mathrm{1}}\left(f(b)\right)\vee ~P_{\mathrm{2}}(a)。若采用二元冲突演绎，则演绎过程如图3所示。

相应地，若采用矛盾体分离多元冲突演绎，则演绎过程如表5至表8所示。

采用虚子句C_{\mathrm{1}}^{\mathrm{\text{'}}}=P_{\mathrm{1}}(x_{\mathrm{1}})进行矛盾体分离多元冲突演绎，演绎过程如表5所示。演绎完成后，生成学习子句C_{\mathrm{5}}=~P_{\mathrm{1}}(a)\vee ~P_{\mathrm{1}}\left(f(b)\right)。

采用虚子句C_{\mathrm{2}}^{\mathrm{\text{'}}}=~P_{\mathrm{1}}(a)进行矛盾体分离多元冲突演绎，演绎过程如表6所示。演绎完成后生成学习子句C_{\mathrm{6}}=P_{\mathrm{1}}(a)。

采用虚子句C_{\mathrm{3}}^{\mathrm{\text{'}}}=P_{\mathrm{1}}\left(f(b)\right)进行矛盾体分离多元冲突演绎，演绎过程如表7所示，演绎完成后，生成学习子句C_{\mathrm{7}}=P_{\mathrm{1}}\left(f(b)\right)。

使用生成的学习子句C_{\mathrm{5}}、C_{\mathrm{6}}、C_{\mathrm{7}}进行矛盾体分离多元冲突演绎，演绎过程如表8所示，生成的矛盾体分离式为空子句，例4得证。

例5 设有一阶逻辑子句集S=\{C_{\mathrm{1}},C_{\mathrm{2}},C_{\mathrm{3}},C_{\mathrm{4}}\}，C_{\mathrm{1}}=P_{\mathrm{1}}(a)，C_{\mathrm{2}}=P_{\mathrm{2}}(b),C_{\mathrm{3}}=~P_{\mathrm{1}}(a)\vee Q(c)，C_{\mathrm{4}}=~P_{\mathrm{2}}(b)\vee ~Q(c)。采用虚子句C_{\mathrm{1}}^{\mathrm{\text{'}}}=~P_{\mathrm{1}}(a)进行矛盾体分离多元冲突演绎，演绎过程如表9所示。

此次演绎过程中虚子句并未参与演绎，通过一次矛盾体分离多元冲突演绎可以直接得到空子句。改进的演绎方式灵活性较强，可以充分使用原始子句集中的子句参与演绎，当生成的学习子句为空子句时，被判定的定理得证。

从两种演绎过程可得出，矛盾体分离多元冲突演绎有如下优势：

(1) 多元演绎。矛盾体分离多元冲突演绎将二元冲突演绎中两两独立的多个二元归结步骤改进为在一个多元演绎步骤中进行，具有多元演绎的特点，且演绎的整体性更强。

(2) 动态演绎。矛盾体分离多元冲突演绎参与演绎的子句具有动态性，在演绎过程中可以根据整体演绎的情况及时判断演绎有效性并动态更换演绎子句。

(3) 协同演绎。矛盾体分离多元冲突演绎能发挥多个子句协同演绎的特点，演绎过程中具有更大的导向性和灵活性。

(4) 具有更强的文字消去能力。矛盾体分离多元冲突演绎参与演绎的每个子句可以消去多个文字，更易产生冲突。

(5) 更易生成学习子句。矛盾体分离多元冲突演绎有效约减了演绎步骤，在使用虚子句进行演绎生成空子句的过程中，取虚子句中的决策文字或替换后的决策文字的否定形式的析取，即可得到学习子句。

(6) 包含定理证明过程。矛盾体分离多元冲突演绎允许学习子句是空子句，当学习子句为空子句时，被判定的定理得到证明，即改进后的冲突演绎方法在寻求冲突过程中也可用于定理的判定。

综上所述，矛盾体分离多元冲突演绎可以充分发挥矛盾体分离演绎与二元冲突演绎两者的优势，使非单元子句中的文字可以参与演绎生成学习子句。当虚子句未参与矛盾体分离多元冲突演绎，即学习子句参与演绎生成空子句时，矛盾体分离多元冲突演绎方法可以直接得到需要证明的定理的判定结果。

4　 虚子句的选取原则

由于学习子句的生成效率和有效性与一阶逻辑自动定理证明直接相关，而学习子句的生成受到虚子句选取的影响。故而，虚子句的选取对于提升矛盾体分离多元冲突演绎的效率具有重要的意义。矛盾体分离多元冲突演绎需要考虑虚子句的有效选取和充分发挥多个子句间的协同演绎能力，选择不同的虚子句进行演绎，会生成不同的学习子句。虚子句选择的不同会影响学习子句的生成质量，即无效的学习子句会增加无效的演绎搜索路径，降低自动定理证明的效率。因此，选取合适的虚子句参与演绎，充分发挥多子句的协同演绎能力进而生成高质量的学习子句，是提升矛盾体分离演绎能力和效率的有效方法。

对于如何选取有效的虚子句进而生成学习子句，参见2.2节可知，生成的学习子句越简单（即得到单元子句），参与演绎的有效性就越高，其参与矛盾体分离多元冲突演绎搜索演绎冲突的能力就越强；其次，含变元项的虚子句是否重复使用对于学习子句的生成也有影响。综上分析，虚子句有以下选取方式：

(1) 基于生成学习子句最简原则。优先选取只含常元项的文字作为虚子句。当虚子句只含常元项时，在矛盾体分离多元冲突演绎的变元替换过程中，更容易生成相同文字析取的学习子句。由于文字相同，这些学习子句可以进行合并，使得生成的学习子句为单元子句。其次，只含常元项的虚子句参与演绎还具有演绎替换式简洁的特点。

(2) 基于文字互补碰撞原则。优先选取子句集中相似度高的文字作为合一互补文字，特别是当某个文字在子句集中出现频次高，并且存在与该文字合一互补的文字项时，更应优先考虑选择该合一互补文字作为虚子句。在文字相似度高的情况下，该虚子句可以与更多的子句进行矛盾体分离多元冲突演绎，从而在一次演绎过程中更容易得到学习子句，充分发挥子句间多元动态协同演绎的特点。

(3) 基于充分使用虚子句原则。优先选取含变元项的文字，演绎过程中含变元项的虚子句可以重复使用，虚子句在参与矛盾体分离多元冲突演绎时，由于含有的变元项存在多种合一方式，导致虚子句在参与演绎时存在多种演绎路径选择。因此，基于充分使用虚子句的主要原则是：在存在多种演绎路径的情况下，虚子句参与矛盾体分离多元冲突演绎后，在已构建的标准矛盾体的基础上尽可能的重复使用该虚子句继续演绎，以最大限度地提升学习子句的生成能力。

5　 实验结果与分析

5.1　实验准备

以下将矛盾体分离多元冲突演绎方法简记为CSCD (contradiction separation multi-clause conflict deduction)。接下来通过以下3组实验来验证CSCD的有效性：(1) 将基于CSCD实现的证明器与基于二元冲突演绎方法的Scavenger^[15]（Scavenger源代码链接：https://gitlab.com/aossie/Scavenger）证明器进行比较。(2) 将CSCD应用到国际顶尖证明器Eprover2.4^[16]（Eprover2.4源代码链接：http://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_2.4/E.tgz）中（记作CSCD_E）,与原始的Eprover2.4进行比较。(3) 使用CSCD_E对TPTP问题库中Rating为1（Rating表示问题的难度等级，其中Rating为1的是目前国际所有的证明器都无法证明的问题）的问题^[17]进行测试，以验证CSCD在解决复杂定理上的有效性。

为确保实验的公平性，其中(1)和(2)选取TPTP问题库CASC-26 FOF组^[18]竞赛例作为实验数据集，共含有500 个竞赛例。测试计算机环境为Intel Xeon(R) W-2123 CPU @ 3.60GHz x 8处理器和32 GB内存，运行Ubuntu 18.04 64位操作系统。每个问题测试的时间限制为300 s（标准时间）。

5.2　CSCD与Scavenger的对比分析

相比基于二元冲突演绎理论实现的Scavenger，CSCD证明器基于本文提出的矛盾体分离多元冲突演绎理论，具有多元演绎的特性。在总数为500 个的竞赛例中，CSCD证明器证明了177 个，比Scavenger多106 个，这表明CSCD证明器在定理证明能力上优于Scavenger。其中，CSCD证明器证明定理平均用时49.426 s，Scavenger平均用时58.730 s。CSCD证明器在定理证明平均时间上减少了9.304 s，具有较好的时间效率。

CSCD允许同时处理多个子句，在推理过程中具备更大的灵活性，从而能够更好地探索证明路径，增加搜索到可行证明路径的概率。实验结果表明，CSCD具有较好的推理能力。

5.3　CSCD_E的实验分析

Eprover是国际顶尖的一阶逻辑自动定理证明器，其推理核心仍采用二元演绎方法。为了进一步验证CSCD能有效应用于一阶逻辑自动定理证明，将CSCD_E与Eprover2.4进行比较。由实验结果可知，CSCD_E成功证明了398 个定理，比原始Eprover2.4多16 个定理，证明的定理比率提升了3.2%，占Eprover2.4未证明定理总数的13.5%。CSCD_E证明398 个定理平均用时20.320 s，而证明382 个定理平均用时为11.817 s。另一方面，Eprover2.4证明382 个定理平均用时14.316 s。则当证明定理数量相同时，CSCD_E相较于Eprover2.4，在证明定理的平均时间上减少了2.499 s。

图4给出了CSCD_E和Eprover2.4在总数为500 个竞赛例上的运行时间对比。由图4可知，当处于相同时间线时，CSCD_E的曲线总体位于Eprover2.4的右侧。这表明在相同的时间限制条件下，CSCD_E能够搜索到更多定理证明路径，定理证明个数优于Eprover2.4。在定理证明数量一致时，曲线越接近横坐标，表示证明器所用的时间越少，CSCD_E的曲线在大部分范围内都更靠近横坐标，表明其在多数定理证明上比Eprover2.4更快。

CSCD_E增加了矛盾体分离多元冲突演绎方法，能充分地利用冲突信息，生成学习子句以指导证明搜索过程，通过快速的回溯机制重新选择子句进行演绎，具有较好的证明搜索效率。实验结果表明，CSCD能有效应用于一阶逻辑自动定理证明。

5.4　CSCD对Rating为1问题的证明情况

通过上述两组实验，已经表明CSCD在证明一般问题上的优势。为了进一步验证CSCD在判定难度等级高的问题上的有效性，使用CSCD_E对TPTP问题库中Rating为1的问题进行了实验测试。Rating为1的问题目前难度系数是最高的，这类问题往往涉及更多的子句、文字数量或复杂的逻辑结构。对这类问题进行测试，可以更好的评估CSCD的能力。

表10列出了CSCD_E证明的5 个Rating为1的问题判定情况，定理判定平均用时153.689 s，这5个定理所含的平均子句个数为247，平均文字总数为501，具有较大的子句和文字规模，其中问题NUM726+4的子句个数为809，文字总数为1 547。

CSCD具有多子句协同演绎的特性，在同时处理多个子句时，能更好的体现问题本身的逻辑结构，具有较好的文字消元能力并能灵活地控制演绎的条件。实验结果表明，CSCD能有效应用于解决难度等级较高的一阶逻辑问题。

6　 结 语

本文提出了一种基于矛盾体分离的多元冲突演绎方法，主要对矛盾体分离多元冲突演绎的理论和方法进行了介绍，通过分析学习子句的生成过程阐述了该方法的优势，并进一步探讨了虚子句的选取原则，是二元冲突演绎在多元演绎层面的推广。矛盾体分离多元冲突演绎方法能够减少演绎步骤，演绎过程中允许多个子句参与协同演绎，更容易生成学习子句。在寻求演绎冲突过程中，能更好地处理长子句。为了验证矛盾体分离多元冲突演绎方法的有效性，通过3组实验表明了提出的演绎方法能较好的应用于一阶逻辑自动定理证明。

在矛盾体分离多元冲突演绎方法中，虚子句的选取对于学习子句的生成具有重要影响，因此下一步研究将在此基础上提出更有效的虚子句选取原则。同时，在寻找演绎冲突的过程中，不同的子句参与演绎对生成空子句具有直接的影响，因此较优的子句选择方法也是下一步研究的重要内容。

参考文献

[1] MOGHADDAM G I， PADMANABHAN R， ZHANG Y. Automated reasoning with power maps［J］. Journal of Automated Reasoning， 2020， 64（4）： 689-697. DOI： 10.1007/s10817-019-09524-0 .

[2] FROM A H， SCHLICHTKRULL A， VILLADSEN J. A sequent calculus for first-order logic formalized in Isabelle/HOL［J］. Journal of Logic and Computation， 2023， 33（4）： 818-836. DOI： 10.1093/logcom/exad013 .

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

[4] BOLLIG B， SANGNIER A， STIETEL O. On the satisfiability of local first-order logics with data［EB/OL］. 2023： arXiv： 2307.00831. DOI: 10.4204/eptcs.370.1 .

[5] GOLOVACH P A， STAMOULIS G， THILIKOS D M. Model-checking for first-order logic with disjoint paths predicates in proper minor-closed graph classes［C］//Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms （SODA）. Philadelphia： Society for Industrial and Applied Mathematics， 2023： 3684-3699. DOI： 10.1137/1.9781611977554.ch141 .

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

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

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

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

[10] SLANEY J， PALEO B W. 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 .

[11] STEEN A， SUTCLIFFE G， FONTAINE P， et al. Representation， verification， and visualization of tarskian interpretations for typed first-order logic［C］//EPiC Series in Computing， 2023， 94： 369-385. DOI： 10.29007/1rhx .

[12] GRILLETTI G， CIARDELLI I. Games and cardinalities in inquisitive first-order logic［J］. The Review of Symbolic Logic， 2023， 16（1）： 241-267. DOI： 10.1017/s1755020321000198 .

[13] ALMAKHOUR M， SLIMAN L， SAMHAT A E， et al. Verification of smart contracts： A survey［J］. Pervasive and Mobile Computing， 2020， 67： 101227. DOI： 10.1016/j.pmcj.2020.101227 .

[14] 曹锋. 一种基于矛盾体分离演绎的一阶逻辑自动定理证明器研究［D］. 成都： 西南交通大学， 2020. DOI： 10.27414/d.cnki.gxnju.2020.000043 .

[15] CAO F. Study on a first-order logic automated theorem prover based on contradiction separation deduction［D］. Chengdu： Southwest Jiaotong University， 2020. DOI： 10.27414/d.cnki.gxnju.2020.000043（Ch ）.

[16] ITEGULOV D， SLANEY J， WOLTZENLOGEL PALEO B. Scavenger 0.1： A theorem prover based on conflict resolution［C］//International Conference on Automated Deduction. Cham： Springer， 2017： 344-356. DOI： 10.1007/978-3-319-63046-5_21 .

[17] SCHULZ S， CRUANES S， VUKMIROVIĆ P. Faster， higher， stronger： E 2.3［C］//International Conference on Automated Deduction. Cham： Springer， 2019： 495-507. DOI： 10.1007/978-3-030-29436-6_29 .

[18] SUTCLIFFE G. The TPTP problem library and associated infrastructure［J］. Journal of Automated Reasoning， 2017， 59（4）： 483-502. DOI： 10.1007/s10817-017-9407-7 .

[19] SUTCLIFFE G. The CADE-26 automated theorem proving system competition–CASC-26［J］. AI Communications， 2017， 30（6）： 419-432. DOI： 10.3233/aic-170744 .

基金资助

国家自然科学基金(62366017)

国家自然科学基金(62066018)

国家自然科学基金(62106206)

江西省科技厅资助项目(20212ACB202003)

江西省教育厅资助项目(GJJ210828)

江西省教育厅资助项目(GJJ200818)

江西省教育厅资助项目(GJJ180482)