作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2019, Vol. 45 ›› Issue (11): 183-190,197. doi: 10.19678/j.issn.1000-3428.0054368

• 人工智能及识别技术 • 上一篇    下一篇

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

钟建a,b, 徐扬b,c, 陈树伟b,c, 何星星b,c   

  1. 西南交通大学 a. 信息科学与技术学院;b. 系统可信性自动验证国家地方联合工程实验室;c. 数学学院, 成都 611756
  • 收稿日期:2019-03-25 修回日期:2019-06-09 发布日期:2019-06-22
  • 作者简介:钟建(1980-),男,博士研究生,主研方向为智能信息处理、自动推理;徐扬,教授、博士生导师;陈树伟、何星星,副教授、博士。
  • 基金资助:
    国家自然科学基金(61673320);中央高校基本科研业务费专项资金(2682018ZT10,2682018CX59)。

Stability-based Term Evaluation Method in First-order Logic

ZHONG Jiana,b, XU Yangb,c, CHEN Shuweib,c, HE Xingxingb,c   

  1. a. The School of Information Science and Technology;b. National-Local Joint Engineering Laboratory of System Credibility Automatic Verification;c. School of Mathematics, Southwest Jiaotong University, Chengdu 611756, China
  • Received:2019-03-25 Revised:2019-06-09 Published:2019-06-22

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

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

Abstract: 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.

Key words: first-order logic, Automated Theorem Prover(ATP), term evaluation, heuristic strategy, Herbrand semantic features

中图分类号: