Control Strategy Based on State Machine for Fuel Cell Hybrid Power System

一阶逻辑是经典的逻辑理论，基于一阶逻辑的定理机器证明和自动推理是人工智能领域的重要研究课题. 1965年，Robinson^[1]提出的归结原理是实现定理自动证明的工具之一，推动了自动推理的发展.自动定理证明器（ATP）通过输入被形式化为一阶逻辑的前提条件和结论，自动从前提条件推出结论. 研究ATP有重要的应用价值：一阶逻辑可以形式化研究软件验证^[2]、数学定理证明^[3]、信息安全的程序自动验证^[4]等.

因为一阶逻辑子句含有变元的函数项，所以搜索空间是无限的，这使得一阶逻辑定理的证明成为一个无限问题. 目前，ATP采用的推理规则主要有2类：一类是归结原理，每次有且仅有2个子句参与归结，只消去一组互补对文字，生成的归结式含有大量文字；另一类是2018年Xu等^[5]提出的标准矛盾体分离（S-CS）规则，突破了静态二元归结的限制，允许多个子句动态参与演绎，生成大量单元子句. Xu等^[6]同年分析了（S-CS）规则的优势，如动态性、协同性、鲁棒性等.

1.   相关工作

根据上述提到的2类推理方法，ATP选择其中一种作为推理机制. 确定推理机制后，提高ATP的证明效率是关键. ATP选择子句集中的子句，按照推理规则进行推理，直至推出空子句，定理得证. 子句的选择是ATP必不可少的部分. 理论和实验表明，有些子句会多次参与演绎推理，而有些则未能参与. 因此，通过启发式策略选取合适的子句对提升ATP性能至关重要. 由于不同推理规则之间存在本质差异，针对基于不同推理规则的ATP，应采用不同的启发式策略.

当前，针对ATP的启发式策略已有广泛研究. 例如，基于重写规则的E中多种项排序策略^[7]、基于二元归结的Vampire中动态选择策略^[8]. 基于S-CS规则的启发式策略包括子句演绎权重^[9]、决策文字选择策略和矛盾体分离式策略^[10]等. 这些子句选择策略通常通过设定策略优先级来决定子句参与演绎的顺序，优先级越高的策略对应的子句会优先被选择. 然而，这些策略有时需要多次比较子句优先级，才能选择出一个合适的子句，在一定程度上会影响对子句的评估.

为解决该问题，本文提出一种新的子句选择框架，将多种策略选择子句视为多属性决策问题. 不同的子句选择策略反映了子句的不同属性特征，因此，每种策略对应不同的子句属性，为多属性决策（MCDM）方法综合评估子句提供了基础. 本文利用MCDM方法，根据多种子句属性值对各子句进行综合评估.

目前，已有多种经典的MCDM方法，例如逼近理想解法（TOPSIS） ^[11]、VIKOR^[12]和偏好顺序结构评估法（PROMETHEE） ^[13]等. 其中，PROMETHEE能在丢失很少属性信息情况下对候选子句进行部分或完全排序，因而在实际决策过程中较其他MCDM方法具有更高的灵活性. PROMETHEE的核心思想是通过正、负优先流以及净占优流对候选子句进行排序，其已扩展出多种形式^[14]，包括PROMEHTEE Ⅰ 、PROMETHEE Ⅱ 、PROMETHEE Ⅲ、PROMETHEE Ⅳ等. 其中，PROMETHEE Ⅱ能够对候选子句进行完全排序，且无需对子句属性值进行量纲化和规范化处理，从而避免了信息偏差. 因此，本文选择PROMETHEE Ⅱ对子句进行评估.

本文采用MCDM方法评估子句有如下优点：1） MCDM基于子句的多种客观信息进行评估，有效避免了人为设定策略优先级的问题，一定程度上减少了为设置优先级而进行的大量实验测试. 2） MCDM已有成熟的研究，为多属性决策评估子句提供了理论依据，支持多种子句属性同时参与决策评估. 3） WCDM是一种高效的动态综合评估方法，能够反映子句的多种属性特征，通过组合策略进行评估，通常优于单一策略.

