自动定理证明中含有等词的Horn集上的输入半锁反驳

本文的主要结果是文献1]的推广。 众所周知,等词(equality)由于它的自反性、对称性、可传性以及替换性,它在谓词演算中有着特殊的地位。这样的特殊性也反映在自动定理证明中,一个含有等词的E不可满足子句集,在各种反驳策略中,除了使用归结原理(resolution)以外,还必须使用调解(paramodulation)这一推理规则。尽管如此,我们仍然可以把不含等词的不可满足子句集上的许多性质和证明技术,推广到含有等词的不可满足子句集上去。例如在文献2]的第八章中,就有相应的输入调解、单位调解和线性调解等等。