基于高阶逻辑的定理证明方法及其对策的应用

康 漫 张 杰 李晓娟 关 永

1(北京化工大学信息科学与技术学院 北京 100029) 2(首都师范大学信息工程学院 北京 100048)

基于高阶逻辑的定理证明方法及其对策的应用

康 漫1张 杰1李晓娟2关 永2

1(北京化工大学信息科学与技术学院 北京 100029)2(首都师范大学信息工程学院 北京 100048)

定理证明是形式化验证的主要方法之一，其中定理证明器的使用是难点。为了提高证明效率，论述HOL4系统中主要的三种证明方法：支持高级证明步骤。自动推理和化简器，为定理的证明提供了一个完整而通用的理论框架。详细说明了以上三种证明方法的相关对策的功能和应用环境，并为应用中可能出现的问题提出解决方案。给出的对策应用实例不仅体现了三种方法中相关对策的实用性，还进一步表明了提出解决方案的有效性。

定理证明方法 形式化验证 定理证明器 证明方法 对策

0 引 言

形式化方法是保证计算机系统设计正确性的一条重要途径。它是用数学的方法表达设计的系统的实现及其规范或性质，根据数学理论来证明所设计的系统实现满足其规范或性质。

形式化验证主要包括等价性检验、模型检测和定理证明。这三种方法各有优缺点。等价性检验主要是检验设计变换前后的一致性，但是不能进行规范和性质的验证。模型检测的优点是完全自动化，如果系统不满足给定的性质，检验结果可以给出反例，但是模型检测存在状态组合爆炸问题。定理证明的方法是用某种逻辑的形式化系统的公式表示所验证的系统及其性质，以该形式化系统的公理和推理规则为基础，可以逐步推导出表达系统性质的公式。定理证明能够处理无限状态的系统，但是这种验证方法的代价较高，需要较高的数学能力并要经过相当时间的训练。因此，定理证明器的使用对定理证明方法的应用和发展起着至关重要的作用。

Higher Order Logic(HOL) 系统是最成熟的用于验证的定理证明器之一。它是由英国剑桥大学的M.J.C.Gordon教授等在80年代开发的一种形式化验证系统，其最新的版本为HOL4。近年来，它已被广泛应用于数学定理的证明、软件验证、协议验证和程序验证[1-4]。

关于定理证明器HOL4系统的理论和对策，有相关的文献介绍[5-8]，但是这些文献的介绍只适合于用于理解HOL4系统，并不能为用户提供证明的思路。Slind等对HOL4系统的逻辑，理论和对策等进行了总的概述。作者在文中指出了用HOL4进行证明的通用的方法：支持高级证明的步骤、化简器和一阶搜索[9]，但是作者并没有进行进一步的阐述和说明。文献[10]对Slind等指出的化简器中重写对策的应用进行了详细的说明，但是并没有完成HOL4系统常用证明方法的阐述。为了能更好更快地完成定理的证明，本文提供了通用的，完整的证明方法，说明了其相关对策的功能和使用环境，并对其应用中出现的问题提出了解决方案。通过给出的常用对策的应用实例，不仅体现了三种方法的实用性，而且进一步表明了提出解决方案的有效性。

1 证明方法与对策

HOL4系统是一种交互式定理证明系统。所谓交互式定理证明系统，是指在高层由人做引导工作，在底层由机器自动化地处理一部分定理推导与证明问题[9]。在HOL4系统中完成定理证明的基本方法有两种，即正向证明法和目标制导法。正向证明方法是从要证明定理的假设条件出发，利用系统中的公理、定理和推理规则等逐步推导出欲证定理。目标制导证明法首先假设欲证明的定理为真，并将其作为初始目标，再通过使用对策引导系统根据已知条件、公理、定义和定理产生简化的子目标。反复使用对策对子目标进行不断地化简，直到当前子目标可以利用某个对策直接证明为止[11]。由于正向证明方法不能快速而有效地完成证明，所以在HOL4系统中，通常使用的证明方法是目标制导法。