本文基于S-CS规则的多个子句动态参与演绎的特性，在演绎过程中应用PROMETHEE Ⅱ方法对子句进行排序. 当子句属性值在演绎过程中发生更新时，子句排序也会相应更新. 对比实验结果表明，基于S-CS规则的PROMETHEE Ⅱ方法能有效提升ATP的性能.

2.   矛盾体分离规则

首先介绍本文涉及的一阶逻辑的相关概念^[15].原子公式由谓词符号（如${P}$）和项组成. 其中，变元（如${x}$, ${y}$）、常元（如${a}$）和函数符（如${f}$）都是项. 原子公式${A}$及其否定${\neg A}$称为文字，称${A}$与${\neg A}$为互补对. 若干个文字的析取称为子句，只有一个文字的子句称为单元子句. 若干个子句的合集称为子句集. 一个替换是形如{${{t}}_{{1}}/{{y}}_{{1}} , t_2/y_2,\cdots , t_N/y_N$}的有限集合，其中，${{y}}_{{J}}\;（{J=}{1}{,}2,\cdots{,N} \text{）}$为变量符号，${N}$为变量个数, ${{t}}_{{J}}$为不同于${{y}}_{{J}}$的项. 集合中$y_J$各不相同，称${{t}}_{{J}}$为替换的分子，${{y}}_{{J}}$为替换的分母.

二元归结方法只允许（有互补对的） 2个子句参与归结，从而仅消去1组互补对文字；而矛盾体分离规则允许多个子句参与演绎，每次演绎可消去多组互补对，是二元归结方法的拓展.

矛盾体分离规则^[5]：设一阶逻辑子句集 $S= \{{C_1,C_2,\cdots, C_m}\}$（${m}$为子句个数），子句 ${{C}}_{{1}}$、${{C}}_{{2}}$、$\cdots$、${{C}}_{{m}}$之间不存在相同变元（若存在不同的子句有相同的变元，则需对变元更名），称由子句集${S}$产生新子句的推理规则为标准矛盾体分离规则，简称S-CS规则.

对于任意子句${{C}}_{{k}}\;（{k=}{1,2}{,}{\cdots}{,m}$），存在替换${{\sigma }}_{{k}}$可以应用于子句${{C}}_{{k}}$（${{\sigma }}_{{k}}$可以为空替换），使得${{C}}_{{k}}$中相同的文字可以合并，得到子句${{C}}_{{k}{{\sigma }}_{{k}}}.$ 将 ${{C}}_{{k}{{\sigma }}_{{k}}}$分为两部分子句（${{C}}_{{k}{{\sigma }}_{{k}}}^{-}$和${{C}}_{{k}{{\sigma }}_{{k}}}^{{ + }}$），满足：

1） ${{C}}_{{k}{{\sigma }}_{{k}}}{=}{{C}}_{{k}{{\sigma }}_{{k}}}^{-}{\vee} {{C}}_{{k}{{\sigma }}_{{k}}}^{{ + }}$, ${{C}}_{{k}{{\sigma }}_{{k}}}^{-}$ 和 ${{C}}_{{k}{{\sigma }}_{{k}}}^{{ + }}$不含相同的文字，${{C}}_{{k}{{\sigma }}_{{k}}}^{-}$不能为空，${{C}}_{{k}{{\sigma }}_{{k}}}^{ + }$可以为空.

2） 对任意${{x}}_{{1}}{,}{{x}}_{{2}}{,}{…}{,}{{x}}_{{m}}\in {\prod }_{{k}{=}{1}}^{{m}}{{C}}_{{k}{{\sigma }}_{{k}}}^{-}$，$x_1, x_2,\cdots, x_m$中至少存在一个互补对文字，称${\bigwedge }_{{k}{=}{1}}^{{m}}{{C}}_{{k}{{\sigma }}_{{k}}}^{-}$为标准矛盾体（S-SC）.

