2.1 归结原理概述 　　归结原理由J.A.Robinson于1965年提出，又称为消解原理。该原理是Robinson在Herbrand理论基础上提出的一种基于逻辑的、采用反证法的推理方法。由于其理论上的完备性，归结原理成为机器定理证明的主要方法。