一阶逻辑中的扩展子句消去原则

宁欣然; 徐扬; 何星星

doi:10.3969/j.issn.0258-2724.20180974

一阶逻辑中的扩展子句消去原则

doi: 10.3969/j.issn.0258-2724.20180974

宁欣然^1,2,,
徐扬^1,3,
何星星^1,3

基金项目: 国家自然科学基金（1673320）；中央高校基本科研业务费专项资金（2682018ZT10）

详细信息

作者简介:
宁欣然（1990—），女，博士研究生，研究方向为自动推理、人工智能，E-mail：xinxinran@my.swjtu.edu.cn

中图分类号: V221.3
计量
- 文章访问数: 583
- HTML全文浏览量: 256
- PDF下载量: 12
- 被引次数: 0
出版历程
- 收稿日期: 2018-11-27
- 修回日期: 2019-06-18
- 网络出版日期: 2020-03-30
- 刊出日期: 2020-06-01

Extended Unifying Principle of Clause Elimination in First-Order Logic

NING Xinran^{1,2
,},
XU Yang^1,3,
HE Xingxing^1,3

摘要

摘要: 对于一阶逻辑定理证明器，子句集化简一直是必不可少的步骤，这将有助于提高后续一阶逻辑定理证明器的证明效率. 针对子句冗余性的判断，提出了一种评估子句冗余性的原则：集合蕴涵模归结原则. 并且证明了该原则在不带等词一阶逻辑上的可靠性，根据该原则删除子句，不会影响原始子句集的不可满足性或者可满足性. 此外，依据该原则提出了两种新型的一阶逻辑预处理方法：集合归结包含消去（set resolution subsumption, SRSE）方法和集合归结不对称恒真消去（set resolution asymmetric tautology elimination, SRATE）方法，并证明了这两种子句消去方法在不带等词一阶逻辑子句集上的可靠性. 最后在理论上比较了SRSE方法和归结包含消去（sesolution subsumption elimination, RSE）方法以及SRATE方法和归结不对称恒真（sesolution asymmetric tautology elimination, RATE）方法之间的有效性，结果表明SRSE方法和SRATE方法分别比RSE方法和RATE方法更为有效.
- 集合蕴涵模归结 /
- 一阶逻辑 /
- 蕴涵模归结 /
- 子句消去方法 /
- 预处理方法
Abstract: Simplifications are indispensable steps of first-order theorem proving, which can enhance the proving efficiency of first-order theorem provers. Set implication modulo resolution, a principle of identifying the redundancy property of clauses, is proposed. The soundness of this principle in first-order logic without equality is proved, which means that eliminating clauses according to the principle has not effect on the unsatisfiability or satisfiability of original formulas. In addition, two novel preprocessing methods in first-order theorem proving are developed given the principle of set implication modulo resolution, i.e., set resolution subsumption elimination (SRSE) and set resolution asymmetric tautology elimination (SRATE). The soundness of the two clause elimination methods is also demonstrated. Finally, the effectiveness is theoretically compared between SRSE and resolution subsumption elimination (RSE) and between SRATE and resolution asymmetric tautology elimination (RATE), which shows SRSE and SRATE are more effective than RSE and RATE, respectively.
- set implication modulo resolution /
- first-order logic /
- implication modulo resolution /
- clause elimination method /
- preprocessing technique

HTML全文