3） ${\vee }_{{k}{=}{1}}^{{m}}{{C}}_{{k}{{\sigma }}_{{k}}}^{{ + }}$=${{C}}_{{{\rm{s}}}{m}{\sigma }}{(}{{C}}_{{1}},C_2,\cdots$,${{C}}_{{m}}{)}$，其中，${\sigma }{=} {\cup}_{{k}{=}{1}}^{{m}}{{\sigma }}_{{k}}$，称${{C}}_{{{\rm{s}}}{m}{\sigma }}({{C}}_{{1}},C_2,\cdots$,${{C}}_{{m}}{)}$为矛盾体分离式（S-CSC）.

根据上述S-CS规则，演绎定义如下：

定义1　矛盾体分离动态演绎^[5]：设一阶逻辑子句集$S=\{C_1,C_2,\cdots,C_m\}$，对于任意的${h}\in \left\{{1,2}{,}\cdots,\bar{{t}}\right\}$（$\bar t$为演绎序列个数），当${{\varPhi}}_{{1}}{,}{{\varPhi}}_{{2}}{,}{\cdots}{,}{{\varPhi}}_{\bar t}$满足下列条件之一，则称${{\varPhi }}_{ {1}} {,}{{\varPhi }}_{ {2}} {,} \cdots {,}{{\varPhi }}_{\bar { {t}}}$为基于标准矛盾体分离的多元动态演绎序列，称该演绎为S-CS演绎：

1）${{\varPhi }}_{ {h}}\in {S}$.

2） 存在 ${ {r}}_{ {1}} {,}{ {r}}_{ {2}} {,} {} \cdots {,}{ {r}}_{{ {l}}_{ {h}}} { < h}$, 有矛盾体分离式${{\varPhi }}_{ {h}} {=} { {C}}_{ {{\mathrm{s}}}{ {r}}_{{ {l}}_{ {h}}}{ {\theta }}_{ {h}}} {(}{{\varPhi }}_{{ {r}}_{ {1}}} {,} {}{{\varPhi }}_{{ {r}}_{ {2}}} {,} \cdots {} {,}{{\varPhi }}_{{ {r}}_{{ {l}}_{ {h}}}})$. 其中，替换 ${ {\theta }}_{ {h}} {=}{ {\cup }}_{ {K=} {1}}^{{ {l}}_{ {h}}}{ {\sigma }}_{ {K}}$,${ {\sigma }}_{ {K}}$为${{\varPhi }}_{{ {r}}_{ {K}}}$的变元替换，${K=} {1} {,} {2} {,\cdots,}{ {l}}_{ {h}}$.

与二元归结演绎形成鲜明对比，S-CS演绎有以下显著的优势：

1） 多元演绎. 多个子句协同参与演绎，通过分离矛盾体删除多个互补对，从而生成含有文字数较少的矛盾体分离式.

2） 可控性. 矛盾体的大小和文字数均可控. 可限制S-CS规则生成的矛盾体分离式所含的文字数，如限制在6个文字以内. 当生成的子句不符合该限制时，将重新构造矛盾体，直到生成的子句满足文字数限制或产生空子句为止.

3） 生成大量单元子句，S-CS规则有生成大量单元子句的能力. 如在矛盾体分离式的文字数不超过6个的限制下，通过实验分析发现，矛盾体分离式为单元子句的占比为90%左右.

3.   子句选择策略

为更好地规划演绎搜索路径并节省计算资源，学者们提出了多种启发式策略^[16-19] ，用于选择合适的子句和文字参与演绎推理. 子句选择策略主要依据不同的评估标准来选择最优子句进行推理，即从不同角度刻画子句特性，描述子句各种属性，根据选择方案确定当前推理过程中的最优子句. 目前，国际主流ATP采用的主要策略包括以下几种类型：

1） 基于字符符号和“序”评估的策略^[7,16]. 如基于重写规则的E中KBO （Knuth-Bendix order） 序方法对等词的有效处理^[16]. 基于人为设定项的权重，KBO序是项重写的基础，可终止等词替换.

