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

摘要

In the present paper, as a continuous work about a-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 a-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 a (i.e. α-false) is established. And, the completeness theorom and soundness theorom of this a-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.