一阶逻辑中的扩展子句消去原则

• 作者: 何星星 宁欣然 徐扬
• 来源期刊: 西南交通大学学报
• 学科: 航空航天
• 关键词: 集合蕴涵模归结 一阶逻辑 蕴涵模归结 子句消去方法 预处理方法
• 年，卷（期）: 2020,（3）
• 页码范围: 588-595
• 页数: 8页
• 分类号: V221.3
• 字数: 10197字
• 语种: 中文
• DOI: 10.3969/j.issn.0258-2724.20180974

摘要

对于一阶逻辑定理证明器,子句集化简一直是必不可少的步骤,这将有助于提高后续一阶逻辑定理证明器的证明效率.针对子句冗余性的判断,提出了一种评估子句冗余性的原则:集合蕴涵模归结原则.并且证明了该原则在不带等词一阶逻辑上的可靠性,根据该原则删除子句,不会影响原始子句集的不可满足性或者可满足性.此外,依据该原则提出了两种新型的一阶逻辑预处理方法:集合归结包含消去(set resolution subsumption,SRSE)方法和集合归结不对称恒真消去(set resolution asymmetric tautology elimination,SRATE)方法,并证明了这两种子句消去方法在不带等词一阶逻辑子句集上的可靠性.最后在理论上比较了SRSE方法和归结包含消去(sesolution subsumption elimination,RSE)方法以及SRATE方法和归结不对称恒真(sesolution asymmetric tautology elimination,RATE)方法之间的有效性,结果表明SRSE方法和SRATE方法分别比RSE方法和RATE方法更为有效.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	徐扬	西南交通大学系统可信性自动验证国家地方联合工程实验室	186	1462	15.0	32.0
5	宁欣然	西南交通大学系统可信性自动验证国家地方联合工程实验室	6	6	2.0	2.0
9	何星星	西南交通大学系统可信性自动验证国家地方联合工程实验室	12	35	3.0	5.0