International Journal of Computational Intelligence Systems

<Previous Article In Issue
Next Article In Issue>
Volume 11, Issue 1, 2018, Pages 384 - 401

Non-Clausal Multi-ary α-Generalized Resolution Calculus for a Finite Lattice-Valued Logic

Authors
Yang Xu1, xuyang@home.swjtu.edu.cn, Jun Liu2, j.liu@ulster.ac.uk, Xingxing He1, *, x.he@home.swjtu.edu.cn, Xiaomei Zhong1, zhongxm2013@home.swjtu.edu.cn, Shuwei Chen1, *, swchen@home.swjtu.edu.cn
1School of Mathematics, Southwest Jiaotong University, Chengdu 610031, P.R. China
2School of Computing, Ulster University, Northern Ireland, UK
Corresponding Authors
Received 30 August 2017, Accepted 7 December 2017, Available Online 1 January 2018.
DOI
10.2991/ijcis.11.1.29How to use a DOI?
Keywords
Automated reasoning; Resolution principle; Lattice-valued logic; Lattice implication algebra; Non-clausal multi-ary α-generalized resolution
Abstract

Due to the need of the logical foundation for uncertain information processing, development of efficient automated reasoning system based on non-classical logics is always an active research area. The present paper focuses on the resolution-based automated reasoning theory in a many-valued logic with truth-values defined in a lattice-ordered many-valued algebraic structure - lattice implication algebras (LIA). Specifically, as a continuation and extension of the established work on binary resolution at a certain truth-value level α (called α-resolution), a non-clausal multi-ary α-generalized resolution calculus is introduced for a lattice-valued propositional logic LP(X) based on LIA, which is essentially a non-clausal generalized resolution avoiding reduction to normal clausal form. The new resolution calculus in LP(X) is then proved to be sound and complete. The concepts and theoretical results are further extended and established in the corresponding lattice-valued first-order logic LF(X) based on LIA.

Copyright
© 2018, the Authors. Published by Atlantis Press.
Open Access
This is an open access article under the CC BY-NC license (http://creativecommons.org/licences/by-nc/4.0/).

Download article (PDF)
View full text (HTML)

<Previous Article In Issue
Next Article In Issue>
Journal
International Journal of Computational Intelligence Systems
Volume-Issue
11 - 1
Pages
384 - 401
Publication Date
2018/01/01
ISSN (Online)
1875-6883
ISSN (Print)
1875-6891
DOI
10.2991/ijcis.11.1.29How to use a DOI?
Copyright
© 2018, the Authors. Published by Atlantis Press.
Open Access
This is an open access article under the CC BY-NC license (http://creativecommons.org/licences/by-nc/4.0/).

Cite this article

risenwbib
TY  - JOUR
AU  - Yang Xu
AU  - Jun Liu
AU  - Xingxing He
AU  - Xiaomei Zhong
AU  - Shuwei Chen
PY  - 2018
DA  - 2018/01/01
TI  - Non-Clausal Multi-ary α-Generalized Resolution Calculus for a Finite Lattice-Valued Logic
JO  - International Journal of Computational Intelligence Systems
SP  - 384
EP  - 401
VL  - 11
IS  - 1
SN  - 1875-6883
UR  - https://doi.org/10.2991/ijcis.11.1.29
DO  - 10.2991/ijcis.11.1.29
ID  - Xu2018
ER  -