论文部分内容阅读
本文对谓词逻辑的归结原理进行了研究。文章首先从一阶谓词逻辑的定义和定理出发，并和归结原理联系起来，使它们成为一个统一的整体。然后介绍Herbrand定理，Herbrand采用了反证法的思想，将永真性的证明问题转化成为不可满足性的证明问题，即要证明一个公式G的永真性，其方法是去证明该公式G的否定的不可满足性。因为归结法完备性证明要使用Herbrand定理，从这个意义上说，归结原理是建立在Herbrand定理之上的。但是归结原理比起Herbrand定理有重大改进，节约了很多时间和空间，使机器定理证明变成了现实。