Affiliations: [a] Intelligent Control Development Center, Southwest Jiaotong University, Chengdu, Sichuan, China
| [b] National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu, China
| [c] College of Mathematics and Information Science Neijiang Normal University, Neijiang, Sichuan, China
Correspondence:
[*]
Corresponding author. Jia Hairui, Intelligent Control Development Center, Southwest Jiaotong University, Chengdu 610031, Sichuan, P.R. China. E-mail: WEML hairuilover@163.com.
Note: [1] This work is supported by National Natural Science Foundation of China (Grant Nos. 61673320, 61100046, 61305074), the application fundamental research plan project of Sichuan Province (Grant No. 2015JY0120), 2014 Doctoral Innovation Program of Southwest Jiaotong University.
Abstract: On the basis of α-minimal resolution principle, an α-n(t)-ary resolution dynamic automated reasoning method—multi-ary α-ordered linear minimal resolution method is studied in lattice-valued propositional logic system LP(X) and lattice-valued first-order logic system LF(X) based on lattice implication algebra (LIA). Firstly, multi-ary α-ordered linear minimal resolution method is established in LP(X), while its theorems of both soundness and completeness are proved. Then, multi-ary α-ordered linear minimal resolution method is further established in the corresponding lattice-valued first-order logic LF(X), along with its soundness theorem, lifting lemma, and completeness theorem. Then, the validity of multi-ary α-ordered linear minimal resolution based on lattice-valued logic is analyzed. At last, an multi-ary α-ordered linear minimal resolution algorithm in LP(X) is designed, and it is proved to be sound and complete, then it is further extended in the corresponding LF(X). This lays the foundation for the further study on α-n(t)-ary resolution dynamic automated reasoning program.