2） 分层的子句选取策略. 如 GKC （graph knowledge core）中分层的子句选择策略^[17]. 针对大知识库，GKC使用2层的子句选择方法，多个队列被用于选择子句，并赋予不同的优先级. 如第1层使用项总数排序和子句生成时间排序的队列，第2层使用4个队列.

3） 基于二元归结的Vampire中动态调度策略^[8,18]. Vampire实现了动态调用策略^[18]，给定策略优先级，优先使用最有可能成功的策略，如生成子句的文字数最小策略.

由于上述ATP受推理机制的影响，在搜索空间中保留了大量含有较多文字数的归结式，所以上面的子句选择策略主要是为了避免搜索空间的迅速增长. 相比而言，基于S-CS规则的子句选择策略有明显不同. 针对S-CS规则的策略更倾向于全面的路径搜索，以充分发挥S-CS规则的动态演绎能力.

基于子句的符号特征，提出以下子句选择策略：

1） 子句的文字数：子句中包含的文字数目. 在演绎过程中，包含文字数较少的子句通常有更高的演绎推理效率. 因此，只含一个文字的单元子句必定参与演绎，其次选择文字数较少的非单元子句参与演绎.

2） 子句函数项嵌套层数：子句的函数项嵌套层数越多，所涉及的替换越复杂，因此，选择函数项嵌套层数少的子句参与演绎，同时也控制生成的矛盾体分离式的函数项嵌套层数.

3） 子句的负文字数：子句中包含的负文字数目. 在演绎过程中，包含负文字多的子句通常与结论密切相关，所以优先选择包含负文字多的子句参与演绎推理. 比如，最多只含一个正文字的Horn子句被优先选择. 特别地，优先选择只有负文字的负子句.

4） 矛盾分离式的文字数：S-CSC包含的文字数目. 当矛盾体分离式为空子句时，ATP证明定理成功. 所以应该控制矛盾体分离式的文字数，如少于6个文字. 当矛盾体分离式的文字数不小于6个时，返回上一演绎步骤，重新选择子句构造矛盾体. 将生成的矛盾体分离式加入原始子句集，以构造新的子句集，直到演绎出空子句.

在子句的使用次数方面，提出以下子句选择策略：

1） 子句参与演绎的次数：每当子句参与一次演绎，其计数加 1，重复使用的子句会多次累计. 这一策略有效避免了演绎路径的局部最优和部分子句未参与推理的情况，确保路径搜索的全面性.

2） 重复使用子句策略^[19]：对子句集中的子句进行重复使用，并设置重复使用次数的阈值. 该策略确保充分使用子句的演绎能力，以搜索更多的演绎路径.

4.   PROMETHEE Ⅱ子句评估框架

本文根据S-CS规则的特点，为充分利用其优势，并体现 S-CS 演绎的以下特性：文字的可控性、子句的可重复性、协同性、灵活性、目标导向性，选取以下5种属性进行综合评估：子句的文字数、重复使用子句的次数、子句参与演绎的次数、子句函数项嵌套层数和子句的负文字数.

4.1   属性权重的确定

MCDM方法中，确定属性权重主要有主观赋权法和客观赋权法2种方式. 属性权重对子句的最后排序影响较大，因此，为保证评估的客观性，选择客观赋权法更为合适. 常见的客观赋权方法包括标准离差法^[20]、因子分析法^[21]、熵权法^[22]等. 其中，熵权法因应用广泛、计算和编程实现简单且精度较高而被广泛采用. 熵权法通过属性的离散程度直观地解释权重赋值，易与MCDM方法结合. 因此，本文采用熵权法确定属性权重. 其计算步骤如下：

步骤1　给定1组候选子句${ {S}}_{\rm{C}}=\{{ {C}}_{ {1}}$,${ {C}}_{ {2}} ,\cdots ,$${ {C}}_{ {m}}\}$和1组属性${ {S}}_{\rm{G}}=\{{ {G}}_{ {1}}$,${ {G}}_{ {2}} ,\cdots ,$${ {G}}_{ {M}}\}$（${M}$为属性个数）. 其评价矩阵中的元素${ {c}}_{ {ij}} \text{（} {i=} {1,2} {,} {…} {,m} {;} {j=} {1,2} {,} {…} {, M}\text{）}$是候选子句的各属性值.

