Ideal resolution principle for lattice-valued first-order logic based on lattice implication algebra

As a continuate work,ideal-based resolution principle for lattice-valued first-order logic system LF(X) is proposed,which is an extension of α-resolution principle in lattice-valued logic system based on lattice implication algebra.In this principle,the resolution level is an ideal of lattice implication algebra,instead of an element in truth-value field.Moreover,the soundness theorem is given.In the light of lifting lemma,the completeness theorem is established.This can provide a new tool for automated reasoning.