α-Resolution Principle Based on an Intermediate Element Lattice-valued First-order Logic IELF(X)

摘要

In the present paper, as a continuous work about α-resolution principle based on an intermediate element lattice-valued propositional logic IELP(X) whose algebra of truth-value is a relative general lattice—lattice implication algebra(LIA), the resolution principle for the corresponding lattice-valued first-order resolution principle for IELF(X) is focused. Firstly, some concepts about lattice-valued resolution principle for IELF(X) are introduced and the Herbrand theorom for IELF(X) is proved. Then, the α-resolution principle, which can be used to judge if an intermediate element lattice-valued first-order logical formula is always false at a truth-valued level α (i.e. α-falsc) is established. And, the completeness theorem and soundness theorom of this α-resolution principle are also proved. It is hoped that the current work will 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.