Non-clausal multi-ary α-generalized resolution principle for a lattice-valued first-order logic

Yang Xu; Jun Liu; Xingxing He; Xiaomei Zhong; Shuwei Chen

doi:10.1109/ISKE.2015.88

Non-clausal multi-ary α-generalized resolution principle for a lattice-valued first-order logic

Yang Xu, Jun Liu, Xingxing He, Xiaomei Zhong, Shuwei Chen

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

5 Citations (Scopus)

Abstract

The present paper focuses on a resolution-based automated reasoning theory in a lattice-valued logic system with truth-values defined in a lattice-valued algebraic structure - lattice implication algebras (LIA) in order to handle automated deduction under an uncertain environment. Particularly, as a continuation and extension of the established work on binary resolution at a certain truth-value level a (called a-resolution), a non-clausal multi-ary a-generalized resolution principle and deduction are introduced in this paper for a lattice-valued first-order logic LF(X) based on LIA, which is essentially non-clausal generalized resolution avoiding the reduction to normal clausal form. Non-clausal multi-ary a-generalized resolution deduction in LF(X) is then proved to be sound and complete. The present work is expected to provide a theoretical foundation of more efficient resolution based automated reasoning in lattice-valued logic.

Original language	English
Title of host publication	Proceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	1-7
Number of pages	7
ISBN (Electronic)	9781467393225
DOIs	https://doi.org/10.1109/ISKE.2015.88
Publication status	Published (in print/issue) - 13 Jan 2016
Event	10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015 - Taipei, Taiwan, Republic of China Duration: 24 Nov 2015 → 27 Nov 2015

Publication series

Name	Proceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015

Conference

Conference	10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015
Country/Territory	Taiwan, Republic of China
City	Taipei
Period	24/11/15 → 27/11/15

Bibliographical note

Publisher Copyright:
© 2015 IEEE.

Keywords

Automated reasoning
Lattice implication algebra
Latticevalued logic
Non-clausal multi-ary - generalized resolution
Resolution principle

Access to Document

10.1109/ISKE.2015.88

Cite this

Xu, Y., Liu, J., He, X., Zhong, X., & Chen, S. (2016). Non-clausal multi-ary α-generalized resolution principle for a lattice-valued first-order logic. In Proceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015 (pp. 1-7). Article 7383015 (Proceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ISKE.2015.88

Xu, Yang ; Liu, Jun ; He, Xingxing et al. / Non-clausal multi-ary α-generalized resolution principle for a lattice-valued first-order logic. Proceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015. Institute of Electrical and Electronics Engineers Inc., 2016. pp. 1-7 (Proceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015).

@inproceedings{b2e57443228a4a1fb340fef02824ec42,

title = "Non-clausal multi-ary α-generalized resolution principle for a lattice-valued first-order logic",

abstract = "The present paper focuses on a resolution-based automated reasoning theory in a lattice-valued logic system with truth-values defined in a lattice-valued algebraic structure - lattice implication algebras (LIA) in order to handle automated deduction under an uncertain environment. Particularly, as a continuation and extension of the established work on binary resolution at a certain truth-value level a (called a-resolution), a non-clausal multi-ary a-generalized resolution principle and deduction are introduced in this paper for a lattice-valued first-order logic LF(X) based on LIA, which is essentially non-clausal generalized resolution avoiding the reduction to normal clausal form. Non-clausal multi-ary a-generalized resolution deduction in LF(X) is then proved to be sound and complete. The present work is expected to provide a theoretical foundation of more efficient resolution based automated reasoning in lattice-valued logic.",

keywords = "Automated reasoning, Lattice implication algebra, Latticevalued logic, Non-clausal multi-ary - generalized resolution, Resolution principle",

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

note = "Publisher Copyright: {\textcopyright} 2015 IEEE.; 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015 ; Conference date: 24-11-2015 Through 27-11-2015",

year = "2016",

month = jan,

day = "13",

doi = "10.1109/ISKE.2015.88",

language = "English",

series = "Proceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015",

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

pages = "1--7",

booktitle = "Proceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015",

address = "United States",

}

Xu, Y, Liu, J, He, X, Zhong, X & Chen, S 2016, Non-clausal multi-ary α-generalized resolution principle for a lattice-valued first-order logic. in Proceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015., 7383015, Proceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015, Institute of Electrical and Electronics Engineers Inc., pp. 1-7, 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015, Taipei, Taiwan, Republic of China, 24/11/15. https://doi.org/10.1109/ISKE.2015.88

Non-clausal multi-ary α-generalized resolution principle for a lattice-valued first-order logic. / Xu, Yang; Liu, Jun; He, Xingxing et al.
Proceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015. Institute of Electrical and Electronics Engineers Inc., 2016. p. 1-7 7383015 (Proceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015).

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

TY - GEN

T1 - Non-clausal multi-ary α-generalized resolution principle for a lattice-valued first-order logic

AU - Xu, Yang

AU - Liu, Jun

AU - He, Xingxing

AU - Zhong, Xiaomei

AU - Chen, Shuwei

PY - 2016/1/13

Y1 - 2016/1/13

N2 - The present paper focuses on a resolution-based automated reasoning theory in a lattice-valued logic system with truth-values defined in a lattice-valued algebraic structure - lattice implication algebras (LIA) in order to handle automated deduction under an uncertain environment. Particularly, as a continuation and extension of the established work on binary resolution at a certain truth-value level a (called a-resolution), a non-clausal multi-ary a-generalized resolution principle and deduction are introduced in this paper for a lattice-valued first-order logic LF(X) based on LIA, which is essentially non-clausal generalized resolution avoiding the reduction to normal clausal form. Non-clausal multi-ary a-generalized resolution deduction in LF(X) is then proved to be sound and complete. The present work is expected to provide a theoretical foundation of more efficient resolution based automated reasoning in lattice-valued logic.

AB - The present paper focuses on a resolution-based automated reasoning theory in a lattice-valued logic system with truth-values defined in a lattice-valued algebraic structure - lattice implication algebras (LIA) in order to handle automated deduction under an uncertain environment. Particularly, as a continuation and extension of the established work on binary resolution at a certain truth-value level a (called a-resolution), a non-clausal multi-ary a-generalized resolution principle and deduction are introduced in this paper for a lattice-valued first-order logic LF(X) based on LIA, which is essentially non-clausal generalized resolution avoiding the reduction to normal clausal form. Non-clausal multi-ary a-generalized resolution deduction in LF(X) is then proved to be sound and complete. The present work is expected to provide a theoretical foundation of more efficient resolution based automated reasoning in lattice-valued logic.

KW - Automated reasoning

KW - Lattice implication algebra

KW - Latticevalued logic

KW - Non-clausal multi-ary - generalized resolution

KW - Resolution principle

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

U2 - 10.1109/ISKE.2015.88

DO - 10.1109/ISKE.2015.88

M3 - Conference contribution

AN - SCOPUS:84966546687

T3 - Proceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015

SP - 1

EP - 7

BT - Proceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015

Y2 - 24 November 2015 through 27 November 2015

ER -

Xu Y, Liu J, He X, Zhong X, Chen S. Non-clausal multi-ary α-generalized resolution principle for a lattice-valued first-order logic. In Proceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015. Institute of Electrical and Electronics Engineers Inc. 2016. p. 1-7. 7383015. (Proceedings - The 2015 10th International Conference on Intelligent Systems and Knowledge Engineering, ISKE 2015). doi: 10.1109/ISKE.2015.88

Non-clausal multi-ary α-generalized resolution principle for a lattice-valued first-order logic

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this