CRTS Ⅱ型板式无砟轨道（以下简称“Ⅱ型板”）是我国高速铁路的主型轨道结构之一，无砟道床主要由轨道板、宽窄接缝、CA砂浆层、支承层等组成，轨道板通过纵向连接器及混凝土组成的结构实现连接，形成纵连式轨道^[1]. 根据运营线路的现场调研，Ⅱ型板总体使用情况良好，但随着高速铁路运营时间的推移，受大规模施工作业、多变的下部基础和经时效应下的结构退化等因素限制，轨道结构不可避免地会产生局部伤损^[2]. 无砟轨道结构的疲劳耐久性是保证其设计寿命的主要指标，根据当前高速铁路无砟轨道的设计理论与方法，采用混凝土设计规范对其疲劳特性和耐久性进行检算时，既有无砟轨道均满足要求^[3]. 但无砟轨道在实际运营过程中出现了多种形式的疲劳损伤，尤其是在轨道的新老混凝土结合面，该现象更为普遍，如轨道板与砂浆层的层间脱连. 轨道板在列车轮载作用下呈上压下拉的受弯形态，因混凝土受拉压特性的差异性，轨道板的损伤多表现为由板底发展的裂缝^[4]. 列车轮载的高频疲劳作用也会使结构内部损伤不断累积，导致刚度下降、变形增加，最终引发结构的损坏.

目前针对混凝土的疲劳损伤普遍采用Miner线性准则与S-N曲线作为评估方法，如宋玉普等^[5-7]通过对混凝土多轴疲劳试验的分析，建立多种应力状态下混凝土疲劳的S-N曲线和疲劳破坏准则；Cornelissen等^[8]通过修正混凝土的S-N曲线，论证了压应力对混凝土的抗拉疲劳破坏有负面影响；Dobromil等^[9]通过将S-N曲线转化为材料损伤的方法，提出了一种适用于高周疲劳的混凝土裂缝损伤新模型. 传统的疲劳损伤判定法则仅考虑荷载幅值与次数的作用，未考虑荷载频率对损伤的影响. 列车轮载作用下无砟轨道混凝土结构应力幅值一般较低，但是荷载的循环次数很高，属于复杂应力状态下的高周疲劳问题^[10]，因此针对无砟轨道使用寿命预测方法应区别于普通混凝土结构的寿命预测.

针对无砟轨道的疲劳损伤问题，徐庆元等^[11-12]对荷载组合作用下桥上纵连板式无砟轨道疲劳应力谱、疲劳寿命分析模型及疲劳破坏关键技术参数进行了研究；Poveda等^[13]与Tarifa等^[14]分别通过数值仿真与现场试验的方法，研究了框架式无砟轨道在列车时变荷载作用下的瞬态效应，通过分析应力幅值的影响，提出了针对框架式无砟轨道的疲劳准则；Konings^[15]基于Miner线性疲劳损伤准则和钢筋混凝土S-N曲线，初步分析了服役期间复杂载荷下RHEDA 2000型无砟轨道的疲劳寿命；刘学毅等^[16]通过对先张与后张Ⅲ型轨道板的疲劳试验，研究了轨道结构各部件位移及轨道板应力随环境温度及列车轮载疲劳作用次数的变化；童明娜等^[17]针对Ⅱ型板潜在的疲劳失效模式，建立列车荷载与温度荷载共同作用下轨道板混凝土疲劳功能函数，开展了基于时变可靠度理论的疲劳时变可靠性研究. Chapeleau等^[18]开展了无砟轨道实尺模型试验，通过测量轨道板内疲劳应变，探索了板中裂纹的扩展规律.

上述研究主要通过数值仿真与现场试验的方法，关注了无砟轨道结构整体的疲劳特性，并初步探索了损伤发展机理，但针对列车高频轮载作用下无砟轨道疲劳特性的研究尚需深入. 特别是在轮对作用间隙阶段，列车高频轮载会引发板体的自振效应，轨道结构会产生微小的高频振动，针对该阶段振动对轨道结构疲劳特性的影响，目前鲜有系统的研究. 故深入探讨列车高频荷载下轨道板的疲劳特性以及轨道板自振效应对疲劳寿命的影响程度，对预防无砟轨道进入故障高发期、保证列车的安全高效运行具有重大的现实意义.

1. 计算模型与参数

建立如图1所示的分析模型研究局部脱空下轨道板的疲劳特性，相应的有限元模型局部如图2所示，并作如下基本假定：

图 1 轨道结构垂向振动分析模型

Figure 1. Vertical vibration analysis model of track structure

下载: 全尺寸图片幻灯片

图 2 有限元模型局部示意