目标制导法当中，仍然需要人工的选择相应的证明对策，在HOL4系统中有大量的对策，在这个拥有庞大数量对策的系统中，如何快速准确地找到合适的对策，是用户完成证明的关键[12]，也是证明的难点。如果用户采用熟悉大量的对策，然后再选择对策进行证明的方法，将会浪费大量的时间和精力。这种证明途径是不科学的、盲目的。为此本文给出的高效可行的证明途径是先确定证明方法，然后选择其对应的对策完成证明。HOL4系统中证明的方法有高级证明、简化器、一阶证明等。经过作者的大量实践，针对目标制导法，本文指出HOL4中的高级证明和简化器是非常有效的证明方法。

由于高级证明包括支持高级证明的步骤和自动推理，所以支持高级证明的步骤、自动推理和简化器是本文介绍的三种证明方法。此三种证明方法从理论上为定理的证明提供了一个完整的框架。此理论框架如图1所示。

在该理论框架中，对于任何需要证明的初始目标，支持高级证明的步骤能够利用HOL4的潜在功能搜索目标中变量在定义数据类型时已经证明的定理或规则，供用户使用，大大减轻了用户证明的负担。其中使用支持高级证明步骤中的归纳方法证明递归法定义的数据类型、函数和谓词是非常有效的。因为在函数性语言中程序的重复都是使用递归方法来完成，所以归纳法对于定理证明尤为重要。通过一次或多次使用支持高级证明的步骤得到的子目标是初始目标分解之后的结果，此时的子目标的形式非常接近系统中已有的理论，便可以采用自动推理和简化器进行证明。自动推理可以用来证明演绎推理中已知条件、公理、定义和定理与证明目标之间的蕴含关系。自动推理是HOL4系统中必不可少的一种方法，它可以完成多次蕴含关系的证明，这是其他对策所不具备的。简化器用来证明演绎推理中已知条件、公理、定义和定理与证明目标之间的等价关系。简化器是HOL4系统中是极为重要的一种证明方法，这是因为目标制导法的证明思想与简化器的证明思路是一致的，都是利用已知条件和系统中已有的公理、定义、定理等完成证明目标的化简与证明。

该理论框架为定理的证明提供了一个通用的方法，也为用户完成证明提供了基本的证明思路，提高了证明效率。然而证明方法的应用离不开对策。HOL4系统中的对策是ML函数，主要实现以下三种功能：一是将要证明的目标分解为子目标，二是将要证明的目标进行化简，三是对当前目标进行证明。下面围绕本文提出的理论框架中的三种证明方法及其相应的对策进行详细的说明和分析。

2 支持高级证明步骤及其对策的应用

HOL4中证明的观点是由用户在高层指导，自动推理完成辅助证明。因此，HOL4系统提供了一个类型索引定理的数据库(包含情况分析、归纳等)，结合一些陈述证明结构，用户在高层可以执行很多证明[9]。HOL4系统为用户提供了许多支持高级证明步骤的对策，比如Induct、Cases、Cases_on、Induct_on等，这些对策都可以使用数据库中的信息减轻HOL的应用负担[5]。

当一个数据类型被成功定义的时候，关于这个新类型的一些标准定理被自动证明，并被添加到一个数据库TypeBase中。这些支持高级证明步骤的对策有一个共同的特点，它们都可以在数据库TypeBase中搜索数据类型，如果搜索到相应的数据类型，就会返回这个类型已有的重写规则，以及相关事实定理。用户通过返回的定理进行情况分析或者归纳，支持下一步的证明。在一些情况下，该类对策的使用将直接决定着证明的成功与失败。

支持高级证明步骤的对策中有一类很重要的对策——归纳对策，它可以有效地处理递归定义的数据型和函数。HOL4系统的元语言是ML语言，ML语言是函数性语言，函数性语言程序的重复主要靠函数的递归[11]，在这种情况下使用归纳法进行证明就方便很多。因此，归纳证明方法在HOL4证明系统中是非常重要的一种证明方法。HOL4系统提供了几种使用归纳法进行证明的途径，对于自然数和表等这些系统内部理论，具有专用的对策进行归纳[11]，而Induct_on对策是归纳证明中最常用的对策，它可以完成自然数和表的专用归纳对策的功能。

作者在大量的实践中发现，利用高级证明步骤中的对策进行证明，最常用的就是Cases_on和Induct_on这两个对策，使用这两个对策有两个关键所在：一是如何选择恰当的对策。对策选择的恰当与否直接影响到后续证明步骤的繁琐与简单，甚至影响证明的结果。二是如何选择这些对策作用的参数。参数选取的合适，将会简化证明步骤，如果选择的不合适将有可能影响证明结果。

下面围绕这两个典型的对策进行详细的分析和描述，并给出它们在应用过程中可能出现的问题和解决方法。

(1) Cases_on对策

Cases_on是最常用的一种证明对策，其类型为term -> tactic[6]，所以在应用该对策时要提供一个项作为参数。该对策基于项的类型ty，使用TypeBase数据库中类型ty的情况定理，对证明目标进行情况分解。

通常情况下，Cases_on的参数可以是变量。对于一个既定的证明目标，如果对目标不能再进行化简，HOL4理论库中已经存在的定理能够对情况分解之后的子目标进行证明，可以使用该对策完成目标的情况分解。

例如现有一个证明目标：“对于任意的两个自然数m与n，如果m整除n，那么m≤n，或者n=0”。系统要想对其进行形式化证明，HOL4系统中已存在divides的定义divides_def ： `a dividesb=?x.b=a*x`，所以可以考虑使用重写对策进行化简。化简得到的子目标中含有项 (m*x)，而在HOL4系统中不存在关于这种形式的项的可用的定理，已存在定理MULT_CLAUSES:|-!m n.(0*m=0)∧(m*0=0)∧(1*m=m)∧(m*1=m)∧(SUCm*n=m*n+n)∧(m*SUCn=m+m*n): thm，定理中含有(m*0)和(m*SUCn)形式的项，所以，我们可以对x施加情况分解对策Cases_on，得到的子目标的基本项与定理MULT_CLAUSES中项的形式相同，我们可以使用重写对策进行下一步的证明[7]。如图2所示。

图2 Cases_on对策参数为变量的例子

由此可见，使用Cases_on对策对证明目标进行情况分解，系统会根据要分解变量的数据类型，将目标分解为两个子目标，以便使用系统中已存在的定理进行自动证明。因此使用该对策要求用户对证明目标中含有的变量的数据类型非常了解。

Cases_on的参数也可以是非变量，对于要证明的目标，如果需要分情况讨论才能证明，则也可以通过使用Cases_on对策对目标进行分情况证明。用项来表示非变量的参数，该对策可以将目标分解为项成立和否定项的情况。通常情况下，目标在不同情况下，使用不同的定理完成证明，用户使用该对策分情况分解目标。

例如现有一个证明目标:“对任意的一个表l，取表l的前m个元素再取前n个元素得到的表，与取表l的前MIN(m,n)个元素得到的表一样”。在HOL4系统中已存在的定理LENGTH_TAKE: |- !n l. n <= LENGTH l ==> (LENGTH (TAKE n l) = n) : thm和TAKE_LENGTH_TOO_LONG:|- !l n. LENGTH l <= n ==> (TAKE n l = l) : thm，从这两个定理中可以看出，需要将目标分成`n <= LENGTH l`和`LENGTH l <= n`两种情况证明，此时可以使用Cases_on对策，将目标分成两种情况的子目标，然后使用已有的定理证明目标。如图3所示。

图3 Cases_on对策参数为非变量的例子

由此可见，使用Cases_on对策对证明目标进行情况分解，系统根据项`m<=LENGTH l`，将目标分解为`m<=LENGTH l`和`～(m<=LENGTH l)`两种情况下的子目标。这样，用户可以利用系统中已有的定理完成证明。

然而，当定义的数据类型在Typebase中没有情况定理时，使用Caese_on会失败，也就是说并不适用于所有情况。如果库中现有的定理不能完成证明，使用Caese_on不仅不能有效地支持证明，还会浪费很多时间。因此，使用该对策用户还需要对HOL4中的理论库有一定的了解。

(2) Induct_on对策

Induct_on对策也是支持高级证明步骤中最常用的对策之一，它的类型是term -> tactic[6]，所以在应用该对策时要提供一个项作为参数。该对策是基于项的类型ty，使用TypeBase数据库中类型ty的归纳定理进行归纳证明。

通常情况下，Induct_on的参数可以是变量也可以是非变量，对于一个既定的证明目标，如果不能再对目标进行简化，可以依据目标存在的数据类型定义时的归纳定理进行归纳证明。

