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

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

Conference

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

Keywords

  • Automated reasoning
  • Clause Selection
  • Literal Selection
  • Logic
  • Resolution

Fingerprint

Dive into the research topics of 'Some synergized clause selection strategies for contradiction separation based automated deduction'. Together they form a unique fingerprint.

Cite this