4.2 归结（消解Resolution）

　　归结是一个重要的推理规则，归结方法自1965年Robinson提出后，使自动定理证明技术得到很大的发展。本节先简要介绍归结方法的基本思想，然后再分别讨论命题逻辑和谓词逻辑的归结原理。