Multi-ary alpha-ordered linear minimal resolution method in lattice-valued logic system

摘要

On the basis of alpha-minimal resolution principle, an alpha-n(t)-ary resolution dynamic automated reasoning method-multi-ary alpha-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 alpha-ordered linear minimal resolution method is established in LP(X), while its theorems of both soundness and completeness are proved. Then, multi-ary alpha-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 alpha-ordered linear minimal resolution based on lattice-valued logic is analyzed. At last, an multi-ary alpha-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 alpha-n(t)-ary resolution dynamic automated reasoning program.