Loading [MathJax]/jax/output/SVG/jax.js
  • ISSN 0258-2724
  • CN 51-1277/U
  • EI Compendex
  • Scopus 收录
  • 全国中文核心期刊
  • 中国科技论文统计源期刊
  • 中国科学引文数据库来源期刊

钢结构涂层的单轴拉伸试验与本构模型研究

魏亚鹏

曾国艳, 徐扬, 陈树伟, 姜世攀. 基于多属性决策的一阶逻辑子句选择方法[J]. 西南交通大学学报, 2025, 60(1): 185-193. doi: 10.3969/j.issn.0258-2724.20230023
引用本文: 魏亚鹏. 钢结构涂层的单轴拉伸试验与本构模型研究[J]. 西南交通大学学报. doi: 10.3969/j.issn.0258-2724.20230591
ZENG Guoyan, XU Yang, CHEN Shuwei, JIANG Shipan. First-Order Logic Clause Selection Method Based on Multi-criteria Decision Making[J]. Journal of Southwest Jiaotong University, 2025, 60(1): 185-193. doi: 10.3969/j.issn.0258-2724.20230023
Citation: WEI Yapeng. Study on Uniaxial Tensile Test and Constitutive Model of Steel Structure Coating[J]. Journal of Southwest Jiaotong University. doi: 10.3969/j.issn.0258-2724.20230591

钢结构涂层的单轴拉伸试验与本构模型研究

doi: 10.3969/j.issn.0258-2724.20230591
基金项目: 中国铁路设计集团有限公司科技研究计划重大课题(2020YY140601);中国铁路设计集团有限公司科技开发课题(2024A0223801)
详细信息
    作者简介:

    魏亚鹏(1996—),男,工程师,研究方向为钢结构理论及应用,E-mail:weiyapeng@crdc.com

  • 中图分类号: O346

