对于一阶逻辑中任一个恒真的公式，使用归结方法都能在有限步内证明这个公式的恒真性，因此归结方法成为定理机器证明的一种重要方法。

以命题逻辑为例，在两个子句中删掉互补的两个文字(如果存在的话)，将剩下的子句再析取起来就是使用归结方法得到的这两个子句的归结式。例如，，，则对和使用归结方法，得到。而也可等价地写成，是，由和得到的推理实际上是三段论推理。因此，三段论是归结方法的一个特例。

用归结方法证明数学定理实质上是一个反驳过程。在数理逻辑中，一个数学定理，通常写成如下公式：

式中是前提公式，是结论公式。证明上述定理成立，相当于证明公式是恒真的，也相当于证明如下公式：

是恒假的。将公式等价地化成合取范式，得到一个子句集（中子句之间是合取关系），用归结方法证明了的恒假性，就相当于证明了上述定理。

这一方法不仅对命题逻辑适用，对一阶逻辑也适用，当然需要加进合一替换的概念。

其后，各国学者对这一方法进行了一系列的改进。1965年，沃斯（Wos），罗宾逊（Robinson）和库森（Curson）等人提出了支撑集归结，支撑集归结是完备的。1967年，斯拉格爾（Slagle）提出了语义归结。1970年，拉夫兰（Loveland）和拉克汉姆（Luckham）提出了线性归结。1971年，博耶（Boyer）提出了锁归结，锁归结是完备的。1979年，刘叙华将锁归结与语义归结相结合，提出了锁语义归结。1982年，王湘浩和刘叙华提出广义归结。在20世纪90年代先后出现了基于归结方法的高效的一阶逻辑定理证明器Otter和Vampire。

归结方法也被引入各种非经典逻辑中，成为自动推理领域中的一种基本方法。