摘要： 针对一阶逻辑中项结构比较复杂、语法与语义特征难以抽取的问题，基于项在文字替换过程中的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

中图分类号: 

• V221.3