如果证明的目标为“对任意的一个表l，表l的长度小于等于n，那么取表l的前n个元素得到的是表l本身”。由于HOL4系统中表是递归定义的，对于表的定义及相关定理通常将表表示为[]或(h::t)的形式，所以对当前目标不存在已有的定理可以将其直接化简。在HOL4系统中已存在的定义: TAKE_def: |- (!n. TAKE n [] = []) / !n x xs. TAKE n (x::xs) = if n = 0 then [] else x::TAKE (n - 1) xs : thm。此时可以使用Induct_on对策，将目标中的表l分解成[]和(h::t)形式的子目标。对于表为[]的子目标，可以使用重写对策直接证明。对于表为(h::t)的子目标，可以使用重写对策将其化简，证明目标。如图4所示。

图4 使用对策Induct_on的例子

多数情况下，对于相同的目标，如果将Cases_on对策和Induct_on对策同时作用于这个目标，且对策的参数相同，这时产生的子目标个数是一样的，如使用Induct_on对策的图4和使用Cases_on对策的图5的两个例子所示。在使用Induct_on对策的图4中产生的第2个子目标中假设条件表中会存一个假设，这将使证明目标的速度快于使用Cases_on对策的情况。

图5 使用对策Cases_on的例子

支持高级证明步骤能够从证明目标的变量或项中，返回其类型定义时存储的定理，从而减轻用户证明的负担。支持高级证明步骤中的对策除了可以返回情况定理和归纳定理，还可以返回重写规则，这时还需要用户考虑使用type_rws对策，这里不再做详细介绍。

3 自动推理

高级证明中除了支持高级证明步骤，还有一种必不可少的证明方法——自动推理。当假设条件，公理，定义和定理与证明目标存在蕴含关系时，使用自动推理中的对策非常有效，另外自动推理还能够很好地处理多层蕴含关系。下面介绍自动推理中最常用的对策PROVE_TAC对策。

PROVE_TAC对策的类型是：thm list -> tactic[9]，所以在应用该对策时要提供一个定理表作为参数。该定理表中包含推导目标所需的公理、定义及定理，系统将根据假设和提供的定理使用一阶推理推导证明目标。

通常情况下，对于一个既定的证明目标，若已有的假设条件和定理能够推导出目标，则可以通过使用PROVE_TAC对策证明目标。

如果存在图6中的目标” TAKE n l = TAKE m l”，从假设条件”n <= m”和” ～(n < m) ”，我们可以使用HOL4理论库中已经存在的定理NOT_LESS: [] |- !m n. ～(m < n) <=> n <= m : thm和LESS_EQUAL_ANTISYM: [] |- !n m. n <= m∧m <= n ==> (n = m) : thm，推导出”m=n”。此时，使用PROVE_TAC对策可以推导出”m=n”，从而，证明目标。

图6 使用对策PROVE_TAC的例子执行

PROVE_TAC对策的结果只有两种情况，证明成功或者证明失败。当系统根据已有的假设和给定的定理或公理进行推导，超出系统设置的搜索深度时，仍没有证明目标，则应用该对策失败。PROVE_TAC对策定理表的构建可以参考已有文献[10]。其实自动推理还包含其他的对策，比如:METIS_TAC能够自动实例化存在量词，DECIDE_TAC对策可以对线性代数的证明应用一个决策程序，这里不再做详细介绍。

4 化简器及其重写对策的应用

化简器的一般作用是通过替换来化简目标，就是将目标等式左边的项与使用的定理的左边的项相匹配，然后用定理等式右边的项替换目标等式右边的项，从而化简目标。重写对策在HOL4中就属于化简器一类。重写是化简对策中的核心操作，在HOL4中是极为重要的一类对策。重写对策可以利用对策中指定的定理重写证明目标，即将HOL4系统中已有的公理、定义和定理与目标中的表达式匹配，如果表达式与等式左边式子的模式相同，则用等式右边的式子替换该表达式，从而对证明目标进行化简或证明[10]。下面介绍使用重写对策的原则、使用问题及解决方法。

SRW_TAC与RW_TAC类似，是一种功能很强大的重写对策，其类型为ssfrag list -> thm list -> tactic[6]。该对策是对一个潜在的化简集工作，通过函数srw_ss进入该化简集，可以添加“化简集片段”和定理而增大化简集。化简集是一个特定的集合，其中包含了一些特定领域的重写定理。在系统中存储许多类型的情况下，RW_TAC的功能就足够了，这是因为在证明目标之前，它可以为已知的类型重复地添加所有的重写定理到一个化简集当中。但是SRW_TAC只需要加载一次重写到srw_ss()下的化简集，在这种情况下，SRW_TAC速度更快。

