TY - JOUR
T1 - Contradiction separation based dynamic multi-clause synergized automated deduction
AU - Xu, Yang
AU - Liu, J.
AU - Chen, Shuwei
AU - Zhong, Xiaomei
AU - He, Xingxing
PY - 2018/9/1
Y1 - 2018/9/1
N2 - Resolution as a famous rule of inference has played a key role in automated reasoning for over five decades. A number of variants and refinements of resolution have been also studied, essentially, they are all based on binary resolution, that is, the cutting rule of the complementary pair while every deduction involves only two clauses. In the present work, we consider an extension of binary resolution rule, which is proposed as a novel contradiction separation based inference rule for automated deduction, targeted for dynamic and multiple (two or more) clauses handling in a synergized way, while binary resolution is its special case. This contradiction separation based dynamic multi-clause synergized automated deduction theory is then proved to be sound and complete. The development of this new extension is motivated not only by our view to show that such a new rule of inference can be generic, but also by our wish that this inference rule could provide a basis for more efficient automated deduction algorithms and systems.
AB - Resolution as a famous rule of inference has played a key role in automated reasoning for over five decades. A number of variants and refinements of resolution have been also studied, essentially, they are all based on binary resolution, that is, the cutting rule of the complementary pair while every deduction involves only two clauses. In the present work, we consider an extension of binary resolution rule, which is proposed as a novel contradiction separation based inference rule for automated deduction, targeted for dynamic and multiple (two or more) clauses handling in a synergized way, while binary resolution is its special case. This contradiction separation based dynamic multi-clause synergized automated deduction theory is then proved to be sound and complete. The development of this new extension is motivated not only by our view to show that such a new rule of inference can be generic, but also by our wish that this inference rule could provide a basis for more efficient automated deduction algorithms and systems.
UR - https://pure.ulster.ac.uk/en/publications/contradiction-separation-based-dynamic-multi-clause-synergized-au
U2 - 10.1016/j.ins.2018.04.086
DO - 10.1016/j.ins.2018.04.086
M3 - Article
VL - 462
SP - 93
EP - 113
JO - Information Sciences
JF - Information Sciences
SN - 0020-0255
ER -