α-resolution principle based on first-order lattice-valued logic LF(X)

In the present paper, as a continuous work about α-resolution principle based on lattice-valued propositional logic LP(X) (Information Sciences 130 (2000) 1-29) whose algebra of truth-values is a relatively general lattice - lattice implication algebra (LIA), the lattice-valued resolution principle for the corresponding first-order lattice-valued logic system LF(X) is focused. Firstly, some concepts about lattice-valued resolution principle for LF(X) are introduced and the Herbrand theorem for LF(X) is proved. Then, an α-resolution principle, which can be used to judge if a first-order lattice-valued logical formula in LF(X) is false at a truth-valued level α (i.e., α-false), is established. Finally, the completeness theorem of this α-resolution principle and the soundness theorem for the strong α-resolution are also proved. It is hoped that the current work would serve as a foundation for constructing resolution-based automated reasoning methods for lattice-valued logic capable of dealing with both comparable and incomparable uncertain information.