步骤2　将各属性的数据分类按式（1）进行归一化处理.

式中：${ {d}}_{ {ij}}$为[0,1]之间的实数.

若属性的属性值越大，对子句的评估表现越好，则该属性为正向属性；反之，为负向属性.

步骤3　根据信息熵的定义，求各属性的熵. 第${j}$个属性的熵值为

式中：${ {e}}_{ {j}} {\geqslant} {0}$；${ {p}}_{ {ij}}={ {d}}_{ {ij}}\bigg/{\displaystyle\sum }_{ {i=} {1}}^{ {m}}{ {d}}_{ {ij}}$；当${ {p}}_{ {ij}} {=} {0}$时，定义${ {p}}_{ {ij}} {\ln}\;{ {p}}_{ {ij}}$=0.

步骤4　传统计算第j个属性的熵权w_j如式（3）所示.

当各熵值${ {e}}_{ {j}}$趋于1且差异微小时，得到的熵权${ {w}}_{ {j}}$却差异很大. 因此，本文采用式（4）所示的改进熵权计算方法^[23]确定属性权重.

式中：${\displaystyle\sum }_{ {j=} {1}}^{ {M}}{ {w}}_{ {j}} {=} {1}$.

4.2   PROMETHEE Ⅱ子句评估方法

步骤1　根据式（4）可得每个属性的熵权${ {w}}_{ {j}}$.

步骤2　计算每对候选子句在各属性下的差异值$\overline{{ {d}}_{ {j}}} {(}{ {C}}_{ {i}} {,}{ {C}}_{\bar { {r}}} {)}$，如式（5）所示. 其中，$\bar { {r}}\in \{{{1} ,2{,\cdots,m} {}}\}$.

式中：${ {g}}_{ {j}} {(}{ {C}}_{ {i}} {)}$和${ {g}}_{ {j}} {(}{ {C}}_{\bar { {r}}} {)}$分别为子句${ {C}}_{ {i}}$和${ {C}}_{\bar { {r}}}$的第${j}$个属性值.

步骤3　选择合适的偏好函数. Brans等^[14]提出6种含参数的偏好函数类型（V-shape、V-shape I、Level、U-shape、Usual 和Gaussian）. 根据评估矩阵的信息，偏好函数选取V-shape，如式（6）所示，其中，参数${q}$为每种属性的最大值. 因为不同的属性，其值域有明显差异，所以，不同的属性对应不同的参数. 本文同时也测试了其他参数以及其他类型的偏好函数，如Usual类型的偏好函数，研究发现式（6）的效果最好. 因此，选择式（6）作为本文的偏好函数.

偏好函数${ {P}}_{ {j}}\left({ {C}}_{ {i}} {,}{ {C}}_{\bar { {r}}}\right)$表示在第${j}$个属性上子句${ {C}}_{ {i}}$优先于${ {C}}_{\bar { {r}}}$的程度，取值范围为 [0,1].

步骤4　定义并计算每一对候选子句的偏好指数，偏好指数${\pi }\left({ {C}}_{ {i}} {,}{ {C}}_{\bar { {r}}}\right)$表示在所有属性上，${ {C}}_{ {i}}$超过${ {C}}_{\bar { {r}}}$的偏好度. 对于任意的$\bar { {r}}、 {i}{,}$ ${\pi }\left({ {C}}_{ {i}} {,}{ {C}}_{\bar { {r}}}\right)$的定义如式（7）所示，取值范围为 [0, 1].

步骤5　定义和计算正负优先流.