Figure 2. Local schematic diagram of finite element model

下载: 全尺寸图片幻灯片

1）钢轨、轨道板简化为均质的连续弹性支承欧拉梁；

2）扣件简化为线弹性点支承；砂浆层简化为均布的弹性支承，忽略轨道板脱空处砂浆层的支承作用；

3）忽略支承层及其他轨道附属结构对轨道板振动的影响.

图2有限元模型采用欧拉梁单元模拟轨道板、钢轨，为消除边界效应建立共计16块板长（约100 m），并选取模型中部轨道板作为分析对象；扣件采用线弹性的离散弹簧单元模拟；轨道板支承段与底座板之间的砂浆层约束简化为均布的线弹性约束. 列车轮载模式是计算疲劳效应的基础，以移动恒载模拟列车轮载作用，并通过瞬态分析方法获取轨道板的受力形态. 以京沪高速铁路为研究背景，按照京沪线上的主要车型CRH380建立典型车辆模型^[19]，模拟两个车辆，共计4个转向架、8个轮对以360 km/h的速度顺序通过钢轨，其中列车轴重为170 kN. 模型主要参数如表1所示^[1,2].

表 1 主要计算参数

Table 1. Main calculation parameters

部件	项目	取值
钢轨	弹性模量/Pa	2.06 × 10¹¹
	惯性矩/m⁴	7.745 × 10⁻³
	密度/（kg•m⁻³）	7850
	泊松比	0.30
	扣件刚度/（N•m⁻¹）	6.0 × 10⁷
轨道板	弹性模量/Pa	3.55 × 10¹⁰
	密度/（kg•m⁻³）	2400
	泊松比	0.20
	宽度（厚度）/m	2.55 （0.20）
CA砂浆	弹性模量/Pa	7.0 × 10⁹
	厚度/m	0.03
	单向受压刚度/（N•m⁻²）	5.95 × 10¹¹

下载: 导出CSV

| 显示表格

2. 轨道板振动力学特性分析

2.1 振动受力分析

受温度、水及列车动荷载等多场耦合荷载共同影响，砂浆层与轨道板间的粘结状态在线路运营后将极大减弱，板底部属于受力的薄弱部位，因此有必要关注轨道板在列车移动荷载作用下板底的受力形态. 为探究轨道板在列车移动荷载作用下的受力特性，假定脱空长度为L₀，轨枕间距为L_a，以L₀ = 0，2.0 L_a，5.0 L_a为例，分析轨道板在列车移动荷载作用下的弯矩时程分布规律，结果如图3所示.

图3表明，轨道板弯矩在轮对行驶于分析点正上方时达到最大值. L₀ = 0时，轨道板承受弯矩较小，弯矩量值为0.505 kN•m，此时板底拉应力为0.03 MPa，远小于Ⅱ型板C55混凝土的抗拉强度2.74 MPa，因此在轨道结构完好的条件下，列车轮载引发轨道板伤损的可能性较小. L₀ = 2.0 L_a，5.0 L_a时，弯矩量值分别为9.66、32.2 kN•m，根据受弯梁的正应力计算方法可得板底拉应力分别为0.56、1.89 MPa，初步计算表明，当L₀ = 6.2 L_a时，轨道板在单次轮对荷载作用下即达到轨道板的抗拉强度极限.

根据列车移动荷载分布特性，轨道板振动弯矩大致可分为5个阶段（见图3）：列车行驶于分析点前的阶段（阶段O）、第1车辆前转向架作用阶段（阶段Ⅰ）、同一车辆的前后2个转向架作用间隙阶段（阶段Ⅱ）、相邻车辆的2个转向架共同作用阶段（阶段Ⅲ）、列车行驶于分析点后的阶段（阶段A）. 图3表明，不同时间点相同阶段的振动弯矩时程分布基本相同（如图3中2个阶段Ⅰ与2个阶段Ⅱ），阶段O、Ⅱ、A的弯矩时程变化规律相近，阶段Ⅲ大致相当于2个阶段Ⅰ的作用效果. 以16车编组的CRH380列车为例，当1列车经过分析点时，轨道板弯矩时程曲线将经历共计1组阶段O、2组阶段Ⅰ、16组阶段Ⅱ、15组阶段Ⅲ、1组阶段A. 此外，在列车行驶于分析点前后（阶段O、A）以及2个转向架之间的阶段（阶段Ⅱ），因列车轮载引发了板体的自振效应，轨道板仍有量级较小的弯矩，但此时的弯矩变化频率远大于轮对行驶于分析点正上方时的弯矩变化频率，故在轨道结构疲劳分析过程中不应该予以忽略.

