带等式广义子句集上的归结原理

本文提出了带等式广义子句的概念,使用带等式广义子句去描述定理会更加自然。为了解决不可满足的等式广义子句集的证明,本文又提出了广义调整的方法。并且,本文还证明了,结合使用广义调整的归结原理是完备的。