Kowalski 图定理证明

Question

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

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

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

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

谁能确认我是否在正确的轨道上？还有，唯一 我可以找到该算法的重要在线参考是 上面的链接，是否有人知道任何其他人或任何现有代码 实现了吗？

Answer 1

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

Answer 2

事实证明，Kowalski 算法并没有我想象的那么有用。基本上，您需要保留生成的所有内容，以免几乎将所有 CPU 时间都花在一遍又一遍地生成相同的子句上。保留所有内容意味着您想要发现重复项，这意味着您想要对所有内容进行哈希处理，这具有有用的副作用，即可以通过简单的指针比较来检查身份（因为每个表达式只有一个副本）。