theorem-proving - Kowalski 图定理证明

Question

我正在尝试使用 Kowalski 图算法来求解定理证明。算法的描述位于 http://www.doc.ic.ac.uk/~rak/对于如何处理大事件却保持沉默它生成的重复子句的数量。我想知道是否有处理它们的众所周知的技术？

特别是，你不能简单地抑制重复的生成子句，因为它们附带的链接是相关的。

在我看来，可能有必要跟踪所有的集合到目前为止生成的子句，当生成重复项时，添加改为指向现有实例的新链接。这可能需要是即使名义上删除了一个子句，也仍会保留该子句，因为当它被删除时重生。

重复可能需要根据文本来定义表示，而不是对象相等，因为不同的子句即使相同，也是不同的对象。

谁能确认我是否走在正确的轨道上？另外，唯一我能找到的关于该算法的重要在线引用是上面的链接，有人知道任何其他链接或任何现有代码吗实现它吗？

Answer 1

这看起来基本上是完全合理的；一些谷歌搜索没有提供任何明显的实现。我同意，您想要查看表示之间的平等而不是身份。