Non-clausal Multi-ary alpha-Ordered Linear Generalized Resolution Method for Lattice-Valued First-Order Logic

Based on the non-clausal multi-ary a-generalized resolution principle for a lattice-valued logic with truth-values defined in a lattice-valued logical algebra structure-lattice implication algebra, the further extended a-generalized resolution method in this lattice-valued logic is discussed in the present paper in order to increase the efficiency of the resolution method. In the present paper, a non-clausal multi-ary a-ordered linear generalized resolution method for lattice-valued first-order logic system LF(X) based on lattice implication algebra is established. The soundness theorem is given in LF(X). By using lifting lemma, the completeness theorem is also investigated in LF(X). This extended generalized resolution method will provide a theoretical basis for automated soft theorem proving and program verification based on lattice-valued logic.