The synergized dynamic contradiction separation based automated deduction theory has provided a novel logic based automated deduction reasoning framework, which extends the static binary resolution inference rule to a dynamic multiple contradiction separation based automated deduction mechanism. This novel contradiction separation based automated deduction mechanism is characterized as a dynamic, multi-clauses involving, synergized, goal-oriented and robust automated reasoning framework. In order to further improve the efficiency and feasibility of this novel automated deduction mechanism, this paper proposes some strategies for clause or literal selection during the automated deduction process, which consider mainly the synergized effect of multi-clauses during the deduction process. Some examples are put forward to illustrate the feasibility of these proposed strategies.
|Title of host publication||Proceedings: 2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE)|
|Editors||Tianrui Li, Luis Martinez Lopez, Yun Li|
|Publisher||Institute of Electrical and Electronics Engineers Inc.|
|Number of pages||6|
|ISBN (Electronic)||978-1-5386-1829-5, 978-1-5386-1828-8|
|Publication status||Published (in print/issue) - 15 Jan 2018|
|Event||12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017 - NanJing, JiangSu, China|
Duration: 24 Nov 2017 → 26 Nov 2017
|Conference||12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017|
|Period||24/11/17 → 26/11/17|
Bibliographical noteFunding Information:
This work has been partially supported by the National Natural Science Foundation of China (Grant No. 61673320), and the Fundamental Research Funds for the Central Universities (Grant No. 2682017ZT12).
© 2017 IEEE.
- Automated reasoning
- Clause Selection
- Literal Selection