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 proceedingConference contributionpeer-review

2 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 languageEnglish
Title of host publicationProceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017
EditorsTianrui Li, Luis Martinez Lopez, Yun Li
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1-6
Number of pages6
ISBN (Electronic)9781538618295
DOIs
Publication statusPublished - 1 Jul 2017
Event12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017 - NanJing, JiangSu, China
Duration: 24 Nov 201726 Nov 2017

Publication series

NameProceedings of the 2017 12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017
Volume2018-January

Conference

Conference12th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2017
CountryChina
CityNanJing, JiangSu
Period24/11/1726/11/17

Keywords

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

Fingerprint

Dive into the research topics of 'Multi-clause synergized contradiction separation based first-order theorem prover-MC-SCS'. Together they form a unique fingerprint.

Cite this