图 3 轨道板弯矩时程分布规律

Figure 3. Time history distribution of track slab bending moments

下载: 全尺寸图片幻灯片

2.2 自振频率分析

列车轮载为典型的周期性荷载，当荷载作用频率与轨道板自振频率相近时，易引发轨道结构的共振，此时列车轮载引发板体的自振效应可能会加剧轨道结构的疲劳损伤. 为探究轨道板振动频率分布特性，以L₀ = 0～10.0 L_a为例，分析L₀对轨道板自振频率的影响，结果如图4所示.

图 4 局部脱空影响下轨道板自振频率

Figure 4. Natural frequencies of track slab under the effect of partial de-bonding

下载: 全尺寸图片幻灯片

图4表明，轨道板自振频率与脱空长度呈负增长关系. 当轨道板不发生脱空时，轨道板的振动主要受砂浆层支承刚度的约束影响^[20]，因此轨道结构各阶自振频率集中于3500 Hz的量值. 当L₀ < 3.0 L_a时，轨道板的高阶频率相近，其量值亦集中于3500 Hz，表明此时高阶频率引发的是轨道板支承段的局部振动. 当L₀ > 4.0 L_a后，轨道板的自振频率随阶数增长，表明此时轨道板的振动能量主要集中于脱空段.

目前针对无砟轨道结构振动特性的分析普遍采用高速列车的车轮通过频率作为加载频率，假定列车轮载以恒定速度通过，若某一轴距对应的加载频率与自振频率相近，有引发轨道板共振的风险. 定义该轴距为临界轴距，若行车速度为360 km/h，局部脱空影响下列车轮载引发轨道结构共振的临界轴距如图5所示.

图 5 引发轨道结构共振的临界轴距

Figure 5. Critical wheelbase for resonance of track structure

下载: 全尺寸图片幻灯片

图5表明，引发轨道结构共振的临界轴距与脱空长度成正增长关系. CRH380车型的典型轴距主要有：固定轴距为2.5 m，同一车辆的前后两个转向架中心距为17.375 m，相邻车辆的两个转向架中心距为7.650 m，车辆间距为25.025 m^[20]. 图5表明，若行车速度为360 km/h，仅固定轴距有引发轨道板共振的风险. 若L₀ =0，此时的临界轴距约为0，故可认定轨道结构完好时，列车轮载不会引发轨道板的共振；L₀小于整块板长时，列车轮载不会引发轨道板的高阶共振; L₀ =7.0 L_a时，临界轴距与单组转向架的轴间距相等，表明此时列车轮载有引发轨道板1阶共振的风险，综合前述分析结果，列车轮载在引发轨道板共振前即发生板底开裂.

3. 轨道板振动疲劳特性分析

3.1 疲劳寿命预测方法

在建立轨道板寿命预测模型时，采用工程上常用的Miner线性损伤累积理论进行计算^[21]，当各种受载情况的损伤之和等于1时，轨道板发生疲劳破坏，即

$\sum\limits_i {\frac{{{n_i}}}{{{N_i}}}} = 1 \text{，}$

(1)

式中：n_i为第i阶段时疲劳荷载的当前作用组数，i =O,Ⅰ,Ⅱ,Ⅲ,A；N_i为第i阶段时应力水平的疲劳作用总组数.

