格值命题逻辑LP(X)中自动推理算法效率分析

　　定理机器证明是自动推理研究中一个重要的研究方向，其目的是实现定理证明的机械化。归结自动推理是自动推理的一种力式，它在专家系统、智能机器人、机器学习、软件正确性检验等许多领域显示出重要的作用。从1956年至今，许多学者致力于此领域的研究，提出了许多方法。其中，由Robison于1965年提出的归结方法因其简洁有效而受到广为重视并在此基础上取得了一系列丰富而重要的研究成