Abstract: Resolution reasoning method based on predicate logic is one of methods which are well-developed and can be implemented on computer.In order to solve automated reasoning based on resolution principle in lattice-valued first-order logic，a resolution automated reasoning algorithm based on α-resolution principle in lattice-valued first-order logic is proposed by analyzing an example.Its soundness and completeness are proved.

Key words: lattice-valued first-order logic, automated reasoning, α-resolution principle, simple generalized clause set

摘要： 基于谓词逻辑的归结推理方法是目前理论上较为成熟、可以在计算机上实现的推理方法之一。针对格值一阶逻辑LF(X)中归结自动推理问题，以格值一阶逻辑LF(X)的α-归结原理为理论基础，通过对例子进行分析，提出了LF(X)中简单广义子句集的归结自动推理算法，并证明了该算法的可靠性和完备性。

关键词: 格值一阶逻辑, 自动推理, α-归结原理, 简单广义子句集