Application of Multi-Clause Synergized Deduction in First-Order Logic Automated Theorem Proving

CAO Feng; XU Yang; CHEN Shuwei; WU Guanfeng; CHANG Wenjing

doi:10.3969/j.issn.0258-2724.20180800

Volume 55 Issue 2

Mar. 2020

Turn off MathJax

Article Contents

Abstract

References

Journal of Southwest Jiaotong University > 2020 > 55(2): 401-408, 427.

ZHAO Shanpeng, ZHANG Yongfeng, ZHANG Youpeng, WANG Sihua. Mechanical Characteristics of Low-Wind-Pressure Catenary Positive Feeder in Gale Area of Lanzhou‒Urumuqi High-Speed Railway[J]. Journal of Southwest Jiaotong University, 2023, 58(5): 1154-1161. doi: 10.3969/j.issn.0258-2724.20220437

Citation:

CAO Feng, XU Yang, CHEN Shuwei, WU Guanfeng, CHANG Wenjing. Application of Multi-Clause Synergized Deduction in First-Order Logic Automated Theorem Proving[J]. Journal of Southwest Jiaotong University, 2020, 55(2): 401-408, 427. doi: 10.3969/j.issn.0258-2724.20180800

Citation:

PDF( 708 KB)

Application of Multi-Clause Synergized Deduction in First-Order Logic Automated Theorem Proving

doi: 10.3969/j.issn.0258-2724.20180800

CAO Feng^{1,2
,},
XU Yang^2,3,
CHEN Shuwei^2,3,
WU Guanfeng^{2,3
,
,},
CHANG Wenjing^1,2

Received Date: 11 Sep 2018
Rev Recd Date: 01 Apr 2019

Available Online: 30 May 2019

Publish Date: 01 Apr 2020

Abstract

Abstract

First-order logic is an important branch in mathematical logic, and automated reasoning of its logical formula is one of the important research hotspots in the field of artificial intelligence. Most of the state of the art first-order logic automated theorem proving systems adopt binary resolution method. There are only two clauses involved, and therefore only a complementary pair of literals are eliminated during each resolution step. As a consequence, the resulted clause has many literals, which affects the deduction efficiency. In this paper, a multi-clause synergized deduction algorithm is proposed based on contradiction separation rule. This algorithm allows multiple clauses used in deduction, and is able to eliminate more than one complementary pairs. The clause of contradiction separation is controllable and usually has less literals, which can effectively improve the inference ability. This multi-clause synergized algorithm adjusts the deduction order of clauses according to two kinds of weights, effective deduction weight and ineffective deduction weight. Backtracking mechanism is used to search for an optimal path, and effectively plan the deduction path. The algorithm is applied to the international top prover－Eprover 2.1, and Conference on Automated Deduction 2017 competition theorems (FOF division) are set as the test object. Eprover 2.1 with multi-clause synergized deduction algorithm outperformed Eprover 2.1 and solved 8 theorems more than Eprover 2.1. It also solved 31 theorems out of the 110 theorems unsolved by Eprover 2.1, accounting for 28.2% of the total.
- mathematical logic,
- artificial intelligence,
- theorem proving,
- binary resolution,
- contradiction separation rule

FullText(HTML)

兰新高铁地处中国西北地区，东起兰州，西至乌鲁木齐，全长1776 km，是世界上第一条一次性建成运营里程最长的高速铁路. 线路穿越我国新疆地区的百里、三十里等四大风区，风区内常年盛行七八级大风，曾发生过列车被大风吹翻的重大铁路安全事故^[1]. 为保证列车安全顺利地通过风区，铁路建设部门在风区线路轨旁修建了高度为3.5～4.0 m的挡风墙. 但挡风墙“防车不防网”，气流经过挡风墙之后出现了明显的加速效应，使得正馈线发生剧烈舞动，导致线间放电、金具磨损加剧、线索疲劳断股，危及行车安全. 由于铁路运输对安全性要求很高，能够采用的防舞措施有限，低风压正馈线不改变接触网结构，有较好的适应性. 因此，设计一种新型低风压正馈线，用于降低正馈线的舞动幅值，保障牵引变电系统的安全可靠运行十分必要.

作用于架空输电导线的风载荷占整个线路所受风载荷的50%以上^[2]，降低正馈线所受风压不仅可以减小线索舞动幅值，还可以降低因线间放电而引起的跳闸风险. 20世纪70年代，日本关西电气与住友电气等单位对多种不同表面形状的导线进行了风洞试验，研究结果表明，导线风阻力系数与导线表面形状有较大关系^[3]. 20世纪90年代起，关西电气和住友电气对低风压导线的运行机理进行了持续研究，研究结果表明，低风压导线负压区面积小于普通导线，风阻力系数较小^[4-5]. 我国在低风压导线领域起步较晚，但发展较快. 近年来，上海电缆研究所、无锡华能电缆有限公司、江苏中天科技股份有限公司等单位研发了不同表面结构的低风压导线产品，并申请了专利^[6].

以6种不同表面形状的低风压正馈线和常规正馈线模型为研究对象，对各型正馈线在12～24 m/s （间隔3 m/s）风载荷作用下的舞动情况进行仿真，监测记录不同型号的低风压正馈线和常规正馈线在不同风载荷下的风阻力系数和跨距中点位移值，分析低风压正馈线表面结构参数对风阻力系数和跨距中点位移值变化的影响规律；对不同风载荷作用下风阻力系数较小的低风压正馈线建立三维有限元模型，并施加轴向拉力，分析其在轴向拉力作用下的形变及应力情况，研究成果为低风压正馈线的制造、选型及现场维护提供理论依据.

1. 模型建立

以现场架设的常规正馈线作为依据，建立常规正馈线二维模型，其二维截面结构如图1所示. 图中，R = 11.88 mm，为正馈线半径. 正馈线是由2层钢股和3层铝股相互绞合而成，其中，钢股直径为2.22 mm，铝股直径为2.85 mm.

图 1 常规正馈线二维截面示意

Figure 1. Two-dimensional cross-sectional diagram of conventional catenary positive feeder

下载: 全尺寸图片幻灯片

本文以低风压导线运行机理为基础，设计凹槽数为8、不同凹槽半径的6种低风压正馈线模型，其中，一种低风压正馈线模型截面结构如图2所示，线径均为23.76 mm. 与常规正馈线相比，低风压正馈线模型的最外层由8根中间带有凹槽的铝股线构成，凹槽的小圆弧半径r 与常规正馈线半径R的比值为0.10～0.15，其余层股线结构参数与常规正馈线相同.

图 2 r/R = 0.14型低风压正馈线截面示意

Figure 2. Cross-sectional diagram of low-wind-pressure catenary positive feeder with r/R = 0.14

下载: 全尺寸图片幻灯片

2. 仿真计算与分析

2.1 仿真计算

对r/R = 0.10～0.15的6种低风压正馈线和常规正馈线模型进行12、15、18、21、24 m/s风载荷下的气动力特性仿真. 首先，设置计算域边界条件，将计算域左侧边界设置为速度入口，导线表面采用无滑移壁面边界，右侧边界设置为压力出口. 迭代收敛残差值取1 × 10⁻⁵，时间步长为0.005 s，计算1000步，以r/R = 0.14型低风压正馈线为例，仿真计算得到常规正馈线和低风压正馈线在18 m/s风载荷下的阻力系数C_D时程图，如图3所示. r/R = 0.14型低风压正馈线在18 m/s风载荷下的阻力系数时程曲线幅值明显小于常规正馈线，为各低风压正馈线中阻力系数幅值最小的一种. 对45 m跨距正馈线在只受重力作用下线索悬垂状态找形成功后，将阻力系数以线性插值的方式添加，得到常规正馈线和r/R = 0.14型低风压正馈线跨距中点在18 m/s风载荷作用下的垂向位移时程图，如图4所示. 在同一坐标系下，r/R = 0.14型低风压正馈线垂向位移曲线幅值明显小于常规正馈线，即r/R = 0.14型低风压正馈线能够降低舞动幅值.

图 3 阻力系数时程图

Figure 3. Time course diagram of drag coefficients

下载: 全尺寸图片幻灯片

图 4 垂向位移曲线

Figure 4. Vertical displacement curves

下载: 全尺寸图片幻灯片

2.2 气动力参数分析