正优先流${ {\varphi}}^{ { + }} {(}{ {C}}_{ {i}} {)}$表示${ {C}}_{ {i}}$优于其他候选子句的程度；${ {\varphi }}^{ { + }} {(}{ {C}}_{ {i}} {)}$越大，子句越优. 负优先流${ {\varphi }}^{-} {(}{ {C}}_{ {i}} {)}$表示${ {C}}_{ {i}}$劣于其他候选子句的程度；${ {\varphi }}^{-} {(}{ {C}}_{ {i}} {)}$越小，子句越优. ${ {\varphi }}^{ { + }} {(}{ {C}}_{ {i}} {)}$和${ {\varphi }}^{-} {(}{ {C}}_{ {i}} {)}$取值范围为[0, 1].

步骤6　计算候选子句的净占优流.

净占优流${\varphi } {(}{ {C}}_{ {i}} {)}$表示子句的综合优先值，${\varphi } {(}{ {C}}_{ {i}} {)}$越大，子句越优，${\varphi } {(}{ {C}}_{ {i}} {)}$取值范围为[−1, 1]，如式（10）所示.

步骤7　对候选子句按净占优流的值从大到小进行排序.

基于PROMETHEE Ⅱ方法的候选子句选择框架如图1所示. 本文只对5个属性进行评估，根据图1中的计算流程，得出候选子句的完全排序.

图  1  基于 PROMETHEE Ⅱ的候选子句选择框架

Figure  1.  Framework diagram for candidate clause selection based on PROMETHEE Ⅱ

下载: 全尺寸图片 幻灯片

4.3   PROMETHEE Ⅱ子句评估框架的应用

目前，基于S-CS规则研发了多个自动定理证明器，如MC-SCS （multi-clause synergized contradiction separation） ^[24]和CSE （contradiction separation extension）^[25]等. 其中，CSE从2018年开始一直参加国际竞赛CADE （Conference on Automated Deduction） ^[25]. 为继续提高CSE的性能，本文将MCDM方法应用到CSE 1.5自动定理证明器，记作MCDM_CSE，其流程如图2所示.

图  2  基于 PROMETHEE Ⅱ的 S-CS 算法流程

Figure  2.  Flowchart of S-CS algorithm based on PROMETHEE Ⅱ

下载: 全尺寸图片 幻灯片

将基于MCDM方法的S-CS演绎算法流程中选择的第一个参与矛盾体分离演绎的子句称为起步子句. 根据S-CS演绎时间决定是否使用新的PROMETHEE Ⅱ方法评估子句，如每隔20 s使用PROMETHEE Ⅱ方法评估子句.

基于S-CS规则的PROMETHEE Ⅱ子句评估方法的主要优势如下：1） MCDM方法可组合多种子句属性，评估出当前演绎步骤中的最优子句. 相比优先级子句选择方法，MCDM方法更高效，对子句评估更灵活. 2） 可增加、删减、更换属性.属性的选取非常重要，所选属性的数量会直接影响评价矩阵，从而影响对子句的评估结果. 3） 克服主观因素对权重的影响. 采用熵权法客观确定属性权重，有效避免了人为因素的影响. 针对不同的子句集，其评价矩阵不同，因此相应属性权重也不同. 4） 使用多属性决策方法的次数可动态调整，可控性更强. 随着演绎过程中属性值的动态变化，更新评价矩阵，再动态使用多属性决策方法.

5.   实验及结果分析

本文对2022年国际竞赛CADE 中FOF （First-Order Form） 组的500个定理和TPTP-v8.1.0 （Thousands of Problems for Theorem Provers）^[26]问题库中FOF格式的9091个定理以及最难的定理进行证明. TPTP问题库中每个定理对应一个rating值参数，代表定理的难度等级. 定理的难度等级是[0, 1]中的实数，rating = 0的定理能被所有自动定理证明器证明，rating = 1的定理目前不能被任何自动定理证明器证明. TPTP问题库也对每个定理进行了分类，如SET表示集合论定理，SWV表示软件验证类的定理. 为评估本文多属性决策方法的有效性，该方法被加入到Vampire 4.7^[27]和Eprover （E 2.6）^[28]，自动定理证明器记作MCDM_V 和MCDM_E.

