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

• 作者: 何星星 徐扬 钟建 陈树伟
• 来源期刊: 计算机工程
• 学科: 航空航天
• 关键词: 一阶逻辑 自动定理证明器 项评估 启发式策略 Herbrand语义特征
• 年，卷（期）: 2019,（11）
• 所属期刊栏目: 人工智能及识别技术
• 页码范围: 183-190,197
• 页数: 9页
• 分类号: V221.3
• 字数: 10636字
• 语种: 中文
• DOI: 10.19678/j.issn.1000-3428.0054368

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	徐扬	西南交通大学系统可信性自动验证国家地方联合工程实验室	186	1462	15.0	32.0
5	何星星	西南交通大学系统可信性自动验证国家地方联合工程实验室	12	35	3.0	5.0
9	钟建	西南交通大学信息科学与技术学院	2	0	0.0	0.0
13	陈树伟	西南交通大学系统可信性自动验证国家地方联合工程实验室	4	9	1.0	3.0