SRW_TAC对策可以根据潜在的化简集以及给定的化简集片段和给定的公理、定义、定理等对证明目标及假设条件表进行重写，且能自动处理证明目标结论中的全称量词、合取符、析取符、蕴含符，甚至是假设条件表中的存在量词等。另外该对策还具备自动执行案例分解、决策程序等更加高级的功能。

通常情况下，SRW_TAC功能强大，利用它可以快速完成许多证明目标的化简或证明工作。

如图7中，目标为“!h n. LENGTH (h::l) <= n ==> (TAKE n (h::l) = h::l)”，使用重写对策便可将目标化简为假设条件表和定理中已成立的情况，完成对目标的证明。

图7 使用对策SRW_TAC的例子

重写对策虽然能够化简目标，但作者在实践过程中发现，重写对策在带有条件的重写中很容易失效。HOL4系统本身能够进行条件重写，当遇到带有条件的定理时，化简器会泄放假设条件，并将条件假设为真，然后再进行目标的重写。尽管条件重写功能很强大，但并不适合于所有的带有条件的定理。在HOL4系统中只有少数通用的条件可以直接使用条件重写，比如除数不能为0。但是对于大多数用户定义的条件，HOL4系统中的重写对策便不能处理。在这种情况下，如果还需要继续使用重写规则，则需要补充假设条件表，这样才可以完成证明。

通常情况下，当要补充的假设条件存在于HOL4已证明的定理中，可以将已证明的定理直接添加到假设条件表，这时候使用STRIP_ASSUME_TAC对策；当补充的假设条件不存在于HOL4已证明的定理中，我们可以使用by对策。

STRIP_ASSUME_TAC的类型是thm_tactic[6]，该对策将一个定理分解为一个定理表，并添加它们到假设条件。

如对于图8中的证明目标:“取一个表l的前m个元素，得到一个新表，再取新表的前n个元素，与取表l的前(MIN n m)个元素得到的表一样”，已经存在两个假设条件` m <= LENGTH l ` 和 `～(n <= m)`，为了后面证明的需要，我们需要添加定理LENGTH_TAKE: |-!n l. n <= LENGTH l ==> (LENGTH (TAKE n l) = n) : thm，此时可以直接使用STRIP_ASSUME_TAC对策添加。

图8 使用对策STRIP_ASSUME_TAC的例子

by的类型是term quotation * tactic -> tactic[6]，该对策有两个参数，一个是项，表示在假设条件表中要添加的定理，一个是对策，该对策用来证明添加的定理是正确的。by对策的功能是证明一个定理，并将其添加到目标的假设条件列表。

对于图9中的例子，证明的目标是“TAKE n (TAKE m l) = TAKE (MIN n m) l”，从假设条件表我们可以推导出” (LENGTH(TAKE m l))<=n”，将” (LENGTH(TAKE m l))<=n”添加到假设条件表，有助于我们使用HOL4理论库中已有的定理证明目标。但是如何将” (LENGTH(TAKE m l))<=n”添加到假设条件列表，我们可以使用by对策。这时将” (LENGTH(TAKE m l))<=n”设为by的第一个参数，作为要添加的假设，使用对策PROVE_TAC和定理LENGTH_TAKE:[] |- !n l. n <= LENGTH l ==> (LENGTH (TAKE n l) = n) : thm来证明要添加的假设。添加完假设条件，使用重写对策，即可证明目标。

图9 使用对策by的例子

化简器中的重写对策主要的功能是对目标进行化简，当化简的目标与系统中已存在的定理一样时，重写对策也可以直接证明目标。重写对策定理表的构建可以参考已有文献[10]。HOL4系统中还有更多的重写对策，如REWRITE_TAC, ASM_REWRITE_TAC和ONCE_ASM_REWRITE_TAC等，关于它们的使用可以参考重写对策的应用的文献[10]。化简器中还存在一类以SIMP_CONV转换为中心的化简对策，有兴趣的读者可以自行查阅。

5 结 语

