来源：期刊VIP网 时间：
作者：曹锋;郭海林;易见兵;李俊;吴贯锋;
单位：江西理工大学信息工程学院;西南交通大学数学学院;
摘要：基于二元归结的冲突演绎方法在每个演绎步骤只处理两个子句，其寻求冲突的演绎效率有待提升。提出了一种基于矛盾体分离的多元冲突演绎方法，给出了矛盾体分离多元冲突演绎的定义、学习子句的生成方法、演绎可靠性证明、演绎特点、演绎方法的优势分析以及虚子句的选取方法。在寻求冲突的演绎过程中，每个演绎步骤能处理多个子句，使演绎更容易产生冲突，更容易处理长子句，进而提升了冲突演绎的效率。实验结果表明，矛盾体分离多元冲突演绎方法具有较好的推理能力，比二元冲突演绎方法证明的定理更多，且定理证明所消耗的平均时间更少，加入矛盾体分离多元冲突演绎的Eprover证明器具有较好的搜索证明效率，能有效应用于一阶逻辑自动定理证明，解决难度等级较高的一阶逻辑问题。
关键词：二元归结;;冲突演绎;;矛盾体分离;;学习子句;;证明器
基金资助：国家自然科学基金（62366017,62066018,62106206）;; 江西省科技厅资助项目（20212ACB202003）;; 江西省教育厅资助项目（GJJ210828,GJJ200818,GJJ180482）
