计算机工程

作者：钟建, 徐扬, 陈树伟, 何星星

单位：西南交通大学 a. 信息科学与技术学院;b. 系统可信性自动验证国家地方联合工程实验室;c. 数学学院, 成都 611756

关键词：一阶逻辑,自动定理证明器,项评估,启发式策略,Herbrand语义特征

基金：国家自然科学基金（61673320）；中央高校基本科研业务费专项资金（2682018ZT10，2682018CX59）。

针对一阶逻辑中项结构比较复杂、语法与语义特征难以抽取的问题，基于项在文字替换过程中的Herbrand语义特征，分析其制约因素和度量规则，给出项稳定度的定义并提出一种基于稳定度的项评估方法。将所提方法作为文字选择的启发式策略，应用于自动定理证明器中子句集的归入冗余判定中，结果表明，该方法能较好地刻画一阶逻辑中的项特征，与基于项序的文字选择方法相比，其检测次数平均减少50.8%，运行时间平均缩短53.3%。

来源：2019年第11期

《计算机工程》期刊编辑部

查看计算机工程杂志2019年第11期