我正在尝试使用 Kowalski 图算法进行分辨率定理证明。http://www.doc.ic.ac.uk/~rak/对算法的描述 没有说明如何处理它生成的大量重复子句。我想知道是否有一种众所周知的技术来处理它们？
特别是，您不能简单地抑制重复子句的生成，因为它们附带的链接是相关的。
在我看来，可能有必要跟踪迄今为止生成的所有子句的集合，并且当生成重复项时，将新链接添加到现有实例。即使在名义上删除子句时，这也可能需要维护，因为当它重新生成时。
重复可能需要根据文本表示来定义，而不是对象相等，因为不同子句的文字即使它们相同也是不同的对象。
谁能确认我在这里是否走在正确的轨道上？另外，我能找到的关于这个算法的唯一重要的在线参考是上面的链接，有没有人知道其他的，或者任何现有的实现它的代码？