• ISSN 0258-2724
  • CN 51-1277/U
  • EI Compendex
  • Scopus 收录
  • 全国中文核心期刊
  • 中国科技论文统计源期刊
  • 中国科学引文数据库来源期刊

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

宁欣然 徐扬 何星星

赵婧昱, 张廷豪, 宋佳佳, 郭涛, 张宇轩, 邓军. 半封闭煤火演化过程的动力学特征[J]. 西南交通大学学报, 2023, 58(1): 117-124, 149. doi: 10.3969/j.issn.0258-2724.20210878
引用本文: 宁欣然, 徐扬, 何星星. 一阶逻辑中的扩展子句消去原则[J]. 西南交通大学学报, 2020, 55(3): 588-595. doi: 10.3969/j.issn.0258-2724.20180974
ZHAO Jingyu, ZHANG Tinghao, SONG Jiajia, GUO Tao, ZHANG Yuxuan, DENG Jun. Dynamic Characteristics for Evolution Process of Semi-closed Coal Fire[J]. Journal of Southwest Jiaotong University, 2023, 58(1): 117-124, 149. doi: 10.3969/j.issn.0258-2724.20210878
Citation: NING Xinran, XU Yang, HE Xingxing. Extended Unifying Principle of Clause Elimination in First-Order Logic[J]. Journal of Southwest Jiaotong University, 2020, 55(3): 588-595. doi: 10.3969/j.issn.0258-2724.20180974

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

doi: 10.3969/j.issn.0258-2724.20180974
基金项目: 国家自然科学基金(1673320);中央高校基本科研业务费专项资金(2682018ZT10)
详细信息
    作者简介:

    宁欣然(1990—),女,博士研究生,研究方向为自动推理、人工智能,E-mail:xinxinran@my.swjtu.edu.cn

  • 中图分类号: V221.3

