.png){kind=icon}
返回
A complementary ratio based clause selection method for contradiction separation dynamic deduction
.png){kind=icon}
PRE
AI
DOI：10.1016/j.knosys.2023.111238.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
Automated reasoning is a key research area of Artificial Intelligence (AI) and has attracted much greater attention in recent years due to the demands of trustworthy AI, where binary resolution inference rule based firstorder automated reasoning play a crucial role. Recently, a novel multi-clause dynamic standard contradiction separation (S-CS) inference rule and related automated deduction theory were proposed to overcome the limitations of binary resolution-based automated deduction. Now that strategies for dynamic clause selection are essential for S-CS based automated deduction, in the present work, a class of novel clause selection strategies, along with the corresponding novel complementary ratio based dynamic S-CS automated deduction algorithm (called CRA), are proposed. Furthermore, we are interested in determining whether CRA may be deployed on top of the current best first-order automated reasoning system designs to increase their performance. As a result, CRA is applied to the current leading systems, Vampire and E, resulting in two integrated automatic reasoning systems, CRA_Vampire and CRA_E. Experiment results demonstrate that CRA can improve E and Vampire in CASC 2020-2022 competitions. The new integrated automated reasoning systems can resolve 44 problems with rating of 1, meaning they are intractable by other existing first-order automated systems.
Keyword:
Automated theorem proving
First order logic
Multi-clause dynamic synergized deduction
Clause selection
Heuristic strategy
期刊
K
IF:
7.6
论文数:
1.3W
被引数:
4.5W
机构
引用论文
.png){kind=icon}
An efficient contradiction separation based automated deduction algorithm for enhancing reasoning capability一种有效的基于矛盾分离的自动推理算法，可提高推理能力
OAAI
OAAI分享收藏
查看更多内容