由于轨道板混凝土抗拉强度远小于抗压强度，故在疲劳特性分析过程中只考虑拉应力部分的计数. Tepfers等^[21]通过拉伸疲劳试验推导出了混凝土单对数疲劳方程, 以列车组数作用下的疲劳破坏荷载循环次数为例，疲劳寿命方程表示为

$S = a - b\left( {1 - R} \right)\lg \;{N_{\rm{S}}},$

(2)

式中：R = σ _min/σ _max为应力比， σ _max、 σ _min分别为疲劳应力的上、下限；S = σ_max/f_t为应力水平，f_t为混凝土抗拉强度；a、b为疲劳试验所确定的系数， a =1.0，b =0.06110112^[22]；N_S为疲劳破坏时作用的列车组数.

当列车作用组数为1时，轨道板将承受共计64组轮对冲击（2组阶段Ⅰ、15组阶段Ⅲ）、17组高频自振（1组阶段O、1组阶段A、15组阶段Ⅱ）的作用，因此，N_S与N_O、N_I、N_Ⅱ、N_Ⅲ、N_A的关系为

$\frac{1}{{{N_{\rm{S}}}}} = \sum\limits_i {\frac{{{\alpha _i}}}{{{N_i}}}},$

(3)

式中：α_i为第i阶段的荷载周期系数，根据16车编组CRH380列车的特点，取α_O = 1，α_I = 2，α_Ⅱ = 16，α_Ⅲ = 15，α_A = 1.

文献[22]表明，式(2)在应力比较高时计算结果虽偏大，但满足实际工程的使用要求. 因此，可基于式(1) ～ (3)分析Ⅱ型板的高频振动疲劳特性.

通过有限元法得到列车移动荷载作用下轨道板分析点的弯矩时程曲线，换算成板底应力后采用雨流计数法^[23]对应力时程曲线进行各阶段的计数，由此得到相应的轨道板疲劳应力谱，代入式(1)～(3)确定轨道板的疲劳寿命.

各阶段对疲劳寿命的影响系数为

${r_i} = {{\left( {\frac{{{\alpha _i}}}{{{N_i}}}} \right)} \mathord{\left/ {\vphantom {{\left( {\frac{{{\alpha _i}}}{{{N_i}}}} \right)} {\left( {\frac{1}{{{N_S}}}} \right)}}} \right. } {\left( {\frac{1}{{{N_{\rm{S}}}}}} \right)}} = {\alpha _i}\frac{{{N_{\rm{S}}}}}{{{N_i}}} .$

(4)

若以阶段Ⅰ、Ⅲ的弯矩时程分布为例，分析列车轮载作用下无脱空轨道板的疲劳寿命，此时同一转向架上2个轮载存在叠加效应，轨道板在上述2个阶段出现幅值约为0.03 MPa的最大拉应力，通过雨流计数法得到该阶段列车轮载对轨道板体产生了幅值0.012 MPa、均值0.018 MPa的疲劳应力，共计64组. 式(1)～(3)计算表明，仅考虑荷载作用次数时（即仅考虑阶段Ⅰ、Ⅲ的疲劳荷载计数），当2.98 × 10¹³个列车组作用后，轨道板即发生疲劳破坏；若另考虑阶段O、Ⅱ、A板体自振的影响，以相同的计数方法算得考虑列车轮载引发板体自振的效应后，疲劳寿命为1.66 × 10¹³个列车组，表明考虑板体自振后，列车轮载对轨道板产生了约1.8倍的疲劳荷载当量.

3.2 脱空长度对疲劳特性影响

3.1节分析表明，阶段Ⅱ、Ⅲ具有较强的周期性，故以这2个阶段为代表，分别分析轨道板自振、列车轮载对结构疲劳特性的影响. 轨道板在L₀ = 0～6.0 L_a的条件下，阶段Ⅱ、Ⅲ疲劳寿命值、疲劳寿命影响系数及疲劳寿命总值如图6所示.

图 6 不同脱空长度下轨道板疲劳寿命值

Figure 6. Fatigue lifes of track slab with different de-bonding lengths

下载: 全尺寸图片幻灯片

图6表明，L₀越长，轨道板越容易发生疲劳损伤. 当L₀ > 4.7 L_a后，轨道板在1个列车组的作用下即发生疲劳破坏. 一般认为，无砟轨道的使用寿命是60 a，假定运营时每天作用100个列车组^[19]，则60 a内将有2.19 × 10⁶个列车组通过，对应于图6的L₀ = 3.2 L_a. 阶段Ⅱ的疲劳寿命受轨道板脱空长度影响较小，疲劳寿命大约维持在4.10 × 10¹³个作用组，当L₀ = 0时，阶段Ⅱ的疲劳损伤影响系数为0.378；当板底发生脱空后，随着板体自振频率降低，阶段Ⅱ的疲劳应力作用次数减小，故该阶段对疲劳寿命的影响程度减弱，此时阶段Ⅲ对应的疲劳作用总组数逐渐接近于疲劳寿命总值. L₀ = L_a时，阶段Ⅱ、Ⅲ的疲劳损伤影响系数分别为0.046、0.901；当L₀ > 2.0 L_a后，阶段Ⅱ的疲劳寿命影响系数趋于0，表明此时可按传统的仅考虑列车轮载作用次数的计数方法进行疲劳寿命预测. 因此，轨道板L₀ > 3.2 L_a后，现场无砟轨道难以维持60 a的使用寿命；当L₀ > 2.0 L_a后，可忽略列车轮载引发板体自振的效应对疲劳损伤的影响.

4. 结　论

1）轨道结构完好时，列车轮载引发轨道板伤损的可能性较小. 若列车行车速度为360 km/h，L₀ =6.2 L_a时，轨道板在单次轮对荷载作用下即达到轨道板的抗拉强度极限；L₀ =7.0 L_a时，列车轮载有引发轨道板共振的风险，表明列车轮载在引发轨道板共振前即发生板底开裂.

2）当L₀ > 4.7 L_a后，轨道板在1个列车组的作用下即发生疲劳破坏；L₀ > 3.2 L_a后，现场无砟轨道难以维持60 a的使用寿命.

3）轨道结构完好时，列车轮载引发的板体自振效应对轨道板疲劳损伤影响程度最大，此时在考虑板体自振后，列车轮载对轨道板产生约1.8倍的疲劳荷载当量；当L₀ > 2.0 L_a后，可忽略板体自振对疲劳损伤的影响.

参考文献(21)

MENEGUZZI F, TELANG P, SINGH M. A first-order formalization of commitments and goals for planning[C]//Proceedings of the Twenty-Seventh AAAI Conference on Artificial Intelligence. Bellevue: AAAI Press, 2013: 697-703.

MORITOMO A, HAMAGUCHI K, KASHIWABARA T. Validity checking for quantifier-free first-order logic with equality using substitution of boolean formulas[C]//International Symposium on Automated Technology for Verification and Analysis 2004, Lecture Notes in Computer Science. Berlin: Springer, 2004: 108-119.

BECKERT B, HAHNLE R. Reasoning and verification:state of the art and current trends[J]. IEEE Intelligent Systems, 2014, 29(1): 20-29. doi: 10.1109/MIS.2014.3

GRUNINGER M, HULL R, MCILRAITHS A. Short overview of flows: a first-order logic ontology for web services[C]//Bulletin of the IEEE Computer Society Technical Committee on Data Engineering. [S.l.]: IEEE, 2008: 3-7.

WITHERELL P, KRISHNAMURTY S, GROSSE I, et al. Improved knowledge management through first-order logic in engineering design ontologies[J]. Creativity:Simulation,Stimulation,and Studies, 2010, 24(2): 245-257.

WANG Zhenghao, YAN Shengquan, WANG Huaming, et al. An overview of Microsoft deep QA system on stanford web questions benchmark[R]. Washington D. C.: Microsoft, 2014.

HODER K, VORONKOV A. Sine qua non for large theory reasoning[C]//Automated Deduction-CADE-23. [S.l.]: CADE, 2011: 299-314.

