-
题名基于子句活跃度和复杂度的多元动态演绎算法及应用
- 1
-
-
作者
林玲瑜
曹锋
易见兵
方旺盛
李俊
吴贯锋
-
机构
江西理工大学信息工程学院
西南交通大学数学学院
-
出处
《计算机工程与科学》
CSCD
北大核心
2023年第12期2256-2264,共9页
-
基金
国家自然科学基金(62066018,62106206)
江西省科技厅项目(20212ACB202003)
+1 种基金
江西省教育厅项目(GJJ200818,GJJ180482)
江西理工大学博士启动基金(205200100060)。
-
文摘
一阶逻辑自动定理证明是知识表示与自动推理领域重要的研究内容,如何有效选取子句参与演绎是提升自动推理能力和效率的研究热点。基于多元动态演绎良好的演绎特性,通过分析子句的变元项性质和函数项结构,提出了一种子句活跃度和复杂度的度量与计算方法,能很好地对不同项结构的子句进行有效评估;基于该子句评估方法,提出了一种子句充分协同演绎的多元动态演绎算法,能有效优化多元演绎搜索路径。将该多元动态演绎算法应用于国际顶尖证明器Eprover 2.6中,以2021年国际自动推理FOF组竞赛例为测试对象,在标准的300 s测试时间内,加入了多元动态演绎算法的Eprover 2.6相比原始Eprover 2.6多证明定理4个,在证明定理总数相同的条件下,平均证明时间减少了1.12 s;能证明Eprover 2.6未证明定理16个,占未证明定理总数的15.1%。实验结果表明,该多元动态演绎算法是一种有效的推理方法,能在一定程度上提升自动定理的证明能力和时间效率。
-
关键词
一阶逻辑
定理证明
自动推理
多元动态演绎
子句评估
-
Keywords
first-order logic
theorem proving
automated reasoning
multi-clause dynamic deduction
clause evaluation
-
分类号
TP311.1
[自动化与计算机技术—计算机软件与理论]
-