一阶逻辑中基于稳定度的项评估方法  

Stability-based Term Evaluation Method in First-order Logic

作　　者：钟建 徐扬[2,3] 陈树伟[2,3] 何星星 ZHONG Jian;XU Yang;CHEN Shuwei;HE Xingxing(The School of Information Science and Technology,Southwest Jiaotong University,Chengdu 611756,China;National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,Southwest Jiaotong University,Chengdu 611756,China;School of Mathematics,Southwest Jiaotong University,Chengdu 611756,China)

机构地区：[1]西南交通大学信息科学与技术学院,成都611756 [2]西南交通大学系统可信性自动验证国家地方联合工程实验室,成都611756 [3]西南交通大学数学学院,成都611756

出　　处：《计算机工程》2019年第11期183-190,197,共9页Computer Engineering

基　　金：国家自然科学基金(61673320);中央高校基本科研业务费专项资金(2682018ZT10,2682018CX59)

摘　　要：针对一阶逻辑中项结构比较复杂、语法与语义特征难以抽取的问题,基于项在文字替换过程中的Herbrand语义特征,分析其制约因素和度量规则,给出项稳定度的定义并提出一种基于稳定度的项评估方法。将所提方法作为文字选择的启发式策略,应用于自动定理证明器中子句集的归入冗余判定中,结果表明,该方法能较好地刻画一阶逻辑中的项特征,与基于项序的文字选择方法相比,其检测次数平均减少50.8%,运行时间平均缩短53.3%。To address the complex term structure and difficult extraction of grammatical and semantic features in first-order logic,this paper analyzes the constraints and measurement rules of Herbrand semantic features of a term in text replacement.On this basis,the paper gives a definition of the stability of a term,and proposes a stability-based term evaluation method.As a heuristic strategy for text selection,this method is applied to the redundancy judgement of the clause set in Automated Theorem Prover(ATP).Results show that this method can better characterize the features of a term in first-order logic.Compared with the word selection method based on term order,its detection times are reduced by 50.8%on average,and its running time is shortened by 53.3%on average.

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

分 类 号：V221.3[航空宇航科学与技术—飞行器设计]