来源：期刊VIP网 时间：
作者：曹锋;徐梓伟;易见兵;李俊;
单位：江西理工大学信息工程学院;
摘要：针对多元演绎如何有效选取子句，通过分析演绎前后项合一能力的变化，提出一种子句影响度的度量方法；通过分析子句影响度、剩余文字个数以及文字演绎能力对多元动态演绎过程的影响，提出一种子句综合权重的子句评估方法，能有效控制矛盾体分离式的文字个数；基于该子句评估方法，提出一种有效选择子句的多元动态演绎算法。将该算法应用到国际顶尖的一阶逻辑自动定理证明器Eprover3.1中，以最新的国际自动定理证明器竞赛例（FOF组）为测试对象，测试结果表明，加入了本文多元动态演绎算法的Eprover3.1比原始Eprover3.1多证明定理18个，且在难问题判定上，证明了8个其他证明器未能证明的定理。
关键词：多元演绎;;子句评估;;矛盾体分离式;;一阶逻辑;;自动定理证明器
基金资助：国家自然科学基金（62366017、62066018）;; 江西省教育厅项目（GJJ200818、GJJ210828）;; 赣州市科技计划项目（GZKJ20206030）;; 江西理工大学博士启动基金（205200100060）
