Some synergized clause selection strategies for contradiction separation based automated deduction

Shuwei Chen; Yang Xu; Yan Jiang; Jun Liu; Xingxing He

doi:10.1109/ISKE.2017.8258741

Some synergized clause selection strategies for contradiction separation based automated deduction

Shuwei Chen, Yang Xu, Yan Jiang, Jun Liu, Xingxing He

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

3 Citations (Scopus)

Abstract

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.

Original language	English
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.
Pages	1-6
Number of pages	6
ISBN (Electronic)	978-1-5386-1829-5, 978-1-5386-1828-8
ISBN (Print)	978-1-5386-1830-1
DOIs	https://doi.org/10.1109/ISKE.2017.8258741
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

Conference	12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017
Country/Territory	China
City	NanJing, JiangSu
Period	24/11/17 → 26/11/17

Bibliographical note

Funding 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).

Publisher Copyright:
© 2017 IEEE.

Keywords

Automated reasoning
Clause Selection
Literal Selection
Logic
Resolution

Access to Document

10.1109/ISKE.2017.8258741

Cite this

Chen, S., Xu, Y., Jiang, Y., Liu, J., & He, X. (2018). Some synergized clause selection strategies for contradiction separation based automated deduction. In T. Li, L. M. Lopez, & Y. Li (Eds.), Proceedings: 2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE) (pp. 1-6). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ISKE.2017.8258741

Chen, Shuwei ; Xu, Yang ; Jiang, Yan et al. / Some synergized clause selection strategies for contradiction separation based automated deduction. Proceedings: 2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE). editor / Tianrui Li ; Luis Martinez Lopez ; Yun Li. Institute of Electrical and Electronics Engineers Inc., 2018. pp. 1-6

@inproceedings{ed90833386e24a2aab0cf31422dfe934,

title = "Some synergized clause selection strategies for contradiction separation based automated deduction",

abstract = "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.",

keywords = "Automated reasoning, Clause Selection, Literal Selection, Logic, Resolution",

author = "Shuwei Chen and Yang Xu and Yan Jiang and Jun Liu and Xingxing He",

note = "Funding 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). Publisher Copyright: {\textcopyright} 2017 IEEE.; 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017 ; Conference date: 24-11-2017 Through 26-11-2017",

year = "2018",

month = jan,

day = "15",

doi = "10.1109/ISKE.2017.8258741",

language = "English",

isbn = "978-1-5386-1830-1",

pages = "1--6",

editor = "Tianrui Li and Lopez, {Luis Martinez} and Yun Li",

booktitle = "Proceedings: 2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE)",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

address = "United States",

}

Chen, S, Xu, Y, Jiang, Y, Liu, J & He, X 2018, Some synergized clause selection strategies for contradiction separation based automated deduction. in T Li, LM Lopez & Y Li (eds), Proceedings: 2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE). Institute of Electrical and Electronics Engineers Inc., pp. 1-6, 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017, NanJing, JiangSu, China, 24/11/17. https://doi.org/10.1109/ISKE.2017.8258741

Some synergized clause selection strategies for contradiction separation based automated deduction. / Chen, Shuwei; Xu, Yang; Jiang, Yan et al.
Proceedings: 2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE). ed. / Tianrui Li; Luis Martinez Lopez; Yun Li. Institute of Electrical and Electronics Engineers Inc., 2018. p. 1-6.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Some synergized clause selection strategies for contradiction separation based automated deduction

AU - Chen, Shuwei

AU - Xu, Yang

AU - Jiang, Yan

AU - Liu, Jun

AU - He, Xingxing

N1 - Funding 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). Publisher Copyright: © 2017 IEEE.

PY - 2018/1/15

Y1 - 2018/1/15

N2 - 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.

AB - 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.

KW - Automated reasoning

KW - Clause Selection

KW - Literal Selection

KW - Logic

KW - Resolution

UR - http://www.scopus.com/inward/record.url?scp=85048116535&partnerID=8YFLogxK

U2 - 10.1109/ISKE.2017.8258741

DO - 10.1109/ISKE.2017.8258741

M3 - Conference contribution

AN - SCOPUS:85048116535

SN - 978-1-5386-1830-1

SP - 1

EP - 6

BT - Proceedings: 2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE)

A2 - Li, Tianrui

A2 - Lopez, Luis Martinez

A2 - Li, Yun

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017

Y2 - 24 November 2017 through 26 November 2017

ER -

Chen S, Xu Y, Jiang Y, Liu J, He X. Some synergized clause selection strategies for contradiction separation based automated deduction. In Li T, Lopez LM, Li Y, editors, Proceedings: 2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE). Institute of Electrical and Electronics Engineers Inc. 2018. p. 1-6 doi: 10.1109/ISKE.2017.8258741

Some synergized clause selection strategies for contradiction separation based automated deduction

Abstract

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this