对6种低风压正馈线和常规正馈线在不同风载荷下的气动力特性进行仿真计算，得到不同线型在不同风载荷下的阻力系数，如图5所示. 统计6种低风压正馈线在18 m/s风载荷作用下跨距中点横向和垂向位移最大值，如图6所示.

图 5 不同低风压正馈线模型阻力系数曲线

Figure 5. Drag coefficient curves for different types ofcatenary positive feeder models

下载: 全尺寸图片幻灯片

图 6 跨距中点位移最大值

Figure 6. Maximum values of displacement at midspan points

下载: 全尺寸图片幻灯片

由图5可知，常规正馈线和6种低风压正馈线风阻力系数基本上随风速的增大呈减小趋势，且在整个测试风速范围内，低风压正馈线阻力系数均小于常规正馈线，说明本文设计的低风压正馈线模型具有防舞效果. 其中：常规正馈线气动力参数在整个测试风速范围内随风速的增大而减小， r/R = 0.10～ 0.11型低风压正馈线阻力系数交替出现下降和上升；r/R = 0.12～0.15型低风压正馈线阻力系数先上升之后一直下降；r/R = 0.14型低风压正馈线除在24 m/s风速时阻力系数略大于r/R = 0.15外，在其余测试风速时阻力系数均小于其他测试对象，为测试对象中降阻效果最好的线型.

由图6可知，常规正馈线跨距中点横向位移最大值为1.338 m，垂向位移最大值为1.240 m，低风压正馈线跨距中点位移最大值均较常规正馈线小，且最大位移值随r/R值的增大整体上呈现下降的趋势，但r/R = 0.15型低风压正馈线位移最大值较r/R = 0.14型低风压正馈线大，说明低风压正馈线设计的关键在于找到恰当的r/R值；r/R = 0.14型低风压正馈线位移幅值最小，其横向位移最大值为0.990 m，垂向位移最大值为0.910 m，较常规正馈线分别下降26.0%和26.6%，与图5风阻力系数相对应，说明了本文仿真方法的合理性以及仿真结果的准确性.

3. 低风压正馈线受力特性分析

正馈线在舞动过程中线夹出口处会产生大小不断变化的集中应力，会加剧连接金具的磨损以及线索疲劳断股. 为研究低风压正馈线在舞动时的受力特性，根据国际大电网会议的建议，以线夹出口89 mm处导线的动弯应变来评估低风压正馈线的运行状况^[7]. 对图5、6各正馈线仿真结果分析发现，r/R = 0.12，0.13，0.14型3种低风压正馈线防舞效果较佳. 因此，建立3种低风压正馈线89 mm长度三维模型，在有限元软件中对自由端面施加一定拉伸载荷，模拟正馈线舞动时的受力情况，分析低风压正馈线发生舞动时的形变量及应力特性^[8-9].

3.1 建立有限元模型

兰新高铁现场架设的常规正馈线结构参数如表1所示，该正馈线铝的杨氏模量为59 GPa，泊松比为0.30，钢的杨氏模量为190 GPa，泊松比为0.28，额定拉断力为83.42 kN. 本文以常规正馈线结构参数为依据，建立89 mm长度低风压正馈线三维模型，在固定端建立三维坐标轴O-XYZ. 其中，r/R = 0.14型低风压正馈线三维模型如图7所示，最外层铝股线中央带有凹槽，股线数为8股，其他层股线结构参数与常规正馈线相同.

表 1 常规正馈线结构参数

Table 1. Structural parameters of conventional positive feeder

材料	层数	股数/股	直径/mm	节径/mm	节距/mm	绞向
钢	最内层	1	2.22
钢	次内层	6	2.22	21	139.86	左
铝	次外层	10	2.85	13	160.68	右
	邻外层	16	2.85	12	216.72	左
	最外层	22	2.85	11	261.36	右

下载: 导出CSV

| 显示表格

图 7 r/R = 0.14型低风压正馈线三维模型

Figure 7. Three-dimensional model of positive feeder with r/R = 0.14

下载: 全尺寸图片幻灯片

3.2 仿真方法验证

