α-Generalized linear resolution method based on lattice-valued first-order logic system

As a continuation of research work on a-generalized resolution for lattice-valued logic system, the α-generalized linear resolution method for lattice-valued first-order logic system LF(X) based on lattice implication algebra is presented, which can provide an automated reasoning tool for information processing and knowledge representation. The soundness theorem is established. By use of the lifting lemma, the weak completeness theorem is also investigated in lattice-valued first-order logic system. Additional, on the basis of the present method for lattice-valued first-order logic system LF(X), an a-generalized linear resolution automated reasoning algorithm is designed.