实验硬件环境为3.4 GHz Inter （R） Core （TM） i7-6700处理器，11.1GB内存，操作系统为Ubuntu15.04 64位. 证明每个定理的时间为国际竞赛标准时间300 s. 本文所有的自动定理证明器在相同的测试环境下进行测试. Prover9^[29] 和Otter^[30]均可检查证明过程的正确性，而Prover9自动定理证明器是在Otter自动定理证明器基础上改进的，并一直参与国际竞赛，所以Prover9作为本实验S-CS演绎过程的验证工具.

5.1   MCDM_CSE自动定理证明器能力分析

MCDM_CSE自动定理证明器证明的定理个数为2586个，比CSE 1.5多证明151个. 其中，CSR、GEO、SET、NUM、SEU、SWV、KRS、SWC和SYN这9类定理的证明数量均超过 100 个. 分析实验数据发现，除SYN以外，其他8类定理的证明个数在MCDM_CSE中均超过CSE 1.5，尤其是NUM多证明了38个. 因此，MCDM_CSE比CSE 1.5的性能更好. 特别地，CSR、GEO、SET、NUM、SEU这5类定理证明的个数均不低于200个.

MCDM_CSE和CSE 1.5在不同难度等级下证明的定理数量对比如表1所示. 每个定理的证明时间均在300 s内，MCDM_CSE证明的数量比CSE 1.5多151个. 当rating值不低于0.1时，MCDM_CSE证明的定理数量均超过了CSE 1.5，表明MCDM_CSE的能力优于CSE 1.5.PROMETHEE Ⅱ方法能有效提升CSE 1.5的性能.

表  1  MCDM_CSE和CSE 1.5在不同难度等级下证明的定理数量对比

Table  1.  Comparison of the number of theorems proved by MCDM_CSE and CSE 1.5 at different difficulty levels 个