1）仿真设置. 在有限元软件中设置钢铝股线的材料属性，将每根股线的中心节点等效为一个整体，在相邻股线之间建立接触对. 在设置边界条件时，将正馈线模型位于线夹一端完全固定约束，即在模型的固定端端面上约束X、Y、Z 3个方向的自由度. 为防止产生端部效应，在模型的自由端端面上建立一个刚域点，将该端面上所有自由度与该刚域点耦合形成一个刚域面，在刚域点上施加运行张力. 最后，采用扫掠法对模型进行正六面体网格划分^[10-12]，得到的模型网格图如图8所示.

图 8 r/R=0.14型低风压正馈线网格示意

Figure 8. Schematic grid of positive feeder with r/R=0.14

下载: 全尺寸图片幻灯片

2）方法验证. 我国一般将导线的运行张力设定为15%～25% 额定拉断力^[13]（rated tensile strength，RTS），兰新高铁考虑正馈线新线系数后正馈线的最大许用张力为32137 N，为额定拉断力的38.5%，但正馈线长期在最大许用张力下运行，容易导致疲劳断股. 本文对常规正馈线施加25% RTS，即20.855 kN拉力，仿真得出各层股线轴向张力，将仿真结果与式（1）正馈线各层股线理论张力计算式结果进行对比^[14]，结果见表2.

表 2 常规正馈线各层股线轴向张力

Table 2. Axial tension of each layer of conventional positive feeder kN

材料	层数	理论值	仿真值	误差
钢	最内层	5.963	5.921	0.242
钢	次内层	7.839	7.818	0.221
铝	次外层	3.956	3.651	0.305
	邻外层	5.045	4.889	0.156
	最外层	3.383	3.112	0.271

下载: 导出CSV

| 显示表格

，

$\begin{split} &{F_n} = \frac{{{\text{π}} d_n^2}}{4}{{\textit{z}}_n}{E_n}{{ }}\cos \; {\alpha _n} \;\times\\ &\quad {\cos \left( {\alpha _n}\sqrt {{{(1 + {\varepsilon _{\rm{i}}})}^2} + {{(\tan {\alpha _n} - \mu {\varepsilon _{\rm{i}}})}^2} - 1} \right) } ， \end{split}$

(1)

式中：F_n为第n层股线轴向张力； ${d_n}$ 为股线直径； ${{\textit{z}}_n}$ 为股线数； ${E_n}$ 为股线弹性模量； ${\alpha _n}$ 为拉伸前股线捻角； ${\varepsilon _{\rm{i}}}$ 为股线轴向伸长率； $\mu$ 为该层股线的泊松比.

由表2可知，常规正馈线在25% RTS作用下，2层钢芯承担了54.1%的拉力，3层铝股线承担了45.9%的拉力，这与正馈线的设计初衷和现场运行情况相符. 仿真值与理论值存在一定误差，是因为理论计算时未考虑股线之间的挤压和摩擦对正馈线应力的影响. 但误差仍处于合理范围内，故本文所采用的仿真方法能够恰当地模拟正馈线在受到轴向拉力时的应力-应变特性.

3.3 结果分析

3.3.1 低风压正馈线受力形变及应力分析

在有限元软件中对r/R = 0.12，0.13，0.14型低风压正馈线三维模型自由端面施加25% RTS，分别比较3种正馈线的形变位移及应力变化情况^[15-16]. 其中，r/R = 0.14型低风压正馈线在施加25% RTS后，轴向整体形变及各层股线轴向形变如图9所示.

图 9 r/R = 0.14型低风压正馈线形变云图

Figure 9. Deformation nephogram of positive feeder with r/R = 0.14

下载: 全尺寸图片幻灯片

由图9（a）可知，正馈线在受到轴向拉力的作用下会发生一定轴向形变，固定端形变量最小，越往自由端，形变量越大，这与现实情况相吻合. 由图9（b）可知，各层股线在受到轴向拉力的情况下，形变量是不同的，轴向形变量从钢层到铝层逐渐增大，至最外层铝股线达到最大，即在现实中正馈线舞动时，最外层铝股线最容易发生金属疲劳断股，这是由于钢的杨氏模量大于铝的杨氏模量，铝的延展性较钢强^[17-18]，在同一拉力作用下，铝的形变量大于钢. 其次，正馈线在受到轴向拉力时，内层股线受到外层股线的挤压，使得内层股线的形变量小于外层股线.

对r/R = 0.14型低风压正馈线施加25% RTS，等效应力云图见图10，其纵向中心截面应变及形变云图见图11.