HOL4系统中提供了数百个对策及几千个定理，对于HOL4的使用者来说，选择合适的对策证明目标，不是一件容易的事情。本文通过讨论支持高级证明步骤、自动推理和化简器的三种证明方法，以及分析三种证明方法相对应的对策的功能、应用环境和应用中可能出现的问题，以期对HOL4系统用户进行定理证明提供有效的帮助和启发。另外，在HOL4系统中进行形式化验证的方法有很多，本文提出的方法是用户最易接受和使用的方法，并从理论上给出了一个完整的证明框架。因此，本文提供的证明思想和方法，对其他的基于高阶逻辑的定理证明器(例如HOL light、PVS等)同样适用。

[1] Zhang J,Mao D W,Guan Y.Formalization of linear space theory in the higher-order logic proving system[J].Journal of Applied Mathematics,2013,2013(1):66-71.

[2] 钱振江,黄皓,宋方敏.操作系统形式化设计与安全需求的一致性验证研究[J].计算机学报,2014,37(5):1083-1099.

[3] Basin D,Capkun S,Schaller P,et al.Formal Reasoning about Physical Properties of Security Protocols[J].Acm Transactions on Information & System Security,2011,14(2):1-28.

[4] Wang A,Fei H,Gu M,et al.Verifying Java Programs By Theorem Prover HOL[C]//International Computer Software & Applications Conference.IEEE Computer Society,2006:139-142.

[5] Cambridge Research Center of SRI International.The HOL system DESCRIPTION(For HOL Kananaskis-10)[EB/OL].[2014-11-10].http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananask-10-description.pdf/download.

[6] Cambridge Research Center of SRI International.The HOL system REFERENCE(For HOL Kananskis-10)[EB/OL].[2014-11-10].http://sourceforge. net/projects/hol/files/hol/kananaskis-10/kananaskis-10-reference.pdf/download.

[7] Cambridge Research Center of SRI International.The HOL system TUTORIAL(For HOL Kananaskis-10)[EB/OL].[2014-11-10].http://sourceforge. net/projects/hol/files/hol/kananaskis-10/ kananask is-10-tutorial.pdf/download.

[8] Cambridge Research Center of SRI International.The HOL system LOGIC(For HOL Kananaskis-10)[EB/OL].[2014-11-10].http://sourceforge. net/projects/hol/files/hol/kananaskis-10/ kananask is-10-logic.pdf/download.

[9] Slind K,Norrish M.A Brief Overview of HOL4[C]//Theorem Proving in Higher Order Logics,International Conference,Tphols 2008,Montreal,Canada, August 18-21,2008.Proceedings.DBLP,2008:28-32.

[10] 张杰,毛丹雯,关永,等.重写对策在基于HOL的形式化证明中的应用[J].计算机工程与设计,2013,34(10):3664-3668.

[11] 韩俊刚,杜慧敏.数字硬件的形式化验证[M].北京:北京大学出版社,2001:3-9.

[12] 李兵.交互式并行定理证明环境的构建[D].甘肃省兰州市:兰州大学,2006:1-54.

THEOREMPROVINGMETHODBASEDONHIGHERORDERLOGICANDITSAPPLICATION

Kang Man1Zhang Jie1Li Xiaojuan2Guan Yong2

1(CollegeofInformationScienceandTechnology,BeijingUniversityofChemicalTechnology,Beijing100029,China)2(CollegeofInformationEngineering,CapitalNormalUniversity,Beijing100048,China)

The use of theorem proving system is always a difficult point in theorem proving method, and the theorem proving is one of the main methods of formal verification. In order to improve the efficiency of proof, three main methods of proof in HOL4 system are discussed: support for high-level proof steps, automated reasoning and simplification. This paper provided a complete and general theoretical framework for proving theorems. The function and application environment of the commonly used tactics in above methods were analyzed in detail. We proposed solutions to the problems in applications. The application of the proposed strategy not only reflects the practicability of the relative measures in the three methods, but also shows the effectiveness of the proposed solution.

Theorem proving method Formal verification Theorem proving system Proof method Strategy

2017-01-16。国家自然科学基金项目(61572331,61373034)。康漫，硕士生，主研领域：形式化验证。张杰，副教授。李晓娟，教授。关永，教授。

TP301.2

A

10.3969/j.issn.1000-386x.2017.11.002