定理证明的实质就是要对给出的（已知的）前提和结论，证明此前提推导出该结论这一事实是永恒的真理。这是非常困难的，几乎是不可实现的。 　　要证明在一个论域上一个事件是永真的，就要证明在该域中的每一个点上该事实都成立。很显然，论域是不可数时，该问题不可能解决。即使可数，如果该轮域是无限的，问题也无法简单地解决。 　　Herbrand采用了反证法的思想，将永真性的证明问题转化成为不可满足性的证明问题。Herbrand理论为自动定理证明奠定了理论基础，而Robinson的归结原理使得自动定理证明得以实现。因此，归结推理方法在人工智能推理方法中有着很重要的历史地位。 　　从某种意义上讲大部分人工智能问题都可以转化为一个定理证明问题。