图 10 r/R = 0.14型低风压正馈线应力

Figure 10. Stress nephogram of positive feeder with r/R = 0.14

下载: 全尺寸图片幻灯片

图 11 r/R = 0.14型低风压正馈线轴向截面云图

Figure 11. Axial section nephogram of positive feeder with r/R = 0.14

下载: 全尺寸图片幻灯片

由图10（a）可知，次内层钢股线在正馈线振动时承担了大部分轴向应力，且除最内层直钢股应力分布均匀外，其他层股线应力分布不均，但具有一定的规律，即应力极值点的位置与正馈线每层股线的绞向相同，这是因为正馈线在轴向拉力作用下，同层相邻股线在绞合方向上相互挤压，形成应力集中点. 从图10（b）可知，钢股等效应力远大于铝股，即在正馈线舞动时钢股承受了很大一部分应力，且应力在直钢芯两侧对称分布，应力从固定端和自由端到中间的变化趋势相似，保证了正馈线受力对称.

由图11（a）可知，股线轴向应变沿最内层钢股两侧对称分布，中心钢股承受了最大拉变，这符合正馈线的设计初衷，邻外层钢股出现了最大压变，这是因为该层股线受到相邻两层股线的挤压. 从图11（b）可知，由固定端到自由端整体形变量逐渐增大，自由端形变量远大于固定端；由于中心钢股非螺旋结构，且钢的杨氏模量大，延展性较铝差，抗拉强度大，所以形变量最小；次内层钢股和邻外层铝股在绞线中间位置附近受到相邻股线的严重挤压，出现了最大形变量.

对r/R = 0.14型低风压正馈线施加25% RTS，沿轴向坐标轴Z轴截取固定端Z = 0至自由端端面，间隔8.9 mm，共11个轴向应力截面，分析其轴向应力，其中4个应力截面如图12所示.

图 12 25% RTS作用下r/R = 0.14型低风压正馈线横向截面应力云图

Figure 12. Stress nephogram of horizontal cross-section of positive feeder with r/R = 0.14 under 25% RTS

下载: 全尺寸图片幻灯片

由图12可知，正馈线在轴向载荷作用下会发生一定程度的扭转. 正馈线的不同截面轴向应力分布不同，中心直钢芯上应力分布较均匀，螺旋钢层和铝层同一股线应力呈阶梯状分布，且应力极值点位置与正馈线层绞合方向相关；从固定端端面到自由端端面的不同截面上，应力极值点位置从与绞合方向相反到与绞合方向相同，但均位于股线接触处，说明在股线接触位置容易出现应力集中点，易引起股线磨损断股；中间位置截面轴向应力呈现中心对称，且在提取的截面中应力最小，轴向应力整体上呈现两端大中间小的情况.

3.3.2 3种低风压正馈线受力特性比较

为更准确地反映3种低风压正馈线在25% RTS作用下的受力特性，对状态变化参数进行比较，得到3种低风压正馈线25% RTS作用下状态参数变化曲线，如图13所示.

图 13 3种低风压正馈线25% RTS作用下状态参数变化曲线

Figure 13. Variation of state parameter for the three types of positive feeders under 25% RTS

下载: 全尺寸图片幻灯片

由图13（a）可知，2层钢股承受了绝大部分应力，邻外层铝股在3层铝股中承受的应力最大，不同型号低风压正馈线在25% RTS作用下，从内向外第1、4层股线承受的应力基本相同，最外层股线最大应力随r/R值的增大而增大. 由图13（b）可知，在轴向拉力的作用下，股线位移量从内层到外层依次增大，表明最外层铝线最容易疲劳断股. 由于中心钢股没有螺旋，抗拉强度大，所以r/R = 0.12，0.13，0.14型低风压正馈线中心钢股位移量基本相等，r/R = 0.13，0.14型低风压正馈线第2、4层股线位移量基本相等；r/R = 0.12型低风压正馈线第2、5层股线位移量均小于其他低风压正馈线，第5层股线位移量随r/R值的增大而增大.

4. 结　论

通过对设计的低风压正馈线进行防舞有效性仿真分析，发现低风压正馈线达到了预期效果，并对其中3种防舞效果较佳的低风压正馈线进行受力特性分析，得出以下结论，并对低风压正馈线的制造、选型及现场维护给出以下建议：

