Affiliations: [a] Key Lab of Data Recovery, Sichuan Province, Neijiang Normal University, Neijiang, Sichuan, P.R. China | [b] College of Mathematics and Information Sciences, Neijiang Normal University, Neijiang, Sichuan, P.R. China | [c] Intelligent Control Development Center, Southwest Jiaotong University, Chengdu, Sichuan, P.R. China
Correspondence:
[*]
Corresponding author. Zhong Xiaomei, Intelligent Control Development Center, Southwest Jiaotong University, Chengdu, 610031 Sichuan, P.R. China. liuyiyl@126.com; zhongxm@126.com.
Note: [1] This work is supported by National Natural Science Foundation of P.R.China (Grant no. 61175055, 61305074); The Application Basic Research Plan Project of Sichuan Province (No.2015JY0120); The Scientific Research Project of Department of Education of Sichuan Province (14ZA0245, 15ZB0270); The Scientific Research Fund of Neijiang Normal University (No.13ZB05).
Abstract: This paper focuses on multi-ary α-semantic resolution automated reasoning method based on multi-ary α-resolution principle for a lattice-valued logic with truth-value in a lattice implication algebra. Firstly, the definitions of the multi-ary α-semantic resolution and multi-ary α-semantic resolution deduction in LF (X) are given, respectively, the soundness and completeness of this ground case are gotten. Secondly, the validity of multi-ary α-semantic resolution method is analyzed. Thirdly, the algorithm for multi-ary α-semantic resolution methods based on lattice-valued first-order logic LF (X) is constructed. This work will provide a theoretical foundation for the more efficient resolution based automated reasoning in lattice-valued logic.