ALAMA J, HESKES, T, KUHLWEIN D, et al. Premise selection for mathematics by corpus analysis and kernel methods[J]. Journal of Automated Reasoning, 2014, 52: 191-213. doi: 10.1007/s10817-013-9286-5

KHASIDASHVILI Z, KOROVIN K. Predicate elimination for preprocessing in first-order theorem proving[C]//International Conference on Theory and Applications of Satisfiability Testing, Lecture Notes in Computer Science. [S.l.]: SAT, 2016: 361-372.

KIESL B, SUDA M, SEIDL M. et al. Blocked clauses in first-order logic[C/OL]//Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21). [2018-09-20]. https://arxiv.org/pdf/1702. 00847.pdf.

NING Xinran, XU Yang; WU Guanfeng, et al. Set-blocked clause and extended set-blocked clause in first-order logic[J]. Symmetry, 2018, 10: 533-1-533-15.

BLOCKEEL H. Identifying non-redundant literals in clauses with uniqueness propagation[C]//The 26th International Conference on Inductive Logic Programming. [S.l.]: Springer, 2017: 8-13.

PIOTROWSKI P, URBAN J. ATPboost: learning premise selection in binary setting with ATP feedback[EB/OL]. [2018-2-15]. https://arxiv.org/abs/1802.03375?context=stat.

KUHLWEIN D, BLANCHETTE J. C. A survey of axiom selection as a machine learning problem[R]. Infinity, Computability and Metamathematics: Festschrift celebrating the 60th birthdays of Peter Koepke and Philip Welch. London: [s.n.], 2014.

陈青山,徐扬,何星星. 利用逻辑演绎求解SAT问题的启发式完全算法[J]. 西南交通大学学报,2017,52(6): 1224-1232. doi: 10.3969/j.issn.0258-2724.2017.06.025

CHEN Qingshan, XU Yang, HE Xingxing. Heuristic complete algorithm for SAT problem by using logical deduction[J]. Journal of Southwest Jiaotong University, 2017, 52(6): 1224-1232. doi: 10.3969/j.issn.0258-2724.2017.06.025

KIESL B, SUDA M. A unifying principle for clause elimination in first-order logic[C]//International Conference on Automated Deduction, Lecture Notes in Computer Science. [S.l.]: Springer, 2017: 274-290.

HEULE M J H, JARVISALO M, BIERE A. Covered clause elimination[C]//Short Papers for the 17th International Conference on Logic for Programming, Artificial intelligence, and Reasoning (LPAR-17-short). Yogyakarta: [s.n.], 2010, 13: 41-46.

HEULE M J H, JARVISALO M, BIERE A. Clause elimination procedures for CNF formulas[C]//Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17). [S.l.]: Springer, 2010: 357-371

JARVISALO M, HEULE M J H, BIERE A. Inprocessing rules[C]//International Joint Conference on Automated Reasoning. [S.l.]: Springer, 2012: 355-370

刘叙华. 基于归结方法的自动推理[M]. 北京: 科学出版社, 1994.

HEULE M J H, SEIDL M, BIERE A. Solution validation and extraction for QBF preprocessing[J]. Journal of Automated Reasoning, 2017, 58: 1-29. doi: 10.1007/s10817-016-9394-0

施引文献

附加材料(0)

访问统计

点击查看大图

计量

文章访问数: 583
HTML全文浏览量: 256
PDF下载量: 12
被引次数: 0

1. 计算模型与参数
2. 轨道板振动力学特性分析
2.1 振动受力分析
2.2 自振频率分析
3. 轨道板振动疲劳特性分析
3.1 疲劳寿命预测方法
3.2 脱空长度对疲劳特性影响
4. 结　论

一阶逻辑中的扩展子句消去原则

doi: 10.3969/j.issn.0258-2724.20180974

作者简介: 宁欣然（1990—），女，博士研究生，研究方向为自动推理、人工智能，E-mail：xinxinran@my.swjtu.edu.cn

计量

出版历程