1）低风压正馈线在受到轴向拉力时，铝股线的轴向形变量大于钢股线，为了平衡正馈线抗拉强度和导电性能，在制造正馈线时可以考虑将钢股线和铝股线交替绞制.

2）在轴向载荷作用下，低风压正馈线在线夹处受到很大的应力，加剧了正馈线与线夹的磨损，容易导致股线断裂. 在正馈线的日常维护中应该加强巡视，确保线夹转动灵活，减小线夹处正馈线的静应力.

3）低风压正馈线在轴向载荷作用下会发生一定程度的扭转，在股线接触处出现应力集中点，应力集中点位置与正馈线绞合方向相关. 在制造正馈线时可以考虑在股线表面覆缓冲层，减缓股线之间的振荡冲击，延长正馈线使用寿命.

4）对3种防舞效果较为理想的低风压正馈线进行受力分析，发现在同一轴向载荷作用下，最外层铝股线层的位移量与r/R比值成正比例关系. 而r/R值越大，最外层铝股线横截面积越小，在正馈线舞动时越容易疲劳断股，因此，在低风压正馈线选型时应该综合考虑，平衡防舞有效性与使用寿命.

致谢：兰州交通大学天佑创新团队计划（TY202010）资助.

References(27)

References

PAVLOV V, SCHUKIN A, CHERKASOVA T. Exploring automated reasoning in first-order logic:tools,techniques and application areas[J]. Communications in Computer & Information Science, 2013, 394(1): 102-116.

DAVIS M. The early history of automated deduction[J]. Handbook of Automated Reasoning, 2002, 714(3): 5-15.

PLAISTED D A. History and prospects for first-order automated deduction[C]//Proceedings of 25th International Conference on Automated Deduction. Cham: Springer, 2015: 3-28.

ROBINSON J A. The generalized resolution principle[M]//SIEKMANN J, WRIGHTSON G. Automation of Reasoning-3. Berlin Heidelberg: Springer International Publishing, 1983: 135-151.

RUBIN N, HARRISON M C. Another generalization of resolution[J]. Journal of the Association for Computing Machinery, 1978, 25(3): 341-351. doi: 10.1145/322077.322078

LU Ruzhan, LIN Kai, SUN Yongqiang. Colored resolution,pi-colored clash and its completeness[J]. Journal of Computer, 1987, 12: 18-25.

LOVELAND D W. A linear format for resolution[C]//Symposium on Automatic Demonstration. Berlin: Springer, 1970: 147-162.

LUCKHAM D. Refinements in resolution theory[C]//Symposium on Automatic Demonstration. Berlin: Springer, 1970: 163-190.

OVERBEEK R, MCCHAREN J, WOS L. Complexity and related enhancements for automated theorem-proving programs[J]. Computers & Mathematics with Applications, 1976, 2(1): 1-16.

ROBINSON J A. Automatic deduction with hyper-resolution[J]. International Journal of Computing & Mathematics, 1965, 1(3): 227-234.

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, 2016, 12(4): 1-24.

RIAZANOV A, VORONKOV A. The design and implementation of vampire[J]. Ai Communications, 2002, 15(2): 91-110.

VORONKOV A. First-order theorem proving and vampire[C]//Proceedings of International Conference on Computer Aided Verification. Berlin: Springer-Verlag, 2013: 1-35.

SCHULZ S. E-a brainiac theorem prover[J]. AI Com- munications, 2002, 15(2): 111-126.

SCHULZ S. System description: E 1.8[C]//Proceedings of 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Berlin: Springer-Verlag, 2013: 735-743.

BAUMGARTNER P, BAX J, WALDMANN U. Beagle－a hierarchic superposition theorem prover[C]// Proceedings of 25th International Conference on Automated Deduction. Cham: Springer, 2015: 367-377.

WEIDENBACH C, BRAHM U, HILLENBRAND T, et al. Spass version 2.0[C]//Proceedings of International Conference on Automated Deduction. Berlin: Springer-Verlag, 2002: 275-279.

VORONKOV A. AVATAR: The architecture for first-order theorem provers[C]//Proceedings of International Conference on Computer Aided Verification. Cham: Springer, 2014: 696-710.

