A novel generalization of resolution principle for automated deduction

Yang Xu; Jun Liu; Shuwei Chen; Xiaomei Zhong

doi:10.1142/9789813146976_0078

A novel generalization of resolution principle for automated deduction

Yang Xu, Jun Liu, Shuwei Chen, Xiaomei Zhong

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

6 Citations (Scopus)

Abstract

Resolution principle proposed originally by Robinson in 1965 has dominated automated deduction for over three decades while the current most successful automated deduction systems are based on resolution. In this paper, we consider a generalization of the standard resolution principle and their variation since then, it is proposed as a multi-ary, dynamic, contradiction separation based inference rule for automated deduction, where the existing resolution rule and its variations are its special cases. The key concepts and some conclusions are briefly outlined in this short paper.

Original language	English
Title of host publication	Uncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016
Editors	Jie Lu, Ludovic Koehl, Etienne E. Kerre, Luis Martinez, Xianyi Zeng
Publisher	World Scientific Publishing Co. Pte Ltd
Pages	483-488
Number of pages	6
ISBN (Electronic)	9789813146969
DOIs	https://doi.org/10.1142/9789813146976_0078
Publication status	Published (in print/issue) - 2016
Event	Uncertainty Modelling in Knowledge Engineering and Decision Making - 12th International Fuzzy Logic and Intelligent Technologies in Nuclear Science Conference, FLINS 2016 - Roubaix, France Duration: 24 Aug 2016 → 26 Aug 2016

Publication series

Name	Uncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016

Conference

Conference	Uncertainty Modelling in Knowledge Engineering and Decision Making - 12th International Fuzzy Logic and Intelligent Technologies in Nuclear Science Conference, FLINS 2016
Country/Territory	France
City	Roubaix
Period	24/08/16 → 26/08/16

Bibliographical note

Funding Information:
This work is partially supported by the National Natural Science Foundation of China (Grant No. 61175055).

Publisher Copyright:
© 2016 by World Scientific Publishing Co. Pte. Ltd.

Keywords

Automated deduction
Contradiction separation
Resolution

Access to Document

10.1142/9789813146976_0078

Cite this

Xu, Y., Liu, J., Chen, S., & Zhong, X. (2016). A novel generalization of resolution principle for automated deduction. In J. Lu, L. Koehl, E. E. Kerre, L. Martinez, & X. Zeng (Eds.), Uncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016 (pp. 483-488). (Uncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016). World Scientific Publishing Co. Pte Ltd. https://doi.org/10.1142/9789813146976_0078

Xu, Yang ; Liu, Jun ; Chen, Shuwei et al. / A novel generalization of resolution principle for automated deduction. Uncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016. editor / Jie Lu ; Ludovic Koehl ; Etienne E. Kerre ; Luis Martinez ; Xianyi Zeng. World Scientific Publishing Co. Pte Ltd, 2016. pp. 483-488 (Uncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016).

@inproceedings{77ba2625d9304cb086333098590c92c0,

title = "A novel generalization of resolution principle for automated deduction",

abstract = "Resolution principle proposed originally by Robinson in 1965 has dominated automated deduction for over three decades while the current most successful automated deduction systems are based on resolution. In this paper, we consider a generalization of the standard resolution principle and their variation since then, it is proposed as a multi-ary, dynamic, contradiction separation based inference rule for automated deduction, where the existing resolution rule and its variations are its special cases. The key concepts and some conclusions are briefly outlined in this short paper.",

keywords = "Automated deduction, Contradiction separation, Resolution",

author = "Yang Xu and Jun Liu and Shuwei Chen and Xiaomei Zhong",

note = "Funding Information: This work is partially supported by the National Natural Science Foundation of China (Grant No. 61175055). Publisher Copyright: {\textcopyright} 2016 by World Scientific Publishing Co. Pte. Ltd.; Uncertainty Modelling in Knowledge Engineering and Decision Making - 12th International Fuzzy Logic and Intelligent Technologies in Nuclear Science Conference, FLINS 2016 ; Conference date: 24-08-2016 Through 26-08-2016",

year = "2016",

doi = "10.1142/9789813146976_0078",

language = "English",

series = "Uncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016",

publisher = "World Scientific Publishing Co. Pte Ltd",

pages = "483--488",

editor = "Jie Lu and Ludovic Koehl and Kerre, {Etienne E.} and Luis Martinez and Xianyi Zeng",

booktitle = "Uncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016",

address = "Singapore",

}

