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

论文摘要

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

论文目录

• 0 概述
• 1 相关知识
• 2 项的稳定度
•   2.1 单因素分析
•     2.1.1 变元项数和基项数对项稳定度的影响
•     2.1.2 变元函数嵌套深度对项稳定度的影响
•     2.1.3 函数元数对项稳定度的影响
•   2.2 项稳定度计算
•   2.3 项关联度计算
•   2.4 项稳定度计算的改进与实现
• 3 实验结果与分析
• 4 结束语

文章来源

类型: 期刊论文

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

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

来源: 计算机工程 2019年11期

年度: 2019

分类: 信息科技

专业: 计算机软件及计算机应用

单位: 西南交通大学信息科学与技术学院,西南交通大学系统可信性自动验证国家地方联合工程实验室,西南交通大学数学学院

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

分类号: TP391.1

DOI: 10.19678/j.issn.1000-3428.0054368

页码: 183-190+197

总页数: 9

文件大小: 549K

下载量: 50