DENZINGER J, KRONENBURG M, SCHULZ S. DISCOUNT-a distributed and learning equational prover[J]. Journal of Automated Reasoning, 1997, 18(2): 189-198. doi: 10.1023/A:1005879229581

MCCUNE W, WOS L. Otter-the CADE-13 competition incarnations[J]. Journal of Automated Reasoning, 1997, 18(2): 211-220. doi: 10.1023/A:1005843632307

REGER G, TISHKOVSKY D, VORONKOV A. Cooperating proof attempts[C]//Proceedings of 25th International Conference on Automated Deduction. Cham: Springer, 2015: 339-355.

SCHULZ S, MOHNMANN M. Performance of clause selection heuristics for saturation-based theorem proving[C]//Proceedings of 8th International Joint Conference. Cham: Springer, 2016: 330-345.

HODER K, REGER G, SUDA M, et al. Selecting the selection[C]//Proceedings of 8th International Joint Conference on Automated Reasoning. Cham: Springer, 2016: 313-329.

XU Yang, LIU Jun, CHEN Shuwei, et al. Contradiction separation based dynamic multi-clause synergized automated deduction[J]. Information Sciences, 2018, 462(5): 93-113.

XU Yang, LIU Jun, CHEN Shuwei, et al. Distinctive features of the contradiction separation based dynamic automated deduction[C]//Proceedings of 13th International FLINS Conference on Decision Making and Soft Computing. Belfast: World Scientific, 2018: 725-732.

SUTCLIFFE.G.The 7th IJCAR automated theorem proving system competition-CASC-J7[J]. AI Communications, 2015, 28(4): 683-692. doi: 10.3233/AIC-150668

SUTCLIFFE.G.The 8th IJCAR automated theorem proving system competition-CASC-J8[J]. AI Communications, 2016, 29(5): 607-619. doi: 10.3233/AIC-160709

Relative Articles