Extended Unifying Principle of Clause Elimination in First-Order Logic

  • 摘要: 对于一阶逻辑定理证明器,子句集化简一直是必不可少的步骤,这将有助于提高后续一阶逻辑定理证明器的证明效率. 针对子句冗余性的判断,提出了一种评估子句冗余性的原则:集合蕴涵模归结原则. 并且证明了该原则在不带等词一阶逻辑上的可靠性,根据该原则删除子句,不会影响原始子句集的不可满足性或者可满足性. 此外,依据该原则提出了两种新型的一阶逻辑预处理方法:集合归结包含消去(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方法更为有效.

     

  • 无论堆煤还是采区遗煤在开采、运输和储存过程中均以颗粒状的松散煤体形式存在. 松散煤体自燃对空气质量、地表植被、地质条件造成了不同程度的影响[1-3],同时粉尘、CO和SO2等有毒有害气体会伴随着煤体自燃大量涌入大气中,造成区域性空气污染,危害人体健康[4-9],并且外界环境(如辐射、大气环境等)和内在因素(如煤体水分含量、粒径等)会对松散煤体的自燃特性造成影响[10-11]. 国内外学者对煤体自燃氧气浓度的演化进行了大量的研究.

    目前,学者们多采用有限元[12]、回归模型[13]等方法对煤自燃温度场的模型进行组建与计算. 赵婧昱等[14-16]模拟松散煤体从常温到着火全过程,得出高温点首先出现在低氧浓度分布区,确定了高温氧化过程中的危险阶段为干裂—活性—增速温度阶段. 张九零等[17-18]模拟了火区自燃蔓延时温度场、一氧化碳浓度和速度场的分布情况,确定了露头自燃点下风侧方向是生成气体的主要集中区域. 此外,学者们还研究了煤体在不同热源温度[19]、粒度[20]、有效孔隙[21]等条件下氧气运移的规律特征. 郭兴明等[22-24]假设煤体为均匀介质,建立了氧气在松散煤体中扩散过程的数学模型;邓军等[25-26]对煤体自燃过程中的耗氧速率进行了理论分析,推导出了低温氧化阶段耗氧速率的量化模型;谭波等[27]基于煤自燃参数对煤自燃的影响分析,建立了煤自燃中温度场的数学模型并进行求解计算,得到了煤自燃数学一维模型.

    由于煤自燃现场研究难度较大,研究人员多建立圆柱形煤火发生实验炉,进行煤自燃的传质、传热过程研究. 研究装置多为程序升温系统,持续进行热源和氧气供给,以维持良好的蓄热环境,但对于自然状态下煤火区域氧气与温度相互作用的效应探索较少. 由于煤体内非等温的温度场导致与外界产生热力压差,致使氧气通过裂隙渗入煤体,维持自燃反应,释放热能,推动高温区域向深部发展,致使燃烧愈加剧烈. 当煤体温度到达一定程度,松散煤体内部的氧浓度逐渐下降至极限氧浓度以下,开始形成煤体需氧量大而氧气浓度低的热环境,煤体开始主动吸附游离在空气中的氧气分子,此时存在煤体表面对氧气进行竞争状态,本文将这个竞争过程称为“煤体自然吸氧效应”. 在此基础上,采用自主研发的半封闭煤火演化实验系统,在自然通风的条件下,分析松散煤体自燃过程中的氧气及温度阶段性演化规律,从而建立高温贫氧条件下煤自燃耗氧速率的量化模型,并揭示其内在联系规律. 研究成果对开采、运输、储存状态下的松散煤体自然发火的防治提供理论基础.

    本实验采用自主搭建半封闭煤火演化实验系统,模拟“自然吸氧效应”,不进行人为主动供氧,热源引燃煤体首层后,测试下五层煤体的自燃特征.

    半封闭煤火演化实验系统包括以下装置:炉体、温度控制和监测平台、气体分析装置以及污染物处理装置等(如图1所示). 实验炉体由耐高温纯纤维毯和碳钢材料压制组成,炉体整体为圆柱体,外部尺寸:半径300 mm × 高730 mm,炉膛内部尺寸:半径150 mm × 高600 mm,侧壁保温层厚度为150 mm,保温层由耐火砖和纤维的混合结构组成. 炉体顶部安装易于控制升温速率的不锈钢加热棒,直径14 mm,功率500 W,额定电压380 V,最大受热温度1100 ℃. 炉壁布置有直径为16 mm的通孔作为温度数据采集点和气体采集点,测温单元与温度记录仪装置连接,采用气相色谱仪对所采集的气体进行测试. 实验炉体顶部设有防潮盖,实验时,防潮盖为常开状态,保证实验为半封闭状态. 炉体为圆柱形设计,这里将横截面圆心位置来表征整个截面的温度变化,测温单元与测气单元布置于煤体正中心位置从上至下共五层;为反映煤体在燃烧过程中横向变化特征,在第三层的位置横向布置3个测点(如图2所示),中心位置5个测点从上至下分别编号为PTC1PTC5,第三层两侧测点分别编号为PTC6PTC7.

    图  1  实验系统
    Figure  1.  Experimental system
    图  2  半封闭煤火发展演化模拟实验装置
    Figure  2.  Device for simulating semi-closed coal fire evolution

    半封闭煤火演化实验在常温、常压下完成. 煤样采自陕西孟村煤矿,从工作面采取后使用布袋密封运送至实验室,使用鄂式破碎机完成破碎,为模拟开采后煤堆粒径尺寸[28],破碎的煤样粒径约为10 mm,实验条件、煤质分析分别如表12所示. 表中:Mad为水分含量;Aad为灰分产率;Vad为挥发分产率;FCad为固定碳含量.

    表  1  实验条件
    Table  1.  Experimental conditions
    项目煤样粒径/mm室温/℃湿度/%煤高/mm装煤量/kg
    参数孟村1066848057.7
    下载: 导出CSV 
    | 显示表格
    表  2  煤质分析
    Table  2.  Coal quality analysis %
    工业分析元素成分分析
    MadAadVadFCadCHONS
    4.414.033.548.078.84.714.21.30.8
    下载: 导出CSV 
    | 显示表格

    该实验无外部气源,通过实验装置留设的通孔布置测温热电偶、采气铜管和加热单元. 对煤体表面进行人为加热,主动提供火源,当顶层煤样开始出现明火时停止加热,之后松散煤体自发燃烧. 实验时采气间隔为1.0 h,当某层温度达到燃点温度,便改变该层采气间隔为2.0 h,所有煤层均达到燃点温度后,改变所有煤层采气间隔为4.0 h,当采集点裸露在空气中或最底层煤体温度达到室温后,不再采集气体.

    通过热重分析法,确定了实验煤样自燃的特征温度. 样品粒径为80~120目,质量为5 mg,温度范围30.0~800.0 ℃,升温速率为5 ℃/min.

    松散煤体在燃烧过程中各测点氧气浓度变化情况如图3所示. 因首层煤样距空气位置较近,煤样反应发生较强,实验开始时,该层煤样相比于其他煤样氧气浓度低5.0%~10.0%. 推测实验初期上层煤样与空气接触面积较大,空气中游离的氧分子充足,更易于被煤体吸附,从而发生煤体“自然吸氧”反应,促使煤体温度升高. 将煤体主动吸收氧气的难易程度称为煤体“自然吸氧强度”. 实验进行至3.0 h后,各层煤样测点处煤体“自然吸氧强度”增高,氧气浓度下降速率开始加快,上层煤样几乎呈直线下降. 3.0 h时第二层测点氧气浓度下降至7.5%~10.0%,与实验初期首层煤样氧气浓度相似. 6.5 h后,首层煤样氧气浓度下降至1.0 %~3.0%,此为火区煤贫氧燃烧的极限氧浓度,此时煤体表面开始出现明火现象,燃烧开始,其后该测点氧气浓度基本保持不变. 7.0 h时第二层煤样测点处氧气浓度也下降至极限氧浓度. 总体来看,各层煤样测点变化趋势基本相似,但由于纵深变化的影响,实验初期,相较于上层煤样,底层煤样与空气接触面积较小,空气不易于流动,其“自然吸氧强度”也就弱于上层煤样,表现形式为氧气浓度开始下降时间的逐渐延后. 而此时,其他三层氧气浓度仍处于较高水平,直至14.0 h后,均下降至极限氧浓度以下.

    图  3  氧气浓度变化与时间关系曲线
    Figure  3.  Curves of oxygen concentration versus time

    在实验进行至4.0 h时,可以观察到第三层煤样3个测点之间氧气浓度下降程度略有不同,且在9.5 h后,第四层测点氧气浓度低于第三层. 推测因煤体自身裂隙发育的影响,使得该区域煤体与空气接触面积呈现出不同情况. 裂隙为氧气的扩散提供了通风线路,促进了其向裂隙扩展方向运移,从而导致同层不同测点之间氧气浓度下降程度的不均衡现象. 故煤体“自然吸氧强度”受氧气浓度、煤层高度、煤体温度及孔隙率共同影响.

    基于Krishnawamy等[29]提出的煤的动力学反应扩散模型求解煤在低氧浓度(氧气浓度小于3.0 %)下自燃时的自然吸氧强度. 假设高温低氧浓度区域是由相同粒径的煤颗粒所组成的,因此,自燃区域的耗氧速率即为煤颗粒的自然吸氧强度. 该区域的耗氧速率即为单位时间内煤体所消耗的氧气浓度,而在低氧浓度环境下煤体所消耗的氧气浓度等于单位时间内所供给的氧气浓度,推导得出自然吸氧强度为

    (1)

    式中:r为自然吸氧强度,mol/(m3·s);η为效率因子;k为质量传输速率,kg/s;Sr为自燃区域底面积,m2ε为煤体的孔隙率,%;Vr为燃烧区的体积,m3C为外部环境中氧气浓度,mol/m3C1为煤体中的氧气浓度,mol/m3.

    由于在高温阶段煤体中的水分已经蒸发殆尽,煤体中的水分不会对氧气的供给产生影响,则其效率因子接近于1,可将该项忽略. 自燃曲的体积与表面积的关系可以化简为

    (2)

    式中: H为自燃区域高度,m.

    质量传输速率k可以根据舍伍德数求出,由半经验公式可得

    (3)

    式中:Sh为舍伍德数,无量纲,通常取0.3;d为煤粒粒径,m.

    式(1)可简化为

    (4)

    式中:D0为热扩散系数,m2/s.

    煤样不同测点的自然吸氧强度随时间变化曲线如图4所示. 由图4可知:自然吸氧强度与氧气浓度变化相反,当氧气浓度下降时,自然吸氧强度逐渐上升;火区低阶煤贫氧燃烧的极限氧浓度为1.0%~3.0%,当氧浓度小于极限氧浓度后,即高温燃烧过程将出现热解进程,此时自然吸氧强度趋于平缓;煤样同层不同测点自然吸氧强度变化规律近似于抛物线形式,第一、二层煤样在3.0 h前自然吸氧强度变化平稳,在3.0~6.5 h急剧提升,6.5 h后又趋于平稳;第三层煤样趋势稍缓,实验15.0 h后趋于平缓;第四、五层深煤样自然吸氧强度变化最慢,在整个阶段呈线性变化,这种现象取决于煤层深度的不同;纵向来看,由于氧气浓度、温度与煤体传热特征等原因,自然吸氧强度随深度的增加逐渐减小;同样地,同层煤样不同测点之间自然吸氧强度变化趋势也基本满足自然吸氧强度与氧气浓度变化相反.

    图  4  自然吸氧强度变化与时间关系曲线
    Figure  4.  Curves of natural absorption oxygen intensity versus time

    松散煤体在堆放、运输、储存过程中主要以自然通风为主,氧气供给充足,当温度达到一定条件之后容易发生自燃反应. 自燃开始形成后,燃烧便会由浅部向深部逐步发展,并不断向深部运移,同时内部环境与外部环境形成热力压差,促进煤体主动吸氧,使得游离在空气中的氧气分子被吸附于煤体内部,维持燃烧的进行. 松散煤体为多孔介质,各部位的传热是传导、辐射、对流共存的综合传热过程,属于不稳定传热. 随着自燃深度的加深,煤氧化学反应不断加剧,蓄热能力增强,传热作用显著增加,裂隙变化,温度发生变动.

    由氧气浓度变化可看出,煤体自燃拥有阶段性变化特征,为了更好地对温度运移与耗氧特征进行分析,选取热重曲线特征温度点[15],根据特征温度对氧化自燃过程进行分阶段划分. 图5为实验煤样的热重(thermal gravity,TG)曲线及导数热重(derivative thermogravimetry,DTG)曲线,T1为吸氧增重起始温度点,此温度点之前为缓慢氧化阶段. T2为吸氧增重最大温度点,T1T2为快速升温阶段. 吸氧增重最大温度点之后,煤氧化自燃开始从缓慢氧化阶段到高温自燃阶段过渡,煤氧反应更加剧烈,经历分界点着火点温度(T3)后,质量迅速下降,并达到DTG曲线谷值上的点T4 (最大失重速率的温度点),此后达到燃尽温度点(T5),煤体温度超过燃尽温度后,进入高温自燃阶段. 煤样3个不同氧化自燃阶段温度范围如表3所示.

    图  5  在空气气氛下的TG及DTG曲线
    Figure  5.  TG and DTG curves in air atmosphere
    表  3  不同氧化自燃阶段温度划分
    Table  3.  Temperature levels in oxidized spontaneous combustion
    阶段氧化自燃阶段平均温度范围/℃
    第一阶段缓慢氧化阶段 0~111.0
    第二阶段快速升温阶段112.0~303.0
    第三阶段高温自燃阶段304.0~604.0
    下载: 导出CSV 
    | 显示表格

    第2节分析了从实验开始至煤体发生燃烧各层测点氧气浓度的变化趋势,而氧气是燃烧必不可少的反应物,氧气浓度的阶段性变化必然会引起温度的阶段性变化. 故本节对各层测点间温度变化趋势进行分析.

    煤自燃在纵向发展过程中,随测点深度加深温度逐渐降低,达到最高温度点的时间依次延长. 测点各阶段的时间与温度如表4所示. 由图4表4可知:第一层煤体在实验4.5 h左右达到121.0 ℃,随着实验的进行,温度逐渐向下传播,其余各层进入缓慢氧化阶段时间依次延后,第二层到第五层依次为12.0、14.0、19.5、32.5 h;其后,各测点温度上升速率逐渐加快,直至6.5 h时,首层煤样温度达到316.0 ℃,煤体表面出现明火现象,燃烧开始. 对于同测点温度变化时间要比氧气浓度变化时间相对延后,可证明氧气浓度的变化要先于温度的变化,在煤体自然过程中,氧气的变化为先决条件,煤体的“自然吸氧”效应使得游离在空气中的氧分子吸附于煤体之中,为自燃提供条件. 在氧气吸附的过程中,煤体温度逐渐升高,从而促使煤体“自然吸氧强度”增高,加快氧气的吸附,直到达到燃点,氧气浓度不再发生改变,于是可得出温度变化时间对氧气浓度变化时间具有一定的滞后性,而其滞后时间主要受煤层高度影响.

    表  4  纵向测点到达各阶段的时间与温度
    Table  4.  Time and temperature of longitudinal measuring points at each phase
    阶段 PTC1 PTC2 PTC3 PTC4 PTC5
    时段/h 温度/℃ 时段/h 温度/℃ 时段/h 温度/℃ 时段/h 温度/℃ 时段/h 温度/℃
    第一阶段 0~4.5 121.0 0~12.0 132.0 0~14.0 120.0 0~19.5 115.0 0~32.5 121.0
    第二阶段 4.5~6.5 316.0 12.0~13.5 314.0 14.0~16.0 308.0 19.5~21.0 301.0 23.5~48.0 302.0
    第三阶段 6.5~23.0 602.0 13.5~24.0 598.0 16.0~48.0 577.0 21.0~43.0 492.0 48.0~73.0 476.0
    下载: 导出CSV 
    | 显示表格

    所有测点处温度处于快速升温阶段的时间远小于缓慢氧化阶段,推测煤体“自然吸氧强度”使得氧气吸附在煤体的速率加快,由此可证明,氧气的变化引起温度的变化.

    煤体纵向5个测点温度随时间变化曲线如图6所示,选取实验前24.0 h数据,温度变化与测点到煤体表面直线距离的关系曲线如图7所示. 由图可知:第一层煤体温度前24.0 h内均处于最高水平,这是由于其距表层最近,氧气浓度充足,同时距离加热层最近造成的;PTC2PTC4的温度变化较快,曲线表现出从第6.0、12.0 h的凹状变为24.0 h的凸状;而第五层由于距离表层最远初始氧气浓度较低,且温度传播需要时间,所以其温度在前24.0 h内始终处于最低水平.

    图  6  纵向温度变化与时间关系
    Figure  6.  Relationship between longitudinal temperature change and time

    对温度随测点距煤体表面距离的变化曲线进行回归分析,得出温度与距离之间的关系为

    (5)

    式中:t为温度,℃;l为距煤体表面距离,mm;A、B、C为回归方程系数;D为回归方程截距.

    煤样所有测点虽距离煤体表面距离的不同,但温度变化曲线拟合均符合该回归方程,相关系数R2值均在0.9800左右,表现较好的相关性. 由此可知,煤体内部温度传播受纵深影响较大,深度越大,温度传播越慢,温度变化趋势越低. 同时做其温升速率变化如图8所示,可以看出随着深度的增加,各层测点温升速率达到峰值时间逐渐后移,峰值速率也逐渐降低,由此反向证明了拟合回归方程的正确性.

    图  7  温度变化与距离关系
    Figure  7.  Relationship between temperature change and distance
    图  8  温升速率随时间变化曲线
    Figure  8.  Curves of temperature rising rate over time

    实验样本中第三层煤样3个测点的变化能够较为准确地反映整个实验的变化特征. 如图9所示,同层煤的不同测点展示出相同的变化规律. 由图可知:实验煤样同层测点的温度增长趋势一致,但到达各阶段的时间不同;PTC6经过13.0 h升至111.2 ℃,最先进入第二阶段,经15.0 h率先超过燃点温度达到312.2 ℃;PTC7温度变化慢于PTC3PTC6,但实验48.0 h后,PTC7的温度下降速度最快,说明此测点氧气浓度较弱;312.0 h后,3个测点均处于低温状态. 煤体孔隙结构的变化能够直接影响氧气的吸附与渗流. 松散煤体为非均匀介质,在燃烧过程中由于温度的升高,煤体内部产生不规则裂隙,致使氧气随裂隙进入煤体内,从而促使燃烧加剧,且不同测点位置孔隙结构有所差异,同层煤不同测点的温度变化情况也因此各不相同.

    图  9  温度变化与时间关系
    Figure  9.  Relationship between temperature change and time

    1) 通过对氧气浓度与温度迁移数据的分析可以表明煤火发展演化模拟实验装置能够较好地模拟和再现煤自燃“自然吸氧”过程.

    2) 煤体自身“自然吸氧效应”为其燃烧提供动力,促使煤体内部氧气浓度发生改变. 随着煤层纵深的增加,氧气浓度下降开始时间逐渐增加,“自然吸氧强度”随也不断减弱.

    实验过程中,氧气浓度的变化是温度变化的前提条件,温度变化时间滞后于氧气浓度变化,其滞后时间差随煤层纵深变化的增加而增加. 在水平方向上高温区域迁移趋势主要受煤体内部裂隙与孔隙分布的影响.

    致谢:西安科技大学优秀青年科技基金项目(2020YQ3-02).

  • 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
  • 期刊类型引用(2)

    1. 吴玉娇,任叶飞,肖裴渊,刘也,冀昆,温瑞智. 考虑近场、中远场区域性差异的地震动工程输入适用性研究. 震灾防御技术. 2024(04): 685-697 . 百度学术
    2. 雷虎军,黄江泽. 考虑桩土相互作用的车-轨-桥系统地震响应分析. 西南交通大学学报. 2021(02): 229-237 . 本站查看

    其他类型引用(15)

  • 加载中
计量
  • 文章访问数:  577
  • HTML全文浏览量:  254
  • PDF下载量:  12
  • 被引次数: 17
出版历程
  • 收稿日期:  2018-11-27
  • 修回日期:  2019-06-18
  • 网络出版日期:  2020-03-30
  • 刊出日期:  2020-06-01

目录

/

返回文章
返回