Multi-clause synergized contradiction separation based first-order theorem prover-MC-SCS

Jian Zhong; Feng Cao; Guanfeng Wu; Yang Xu; Jun Liu

doi:10.1109/ISKE.2017.8258793

Multi-clause synergized contradiction separation based first-order theorem prover-MC-SCS

Jian Zhong, Feng Cao, Guanfeng Wu, Yang Xu, Jun Liu

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

3 Citations (Scopus)

Abstract

After extending the term 'contradiction' from the traditionally defined a complementary pair based on two clauses into a typical unsatisfiable clause set (i.e., a standard contradiction which might consist of more than two clauses), a recent work by the same author group proposes a new inference principle and its sound and complete first-order theory framework to escape from the existing static binary resolution into a dynamic Multi-Clause Synergized Contradiction Separation based inference rule, which is essentially different from the multi-ary resolution, but includes binary resolution as its special case. The corresponding first-order automated deduction system is called MC-SCS. This present work focuses on the MC-SCS's reasoning algorithm scheme, proof procedure, implementation, and experimental results. The empirical evaluation shows promising results compared with some state of art first-order theorem provers.

Original language	English
Title of host publication	Proceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017
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)	9781538618295
DOIs	https://doi.org/10.1109/ISKE.2017.8258793
Publication status	Published (in print/issue) - 1 Jul 2017
Event	12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017 - NanJing, JiangSu, China Duration: 24 Nov 2017 → 26 Nov 2017

Publication series

Name	Proceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017
Volume	2018-January

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:
ACKNOWLEDGMENT This work is partially supported by the National Natural Science Foundation of China (Grant No. 61673320). Also is supported by the Fundamental Research Funds for the Central Universities(Grant No. 2682017ZT12)

Publisher Copyright:
© 2017 IEEE.

Keywords

automated deduction
contradiction separation
dynamic multi-clause synergized deduction
resolution
theorem proving

Access to Document

10.1109/ISKE.2017.8258793

Cite this

Zhong, J., Cao, F., Wu, G., Xu, Y., & Liu, J. (2017). Multi-clause synergized contradiction separation based first-order theorem prover-MC-SCS. In T. Li, L. M. Lopez, & Y. Li (Eds.), Proceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017 (pp. 1-6). (Proceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017; Vol. 2018-January). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ISKE.2017.8258793

Zhong, Jian ; Cao, Feng ; Wu, Guanfeng et al. / Multi-clause synergized contradiction separation based first-order theorem prover-MC-SCS. Proceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017. editor / Tianrui Li ; Luis Martinez Lopez ; Yun Li. Institute of Electrical and Electronics Engineers Inc., 2017. pp. 1-6 (Proceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017).

@inproceedings{455e3711b31648d7b6854aab7f37558c,

title = "Multi-clause synergized contradiction separation based first-order theorem prover-MC-SCS",

abstract = "After extending the term 'contradiction' from the traditionally defined a complementary pair based on two clauses into a typical unsatisfiable clause set (i.e., a standard contradiction which might consist of more than two clauses), a recent work by the same author group proposes a new inference principle and its sound and complete first-order theory framework to escape from the existing static binary resolution into a dynamic Multi-Clause Synergized Contradiction Separation based inference rule, which is essentially different from the multi-ary resolution, but includes binary resolution as its special case. The corresponding first-order automated deduction system is called MC-SCS. This present work focuses on the MC-SCS's reasoning algorithm scheme, proof procedure, implementation, and experimental results. The empirical evaluation shows promising results compared with some state of art first-order theorem provers.",

keywords = "automated deduction, contradiction separation, dynamic multi-clause synergized deduction, resolution, theorem proving",

author = "Jian Zhong and Feng Cao and Guanfeng Wu and Yang Xu and Jun Liu",

note = "Funding Information: ACKNOWLEDGMENT This work is partially supported by the National Natural Science Foundation of China (Grant No. 61673320). Also is supported by 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 = "2017",

month = jul,

day = "1",

doi = "10.1109/ISKE.2017.8258793",

language = "English",

series = "Proceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017",

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

pages = "1--6",

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

booktitle = "Proceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017",

address = "United States",

}

Zhong, J, Cao, F, Wu, G, Xu, Y & Liu, J 2017, Multi-clause synergized contradiction separation based first-order theorem prover-MC-SCS. in T Li, LM Lopez & Y Li (eds), Proceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017. Proceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017, vol. 2018-January, 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.8258793

Multi-clause synergized contradiction separation based first-order theorem prover-MC-SCS. / Zhong, Jian; Cao, Feng; Wu, Guanfeng et al.
Proceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017. ed. / Tianrui Li; Luis Martinez Lopez; Yun Li. Institute of Electrical and Electronics Engineers Inc., 2017. p. 1-6 (Proceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017; Vol. 2018-January).

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

TY - GEN

T1 - Multi-clause synergized contradiction separation based first-order theorem prover-MC-SCS

AU - Zhong, Jian

AU - Cao, Feng

AU - Wu, Guanfeng

AU - Xu, Yang

AU - Liu, Jun

N1 - Funding Information: ACKNOWLEDGMENT This work is partially supported by the National Natural Science Foundation of China (Grant No. 61673320). Also is supported by the Fundamental Research Funds for the Central Universities(Grant No. 2682017ZT12) Publisher Copyright: © 2017 IEEE.

PY - 2017/7/1

Y1 - 2017/7/1

N2 - After extending the term 'contradiction' from the traditionally defined a complementary pair based on two clauses into a typical unsatisfiable clause set (i.e., a standard contradiction which might consist of more than two clauses), a recent work by the same author group proposes a new inference principle and its sound and complete first-order theory framework to escape from the existing static binary resolution into a dynamic Multi-Clause Synergized Contradiction Separation based inference rule, which is essentially different from the multi-ary resolution, but includes binary resolution as its special case. The corresponding first-order automated deduction system is called MC-SCS. This present work focuses on the MC-SCS's reasoning algorithm scheme, proof procedure, implementation, and experimental results. The empirical evaluation shows promising results compared with some state of art first-order theorem provers.

AB - After extending the term 'contradiction' from the traditionally defined a complementary pair based on two clauses into a typical unsatisfiable clause set (i.e., a standard contradiction which might consist of more than two clauses), a recent work by the same author group proposes a new inference principle and its sound and complete first-order theory framework to escape from the existing static binary resolution into a dynamic Multi-Clause Synergized Contradiction Separation based inference rule, which is essentially different from the multi-ary resolution, but includes binary resolution as its special case. The corresponding first-order automated deduction system is called MC-SCS. This present work focuses on the MC-SCS's reasoning algorithm scheme, proof procedure, implementation, and experimental results. The empirical evaluation shows promising results compared with some state of art first-order theorem provers.

KW - automated deduction

KW - contradiction separation

KW - dynamic multi-clause synergized deduction

KW - resolution

KW - theorem proving

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

U2 - 10.1109/ISKE.2017.8258793

DO - 10.1109/ISKE.2017.8258793

M3 - Conference contribution

AN - SCOPUS:85048079260

T3 - Proceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017

SP - 1

EP - 6

BT - Proceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017

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 -

Zhong J, Cao F, Wu G, Xu Y, Liu J. Multi-clause synergized contradiction separation based first-order theorem prover-MC-SCS. In Li T, Lopez LM, Li Y, editors, Proceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017. Institute of Electrical and Electronics Engineers Inc. 2017. p. 1-6. (Proceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017). doi: 10.1109/ISKE.2017.8258793

Multi-clause synergized contradiction separation based first-order theorem prover-MC-SCS

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this