[1]	ZHANG Hong, JIANG Xiaogang, ZHU Zhiwei, XIA Runchuan, ZHOU Jianting. Review on Intelligent Image Recognition of Apparent Diseases of Stay Cable[J]. Journal of Southwest Jiaotong University, 2025, 60(1): 10-26. doi: 10.3969/j.issn.0258-2724.20220647
[2]	YANG Yanchun, YAN Yan, WANG Ke. Infrared and Visible Image Fusion Based on Attention Mechanism and Illumination-Aware Network[J]. Journal of Southwest Jiaotong University, 2024, 59(5): 1204-1214. doi: 10.3969/j.issn.0258-2724.20230529
[3]	YUE Chuan, WANG Lide, YAN Haipeng. Attack-Sample Generation Method for Train Communication Network Under Few-Shot Condition[J]. Journal of Southwest Jiaotong University, 2023, 58(6): 1277-1285. doi: 10.3969/j.issn.0258-2724.20210557
[4]	XIA Ying, LIU Min. Traffic Flow Prediction Based on Spatial-Temporal Attention Convolutional Neural Network[J]. Journal of Southwest Jiaotong University, 2023, 58(2): 340-347. doi: 10.3969/j.issn.0258-2724.20210526
[5]	YANG Yueyi, WANG Lide, WANG Chong, WANG Huizhen, LI Ye. Fault Diagnosis Method Based on Deep Active Learning For MVB Network[J]. Journal of Southwest Jiaotong University, 2022, 57(6): 1342-1348, 1385. doi: 10.3969/j.issn.0258-2724.20210195
[6]	LI Zechen, LI Hengchao, HU Wenshuai, YANG Jinyu, HUA Zexi. Masked Face Detection Model Based on Multi-scale Attention-Driven Faster R-CNN[J]. Journal of Southwest Jiaotong University, 2021, 56(5): 1002-1010. doi: 10.3969/j.issn.0258-2724.20210017
[7]	YANG Gang, LI Hengchao, TAN Bei, SHI Chaoqun, ZHANG Xueqin, GUO Yujun, WU Guangning. Application of Hierarchical Extreme Learning Machine in Prediction of Insulator Pollution Degree Using Hyperspectral Images[J]. Journal of Southwest Jiaotong University, 2020, 55(3): 579-587. doi: 10.3969/j.issn.0258-2724.20190093
[8]	YUAN Fei, ZHAO Xuyan, WANG Yige, ZHAO Zhisheng. Smoke Recognition Algorithm Based on Lightweight Convolutional Neural Network[J]. Journal of Southwest Jiaotong University, 2020, 55(5): 1111-1116, 1132. doi: 10.3969/j.issn.0258-2724.20190777
[9]	TIAN Sheng, ZHANG Jianfeng, ZHANG Yutian, XU Kai. Lane Detection Algorithm Based on Dilated Convolution Pyramid Network[J]. Journal of Southwest Jiaotong University, 2020, 55(2): 386-392, 416. doi: 10.3969/j.issn.0258-2724.20181026
[10]	XIANG Yu, CONG Deming, ZHANG Yang, YUAN Fei. Two-Stream Neural Network Fusion Model for Highway Fog Detection[J]. Journal of Southwest Jiaotong University, 2019, 54(1): 173-179. doi: 10.3969/j.issn.0258-2724.20180205
[11]	ZHAI Donghai, HOU Jialin, LIU Yue. Parallel Algorithms for Text Sentiment Analysis Based on Deep Learning[J]. Journal of Southwest Jiaotong University, 2019, 54(3): 647-654. doi: 10.3969/j.issn.0258-2724.20160948
[12]	HOU Jin, LÜ Zhiliang, XU Mao, WU Peijun, LIU Yuling, ZHANG Xiaoyu, CHENG Zeng. Combined Neural Networks Based on Deep Learning for Signal Detection in Aeronautical Communications[J]. Journal of Southwest Jiaotong University, 2019, 54(4): 863-869, 878. doi: 10.3969/j.issn.0258-2724.20180164
[13]	QIN Zhentao, YANG Wunian, YANG Ru, PAN Peifen, DENG Cong. Hyperspectral Image Classification Based on Structured Dictionary Learning[J]. Journal of Southwest Jiaotong University, 2015, 28(2): 336-341. doi: 10.3969/j.issn.0258-2724.2015.02.020
[14]	JIA Zhen, HE Dake, YIN Hongfeng, LI Tianrui. Acquisition of Part-Whole Relations Based on Unsupervised Learning[J]. Journal of Southwest Jiaotong University, 2014, 27(4): 590-596. doi: 10.3969/j.issn.0258-2724.2014.04.005
[15]	HAN Zhi-Wei, LIU Zhi-Gang, ZHAO Fei. Directional Reconstruction of Super Resolution Image by Magnifying Curvelet Basis[J]. Journal of Southwest Jiaotong University, 2011, 24(4): 620-625. doi: 10.3969/j.issn.0258-2724.2011.04.015
[16]	XIAO Qinghua, ZHANG Jichun, XIA Zhenrong. Calculation of Tunnel Blasting Parameters Based on Prior Knowledge and BP Neural Network[J]. Journal of Southwest Jiaotong University, 2007, 20(5): 537-541.
[17]	XU Min, ZHANG Liping, ZHU Wujia. Document Classification by Semi-supervised Online Learning Based on ART[J]. Journal of Southwest Jiaotong University, 2006, 19(3): 335-340.
[18]	YE Li-sheng, HE Feng-dao. The Learning of BP Neural Network Based on Evolutionary Programming[J]. Journal of Southwest Jiaotong University, 2001, 14(5): 545-548.
[19]	He Zhengyou, Qian Qingquan. An Improved Wavelet Neural Network Structure and Its Learning Algorithm[J]. Journal of Southwest Jiaotong University, 1999, 12(5): 436-440.
[20]	HE Zheng-You, Jian-Qing-Quan. An Improved Wavelet Neural Network Structure and Its Learning Algorithm[J]. Journal of Southwest Jiaotong University, 1999, 12(5): 436-440.

Supplements(0)

Cited By

Cited by
Periodical cited type(1)
1. 詹宝容，庾锡昌. 联合收割机裂纹转子与滚动轴承故障诊断系统研究——基于卷积神经网络. 农机化研究. 2024(05): 187-191 .
Other cited types(4)

Proportional views

Proportional views

通讯作者: 陈斌, bchen63@163.com

1.
沈阳化工大学材料科学与工程学院沈阳 110142

Figures(3) / Tables(2)

Get Citation

PDF

XML

Article views(625) PDF downloads(15)