10.19678/j.issn.1000-3428.0054368
一阶逻辑中基于稳定度的项评估方法
针对一阶逻辑中项结构比较复杂、语法与语义特征难以抽取的问题,基于项在文字替换过程中的Herbrand语义特征,分析其制约因素和度量规则,给出项稳定度的定义并提出一种基于稳定度的项评估方法.将所提方法作为文字选择的启发式策略,应用于自动定理证明器中子句集的归入冗余判定中,结果表明,该方法能较好地刻画一阶逻辑中的项特征,与基于项序的文字选择方法相比,其检测次数平均减少50.8%,运行时间平均缩短53.3%.
一阶逻辑、自动定理证明器、项评估、启发式策略、Herbrand语义特征
45
V221.3(飞机构造与设计)
国家自然科学基金61673320;中央高校基本科研业务费专项资金2682018ZT10,2682018CX59
2019-12-05(万方平台首次上网日期,不代表论文的发表时间)
共9页
183-190,197