难度等级	MCDM_CSE	CSE 1.5
[0, 0.10）	1061	1073
[0.10,0.50）	1338	1212
[0.50,0.60）	98	79
[0.60,0.70）	43	39
[0.70,0.80）	22	16
[0.80,0.90）	13	11
[0.90,1.00）	8	5
1.00	3	0

下载: 导出CSV 

| 显示表格

分析结果表明，多属性决策子句评估方法发挥了关键作用. 对于CSE 1.5不能证明的151个定理，多属性决策方法能缩短定理判定的总时间，使得这些定理能在300 s内被MCDM_CSE证明. 在证明定理效率方面，CSE 1.5的平均时间为26.19 s，而MCDM_CSE平均时间为25.24 s. 相比CSE 1.5, MCDM_CSE提高了1540个定理的证明效率.

表2列出6个被MCDM_CSE证明但未被CSE 1.5证明的定理，这些定理的难度等级均大于 0.90，平均证明时间为132.34 s. 这表明 MCDM_CSE 对较难定理的证明具有良好表现. 尤其值得注意的是，其中有 3 个定理的难度等级为 1.00，目前尚无其他 ATP 能证明这些定理.

表  2  MCDM_CSE证明难度大于0.90的定理所需的证明时长

Table  2.  Time consumed by MCDM_CSE to prove theorems with difficulty greater than 0.90

定理名称	难度等级	证明时间/s
SEU413 + 2	0.92	26.81
SWB088 + 1	0.97	137.78
SWB090 + 1	0.97	126.04
NUM736 + 4	1.00	65.49
SYO625-1	1.00	219.51
SYO587 + 1	1.00	218.41

下载: 导出CSV 

| 显示表格

表3为MCDM_CSE已证明的2586个定理在国际知名自动定理证明器中的对比情况. Vampire 自 2002 年起一直是国际自动定理证明器竞赛 （FOF 组） 的冠军，E 多年稳居亚军或季军，而 Prover9 被广泛视为衡量 ATP 能力的基准自动定理证明器. 因此，本文选取这3个证明器作为比较对象. 结果显示，Vampire 4.7有5个定理不能证明， E 2.6有41个定理不能证明， Prover9有293个定理不能证明.

表  3  对已证明定理（按难度等级）在国际知名自动定理证明器中证明数量的比较

Table  3.  Comparison of the number of theorems (by difficulty level) proved by internationally known ATPs 个

自动定理证 明器	难度等级
	[0,0.70）	[0.70,0.80）	[0.80,0.90）	[0.90,1.00]
MCDM_CSE	2540	22	13	11
Vampire 4.7	2539	21	13	8
E 2.6	2532	12	1	0
Prover9	2264	13	8	8

下载: 导出CSV 

| 显示表格

5.2   基于2022年CADE国际竞赛的证明情况

为进一步评估多属性决策方法的有效性，本文测试了2022年CADE竞赛的500个竞赛例，测试的自动定理证明器为MCDM_V、 MCDM_E、Vampire 4.7和E 2.6.

表4为各自动定理证明器在2022年CADE竞赛的比较结果. MCDM_V 证明了462个定理，比Vampire 4.7多6个. MCDM_E证明了387个定理，比E 2.6多7个. 因此，本文的多属性决策评估子句的方法能有效地评估子句，能提高Vampire 4.7和E 2.6的能力. 在效率方面，MCDM_V证明462个定理的平均时间为15.30 s，比Vampire 4.7少0.80 s. MCDM_E证明387个定理的平均时间为27.40 s，比E 2.6少4.30 s. 实验表明，多属性决策评估子句方法能节省子句评估时间.

表  4  2022年CADE竞赛的比较结果

Table  4.  Comparative results on the CADE 2022 competition

自动定理证明器	平均时间/s	证明个数/个
MCDM_V	15.3	462
Vampire 4.7	16.1	456
MCDM_E	27.4	387
E 2.6	31.7	380

下载: 导出CSV 

| 显示表格

图3表示在300 s内每个自动定理证明器证明定理的实验结果，横轴表示证明的定理个数，纵轴表示证明定理所需的CPU时间. 从图3可以看出，在相同时间内（同一水平线），MCDM_E的曲线几乎在E 2.6的右边或与E 2.6重合，MCDM_V的曲线几乎在Vampire 4.7的右边或与Vampire 4.7重合. 并且通过分析实验数据发现，相比E 2.6，MCDM_E提高了证明79个定理的效率；相比Vampire 4.7, MCDM_V提高了28个定理的效率. 因此，多属性决策方法能提高自动定理证明器的能力和效率.

图  3  不同ATP在2022年CADE竞赛的CPU时间比较

Figure  3.  Comparison of CPU time of different ATPs for the CADE 2022 competition

下载: 全尺寸图片 幻灯片

6.   结　论

为削弱主观因素对子句评估的影响，通过充分利用多种子句属性信息对子句进行客观评估，本文提出一种用于动态综合评估子句的多属性决策方法.实验结果表明，本文提出的方法能提高自动定理证明器的性能，主要贡献如下：

1） 本文提出一种新的子句选择方法，结合S-CS规则的特性，应用PROMETHEE Ⅱ方法得到子句的完全排序，从而选择最优的候选子句参与S-CS演绎.

2） 针对PROMETHEE Ⅱ方法中属性权重的确定，采用熵权法（客观赋权法）计算属性权重，避免人为因素造成偏差.

3） 将PROMETHEE Ⅱ方法应用到自动定理证明器CSE 1.5、Vampire 4.7和E 2.6中. 实验表明，该方法有效提高了证明器的性能，尤其在子句的选择方面发挥重要作用，能更精确地评估子句，有利于子句的选择.

4） 针对多个属性值相同的子句，PROMETHEE Ⅱ方法可以进行完全排序，从而选择更适合的子句参与S-CS演绎，有效避免按照优先级对子句进行多次比较.

综上所述，多属性决策子句评估方法均能提高CSE 1.5、Vampire 4.7和E 2.6的性能，但仍有一些不足之处可改进. 如可以按照TPTP库的定理类型进行评估，以及增加对文字的评估.