Study on Uniaxial Tensile Test and Constitutive Model of Steel Structure Coating

  • 摘要:

    为研究钢结构桥梁涂装层的力学本构模型,以长效型涂装体系为试验对象对其分别进行单轴拉伸试验,得出面漆、中间漆、底漆和复合涂层的应力-应变曲线;通过无量纲化处理获得长效型涂装体系上升段本构方程的统一表达形式,并针对每种漆膜适用条件给出相应的本构方程. 研究结果表明:1) H06-X环氧富锌底漆(含锌量80%)和长效型复合涂层的应力-应变曲线分为弹塑型阶段、应变强化阶段和破坏阶段;H06-C2环氧厚浆云母氧化铁中间漆的应力-应变曲线分为应变强化阶段和破坏阶段;E01-JY氟碳面漆的应力-应变曲线分为近似线弹性阶段和破坏阶段. 2) 依据应力-应变曲线得出了底漆、中间漆、面漆和复合涂层的弹性模量、泊松比、剪切模量、单轴拉伸强度、拉伸断裂应变等力学性能特征参数;底漆的单轴拉伸强度最强,中间漆次之,面漆最差;面漆的变形性能最佳,中间漆次之,底漆最差.

     

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

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

    根据上述提到的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的性能.

    首先介绍本文涉及的一阶逻辑的相关概念[15].原子公式由谓词符号(如P)和项组成. 其中,变元(如x, y)、常元(如a)和函数符(如f)都是项. 原子公式A及其否定¬A称为文字,称A¬A为互补对. 若干个文字的析取称为子句,只有一个文字的子句称为单元子句. 若干个子句的合集称为子句集. 一个替换是形如{t1/y1,t2/y2,,tN/yN}的有限集合,其中,yJJ=1,2,,N为变量符号,N为变量个数, tJ为不同于yJ的项. 集合中yJ各不相同,称tJ为替换的分子,yJ为替换的分母.

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

    矛盾体分离规则[5]:设一阶逻辑子句集 S={C1,C2,,Cm}m为子句个数),子句 C1C2Cm之间不存在相同变元(若存在不同的子句有相同的变元,则需对变元更名),称由子句集S产生新子句的推理规则为标准矛盾体分离规则,简称S-CS规则.

    对于任意子句Ckk=1,2,,m),存在替换σk可以应用于子句Ckσk可以为空替换),使得Ck中相同的文字可以合并,得到子句Ckσk.Ckσk分为两部分子句(CkσkC+kσk),满足:

    1) Ckσk=CkσkC+kσk, CkσkC+kσk不含相同的文字,Ckσk不能为空,C+kσk可以为空.

    2) 对任意x1,x2,,xmmk=1Ckσkx1,x2,,xm中至少存在一个互补对文字,称mk=1Ckσk为标准矛盾体(S-SC).

    3) mk=1C+kσk=Csmσ(C1,C2,,Cm),其中,σ=mk=1σk,称Csmσ(C1,C2,,Cm)为矛盾体分离式(S-CSC).

    根据上述S-CS规则,演绎定义如下:

    定义1 矛盾体分离动态演绎[5]:设一阶逻辑子句集S={C1,C2,,Cm},对于任意的h{1,2,,ˉt}ˉt为演绎序列个数),当Φ1,Φ2,,Φˉt满足下列条件之一,则称Φ1,Φ2,,Φˉt为基于标准矛盾体分离的多元动态演绎序列,称该演绎为S-CS演绎:

    1)ΦhS.

    2) 存在 r1,r2,,rlh<h, 有矛盾体分离式Φh=Csrlhθh(Φr1,Φr2,,Φrlh). 其中,替换 θh=lhK=1σK,σKΦrK的变元替换,K=1,2,,lh.

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

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

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

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

    为更好地规划演绎搜索路径并节省计算资源,学者们提出了多种启发式策略[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]:对子句集中的子句进行重复使用,并设置重复使用次数的阈值. 该策略确保充分使用子句的演绎能力,以搜索更多的演绎路径.

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

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

    步骤1 给定1组候选子句SC={C1,C2,,Cm}和1组属性SG={G1,G2,,GM}M为属性个数). 其评价矩阵中的元素ciji=1,2,,m;j=1,2,,M是候选子句的各属性值.

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

    dij={cijmincijmaxcijmincij,maxcijcijmaxcijmincij, (1)

    式中:dij为[0,1]之间的实数.

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

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

    ej=1lnmmi=1pijlnpij (2)

    式中:ej0pij=dij/mi=1dij;当pij=0时,定义pijlnpij=0.

    步骤4 传统计算第j个属性的熵权wj如式(3)所示.

    wj=(1ej)/Mj=1(1ej). (3)

    当各熵值ej趋于1且差异微小时,得到的熵权wj却差异很大. 因此,本文采用式(4)所示的改进熵权计算方法[23]确定属性权重.

    wj=1ej+0.1Mj=1(1ej)Mj=1[1ej+0.1Mj=1(1ej)] (4)

    式中:Mj=1wj=1.

    步骤1 根据式(4)可得每个属性的熵权wj.

    步骤2 计算每对候选子句在各属性下的差异值¯dj(Ci,Cˉr),如式(5)所示. 其中,ˉr{1,2,,m}.

    ¯dj(Ci,Cˉr)=gj(Ci)gj(Cˉr) (5)

    式中:gj(Ci)gj(Cˉr)分别为子句CiCˉr的第j个属性值.

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

    Pj(Ci,Cˉr)={0,¯dj(Ci,Cˉr)0,¯dj(Ci,Cˉr)/q,0<¯dj(Ci,Cˉr)q,1,¯dj(Ci,Cˉr)>q. (6)

    偏好函数Pj(Ci,Cˉr)表示在第j个属性上子句Ci优先于Cˉr的程度,取值范围为 [0,1].

    步骤4 定义并计算每一对候选子句的偏好指数,偏好指数π(Ci,Cˉr)表示在所有属性上,Ci超过Cˉr的偏好度. 对于任意的ˉri, π(Ci,Cˉr)的定义如式(7)所示,取值范围为 [0, 1].

    π(Ci,Cˉr)=Mj=1Pj(Ci,Cˉr)wj. (7)

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

    φ+(Ci)=1n1nˉr=1π(Ci,Cˉr), (8)
    φ(Ci)=1n1nˉr=1π(Cˉr,Ci) (9)

    正优先流φ+(Ci)表示Ci优于其他候选子句的程度;φ+(Ci)越大,子句越优. 负优先流φ(Ci)表示Ci劣于其他候选子句的程度;φ(Ci)越小,子句越优. φ+(Ci)φ(Ci)取值范围为[0, 1].

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

    净占优流φ(Ci)表示子句的综合优先值,φ(Ci)越大,子句越优,φ(Ci)取值范围为[−1, 1],如式(10)所示.

    φ(Ci)=φ+(Ci)φ(Ci). (10)

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

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

    图  1  基于 PROMETHEE Ⅱ的候选子句选择框架
    Figure  1.  Framework diagram for candidate clause selection based on 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) 使用多属性决策方法的次数可动态调整,可控性更强. 随着演绎过程中属性值的动态变化,更新评价矩阵,再动态使用多属性决策方法.

    本文对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演绎过程的验证工具.

    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 
    | 显示表格

    为进一步评估多属性决策方法的有效性,本文测试了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

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

    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库的定理类型进行评估,以及增加对文字的评估.

  • 图 1  标准漆膜试件

    Figure 1.  Sample of standard coating film

    图 2  涂层拉伸的应力-应变实测曲线

    Figure 2.  Measured stress–strain curves for coatings in tension

    图 3  长效型涂装体系σmεm对比分析

    Figure 3.  Comparative analysis of σm and εm of long-lasting coating system

    表  1  钢结构桥梁长效型涂装体系组分及配比

    Table  1.   Components and ratios of long-lasting coating system for steel bridge

    对象 A组分 B组分 比例
    底漆 H06-X环氧富锌底漆
    (含锌量80%)
    H06-X固化剂 12.8∶1
    中间漆 H06-C2环氧厚浆云母
    氧化铁中间漆
    H06-C2固化剂 13.5∶1
    面漆 E01-JY氟碳面漆 E01-JY固化剂 10∶1
    下载: 导出CSV

    表  2  涂层力学性能参数

    Table  2.   Mechanical property parameters for coatings

    涂层种类 E/MPa υ G/MPa σm /MPa εm εb
    H06-X底漆 535.7 0.20 223.2 11.0 0.021 0.026
    H06-C2中间漆 71.5 0.06 33.8 5.4 0.075 0.086
    E01-JY面漆 9.9 0.03 4.8 2.5 0.248 0.289
    复合涂层 95.1 0.13 41.9 4.7 0.049 0.062
    下载: 导出CSV
  • [1] KAMANI P K. Corrosion management & coatings[J]. Paintindia, 2016, 1: 100-105.
    [2] 戴润达. 钢桥梁的长效防腐涂装[J]. 涂料工业,2018,48(12): 74-79. doi: 10.12020/j.issn.0253-4312.2018.12.74

    DAI Runda. Research on long-lasting anticorrosive coating of steel bridge[J]. Paint & Coatings Industry, 2018, 48(12): 74-79. doi: 10.12020/j.issn.0253-4312.2018.12.74
    [3] TOUBIA E A, EMAMI S. Experimental evaluation of structural steel coating systems[J]. Journal of Materials in Civil Engineering, 2016, 28(12): 4016147.1-4016147.10.
    [4] 蔺鹏臻,魏亚鹏,乔叶伟. 风沙冲蚀下钢结构涂层的界面应力与破坏准则[J]. 西南交通大学学报,2023,58(1): 236-243. doi: 10.3969/j.issn.0258-2724.20210189

    LIN Pengzhen, WEI Yapeng, QIAO Yewei. Interfacial stress and failure criteria of steel structure coatings under wind-sand erosion[J]. Journal of Southwest Jiaotong University, 2023, 58(1): 236-243. doi: 10.3969/j.issn.0258-2724.20210189
    [5] HIROKAZU M. A multi-step linear approximation method for nonlinear analysis of stress and deformation of coated plain-weave fabric[J]. Journal of Textile Engineering, 2006, 52(5): 189-195. doi: 10.4188/jte.52.189
    [6] BOGNER B H. The mechanical behaviour of coated fabrics used in prestressing textile engineering structures: theory, simulation and numerical analysis to be used in a fem-model[J]. Journal of the International Association for Shell and Spatial Structures, 2008, 49(1): 39-47.
    [7] 许荔,江晓禹,钱林茂. 树脂基纳米涂层复合材料力学性能试验研究[J]. 西南交通大学学报,2005,40(3): 347-350. doi: 10.3969/j.issn.0258-2724.2005.03.014

    XU Li, JIANG Xiaoyu, QIAN Linmao. Experimental study on mechanical properties of resin matrix nano-coating composites[J]. Journal of Southwest Jiaotong University, 2005, 40(3): 347-350. doi: 10.3969/j.issn.0258-2724.2005.03.014
    [8] 陈辉,苟国庆,刘艳,等. 等离子喷涂WC-17Co纳米涂层形成及强韧化机理[J]. 西南交通大学学报,2008,43(5): 633-637. doi: 10.3969/j.issn.0258-2724.2008.05.015
    [9] CHEN Hui, GOU Guoqing, LIU Yan, et al. Formation and strengthening mechanisms of plasma sprayed nanostructured WC-Co coating[J]. Journal of Southwest Jiaotong University, 2008, 43(5): 633-637.
    [10] 易洪雷,丁辛,陈守辉. PES/PVC膜材料拉伸性能的各向异性及破坏准则[J]. 复合材料学报,2005,22(6): 98-102. doi: 10.3321/j.issn:1000-3851.2005.06.017

    YI Honglei, DING Xin, CHEN Shouhui. Orthotropic behavior and strength criterion of pes/pvc membrane materials under tensile loading[J]. Acta Materiae Compositae Sinica, 2005, 22(6): 98-102. doi: 10.3321/j.issn:1000-3851.2005.06.017
    [11] 刘平,吴刚,唐柏鉴,等. PVDF涂层织物拉伸力学性能试验研究[J]. 东南大学学报(自然科学版),2017,47(6): 1195-1200.

    LIU Ping, WU Gang, TANG Baijian, et al. Experimental study on mechanical properties of PVDF textile[J]. Journal of Southeast University (Natural Science Edition), 2017, 47(6): 1195-1200.
    [12] 于沁灵,龚景海,郭晓,等. 涂层织物类膜材的拉伸试验及力学参数研究[J]. 空间结构,2020,26(4): 64-69.

    YU Qinling, GONG Jinghai, GUO Xiao, et al. Tensile test and mechanical parameters of coated fabric membrane[J]. Spatial Structures, 2020, 26(4): 64-69.
    [13] 王利钢,陈务军,高成军. 聚酯纤维机织物-聚氯乙烯-聚偏氟乙烯膜材双轴剪切力学性能试验[J]. 复合材料学报,2015,32(4): 1118-1124.

    WANG Ligang, CHEN Wujun, GAO Chengjun. Test on biaxial shear mechanical performance of polyester fabric-polyvinyl chloride-polyvinylidene fluoride membrane[J]. Acta Materiae Compositae Sinica, 2015, 32(4): 1118-1124.
    [14] 李阳. 建筑膜材料和膜结构的力学性能研究与应用[D]. 上海:同济大学,2007.

    LI Yang. Study and Applications on Mechanical Properties of Membrane Materials and Structures[D]. Shanghai: Tongji University, 2007.
    [15] 许珊珊,张营营,徐俊豪,等. PVC涂层织物膜材的非线性各向异性本构关系模型[J]. 建筑材料学报,2020,23(5): 1098-1103. doi: 10.3969/j.issn.1007-9629.2020.05.015

    XU Shanshan, ZHANG Yingying, XU Junhao, et al. Nonlinear anisotropic constitutive model of PVC coated fabric membrane[J]. Journal of Building Materials, 2020, 23(5): 1098-1103. doi: 10.3969/j.issn.1007-9629.2020.05.015
    [16] 张营营,徐俊豪,曹原,等. PTFE膜材料的偏轴拉伸性能及破坏机理[J]. 哈尔滨工业大学学报,2016,48(12): 135-141,164.

    ZHANG Yingying, XU Junhao, CAO Yuan, et al. Off-axial tensile behaviors and failure mechanisms of PTFE coated fabrics[J]. Journal of Harbin Institute of Technology, 2016, 48(12): 135-141,164.
    [17] European Committee for Standardization. Plastics determination of Tensile Properties: ISO 527 -3-2018[S]. Belgium Brusse: European Committee for Standardization, 2018.
    [18] 何平笙. 高聚物的力学性能[M]. 第3版. 合肥:中国科学技术大学出版社,2021:218.
    [19] 束德林. 工程材料力学性能[M]. 第3版. 北京:机械工业出版社,2016:192-195.
  • 加载中
图(3) / 表(2)
计量
  • 文章访问数:  40
  • HTML全文浏览量:  16
  • PDF下载量:  9
  • 被引次数: 0
出版历程
  • 收稿日期:  2023-11-07
  • 修回日期:  2024-03-22
  • 网络出版日期:  2025-02-18

目录

/

返回文章
返回