Xu, Y, Liu, J, Chen, S & Zhong, X 2016, A novel generalization of resolution principle for automated deduction. in J Lu, L Koehl, EE Kerre, L Martinez & X Zeng (eds), Uncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016. Uncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016, World Scientific Publishing Co. Pte Ltd, pp. 483-488, Uncertainty Modelling in Knowledge Engineering and Decision Making - 12th International Fuzzy Logic and Intelligent Technologies in Nuclear Science Conference, FLINS 2016, Roubaix, France, 24/08/16. https://doi.org/10.1142/9789813146976_0078

A novel generalization of resolution principle for automated deduction. / Xu, Yang; Liu, Jun; Chen, Shuwei et al.
Uncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016. ed. / Jie Lu; Ludovic Koehl; Etienne E. Kerre; Luis Martinez; Xianyi Zeng. World Scientific Publishing Co. Pte Ltd, 2016. p. 483-488 (Uncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016).

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

TY - GEN

T1 - A novel generalization of resolution principle for automated deduction

AU - Xu, Yang

AU - Liu, Jun

AU - Chen, Shuwei

AU - Zhong, Xiaomei

N1 - Funding Information: This work is partially supported by the National Natural Science Foundation of China (Grant No. 61175055). Publisher Copyright: © 2016 by World Scientific Publishing Co. Pte. Ltd.

PY - 2016

Y1 - 2016

N2 - Resolution principle proposed originally by Robinson in 1965 has dominated automated deduction for over three decades while the current most successful automated deduction systems are based on resolution. In this paper, we consider a generalization of the standard resolution principle and their variation since then, it is proposed as a multi-ary, dynamic, contradiction separation based inference rule for automated deduction, where the existing resolution rule and its variations are its special cases. The key concepts and some conclusions are briefly outlined in this short paper.

AB - Resolution principle proposed originally by Robinson in 1965 has dominated automated deduction for over three decades while the current most successful automated deduction systems are based on resolution. In this paper, we consider a generalization of the standard resolution principle and their variation since then, it is proposed as a multi-ary, dynamic, contradiction separation based inference rule for automated deduction, where the existing resolution rule and its variations are its special cases. The key concepts and some conclusions are briefly outlined in this short paper.

KW - Automated deduction

KW - Contradiction separation

KW - Resolution

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

U2 - 10.1142/9789813146976_0078

DO - 10.1142/9789813146976_0078

M3 - Conference contribution

AN - SCOPUS:85037367514

T3 - Uncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016

SP - 483

EP - 488

BT - Uncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016

A2 - Lu, Jie

A2 - Koehl, Ludovic

A2 - Kerre, Etienne E.

A2 - Martinez, Luis

A2 - Zeng, Xianyi

PB - World Scientific Publishing Co. Pte Ltd

T2 - Uncertainty Modelling in Knowledge Engineering and Decision Making - 12th International Fuzzy Logic and Intelligent Technologies in Nuclear Science Conference, FLINS 2016

Y2 - 24 August 2016 through 26 August 2016

ER -

Xu Y, Liu J, Chen S, Zhong X. A novel generalization of resolution principle for automated deduction. In Lu J, Koehl L, Kerre EE, Martinez L, Zeng X, editors, Uncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016. World Scientific Publishing Co. Pte Ltd. 2016. p. 483-488. (Uncertainty Modelling in Knowledge Engineering and Decision Making - Proceedings of the 12th International FLINS Conference, FLINS 2016). doi: 10.1142/9789813146976_0078

A novel generalization of resolution principle for automated deduction

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this