多值逻辑具有两大特点,一是真值取值个数为两个以上,二是联结词具有离散函数结构。因此,多值逻辑的自动推理呈现出了不同于经典逻辑自动推理的特点,其难点为归结原理的元语言、公式的子句化以及机器证明的运行环境。本文围绕多值逻辑的自动推理进行了如下工作:第一章绪论概括了多值逻辑及其自动推理的研究现状。第二章阐述了经典逻辑归结原理的基本理论,一阶逻辑的归结原理以Herbrand定理为理论基础,以合一替换为推演规则,具备可靠性与完备性,是构建其它非经典逻辑归结原理的重要参考对象。第三章以三值命题逻辑系统为例,描述了多值逻辑的语义性质,对多值逻辑联结词的函数性质与代数性质作了基本介绍。第四章给出了指示语言下的多值逻辑指示归结法,重点处理多值逻辑公式合取范式化的问题。第五章借助定理证明辅助工具Coq,以卢卡谢维奇三值命题逻辑为例,构建了多值逻辑定理证明的语言环境。本文重点探讨了一种多值逻辑公式合取范式化的方法——RES转换,可有效降低归结算法的复杂度。此外,使用Coq构建多值逻辑的机器语言环境是对多值逻辑自动推理从理论到应用的初步尝试。