【摘 要】
：
对于一阶逻辑定理证明器,子句集化简一直是必不可少的步骤,这将有助于提高后续一阶逻辑定理证明器的证明效率.针对子句冗余性的判断,提出了一种评估子句冗余性的原则:集合蕴
【机 构】
：
西南交通大学系统可信性自动验证国家地方联合工程实验室,西南交通大学信息科学与技术学院,西南交通大学数学学院
【基金项目】
：
国家自然科学基金(1673320),中央高校基本科研业务费专项资金(2682018ZT10)
论文部分内容阅读
对于一阶逻辑定理证明器,子句集化简一直是必不可少的步骤,这将有助于提高后续一阶逻辑定理证明器的证明效率.针对子句冗余性的判断,提出了一种评估子句冗余性的原则:集合蕴涵模归结原则.并且证明了该原则在不带等词一阶逻辑上的可靠性,根据该原则删除子句,不会影响原始子句集的不可满足性或者可满足性.此外,依据该原则提出了两种新型的一阶逻辑预处理方法:集合归结包含消去(set resolution subsumption,SRSE)方法和集合归结不对称恒真消去(set resolution asymmetric tau
其他文献
目前大学英语课堂教学和评价体系过于强调传授和评估学生的语言知识和形式，而利用多媒体网络交互式教学可以有效提高学生的听、说、读、写等语言综合运用能力，调动学生的学习兴
目的探讨乳腺腺病的磁共振影像学特点并分析误诊原因。方法回顾性分析经手术病理证实的20例乳腺腺病患者的MRI影像资料,随机选取同期经手术病理证实的20例乳腺癌病例作为对照
农民收入是西部少数民族地区农村摆脱贫困最为关键的一个指标.现阶段西部少数民族地区农民收入状况十分严峻,已经严重影响国内市场的扩大和农村的稳定.21世纪初,必须适当提高
在农村不断发展的过程中,对于电能的需求也在不断的提升,配电网运行中存在的安全问题在不断的凸显,这样在影响供电的同时也会影响到农村经济的发展和进步。因此,一定要采取有
形势与政策教育是高等学校学生思想政治教育的重要内容和途径。通过对影响形势与政策教育课教学实效性因素分析，从思想认识、推进思想政治理论课“05”改革方案、教师队伍建设
数字电视技术交互、高效等特性,将对现代远程教育产生积极影响.基于数字电视广播技术的实时教学系统,将有助于"形成开放式教育网络,构建终身学习体系",对于创建"学习型社会"