Kowalski 图定理证明
我正在尝试使用 Kowalski 图算法来求解定理 证明。 算法的描述位于 http://www.doc.ic.ac.uk/~rak/ 对于如何处理大事件保持沉默 它生成的重复子句的数量。 我想知道是否有 处理它们的众所周知的技术？
特别是，你不能简单地抑制重复的生成 条款，因为它们附带的链接是相关的。
在我看来，可能有必要跟踪所有的集合 到目前为止生成的子句，当生成重复项时，添加 改为指向现有实例的新链接。 这可能需要是 即使名义上删除了一个子句，也仍会保留该子句，因为当它被删除时 再生了。
重复可能需要根据文本来定义 表示，而不是对象相等，因为 不同的子句即使相同，也是不同的对象。
谁能确认我是否走在正确的轨道上？ 另外，唯一 我能找到的关于该算法的重要在线参考是 上面的链接，有人知道任何其他链接或任何现有代码吗 实施吗？
I'm trying to use the Kowalski graph algorithm for resolution theorem
proving. The description of the algorithm at
http://www.doc.ic.ac.uk/~rak/ is silent on what to do about the large
number of duplicate clauses it generates. I'm wondering if there's a
well-known technique for dealing with them?
In particular, you can't simply suppress the generation of duplicate
clauses, because the links that come with them are relevant.
It seems to me that it's probably necessary to track the set of all
clauses generated thus far, and when a duplicate is generated, add the
new links to the existing instance instead. This probably needs to be
maintained even when a clause is nominally deleted, for when it is
regenerated.
Duplication probably needs to be defined in terms of textual
representation, rather than object equality, because literals of
different clauses are distinct objects even when they are identical.
Can anyone confirm whether I'm on the right track here? Also, the only
significant online reference I could find to this algorithm was the
link above, does anyone know of any others, or any existing code
implementing it?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
这看起来基本上是完全合理的。 一些谷歌搜索没有提供任何明显的实现。 我同意，你想看看表征之间的平等而不是同一性。
This mostly looks perfectly plausible; some Googling doesn't present any obvious implementations. I agree, you want to look at equality between the representations instead of identity.
事实证明，Kowalski 算法并不像我想象的那么有用。 基本上，您需要保留生成的所有内容，以免将几乎所有的 CPU 时间都花在一遍又一遍地生成相同的子句上。 保留所有内容意味着您想要发现重复项，这意味着您想要对所有内容进行哈希处理，这有一个有用的副作用，即可以通过简单的指针比较来检查身份（因为每个表达式只有一个副本）。
Turns out the Kowalski algorithm just isn't as useful as I thought it might be. Basically you need to keep everything you generate so as not to spend practically all your CPU time generating the same clauses over and over again. Keeping everything means you want to spot duplicates which means you want to hash everything, which has the useful side effect that identity can be checked by simple pointer comparison (since you only have one copy of each expression).