归结原理由J.A.Robinson由1965年提出。 与演绎法(deductiveinference)完全不同，新的逻辑演算(inductiveinference)算法。 一阶逻辑中，至今为止的最有效的半可判定的算法。即，一阶逻辑中任意恒真公式，使用归结原理，总可以在有限步内给以判定。 语义网络、框架表示、产生式规则等等都是以推理方法为前提的。即，有了规则已知条件，顺藤摸瓜找到结果。而归结方法是自动推理、自动推导证明用的。（“数学定理机器证明”）