代码之家 › 专栏 › 技术社区 › rwallace

科瓦尔斯基图定理证明

theorem-proving

4

rwallace · 技术社区 · 16 年前

我想用Kowalski图的算法来求解分辨率定理证明。算法的描述 http://www.doc.ic.ac.uk/~rak/ 对如何处理大型企业保持沉默它生成的重复子句数。我想知道是否有处理它们的著名技术?

尤其是,不能简单地抑制复制的生成子句,因为它们附带的链接是相关的。

在我看来,可能有必要追踪到目前为止生成的子句,当生成副本时,将而是指向现有实例的新链接。这可能需要即使子句名义上被删除,也要维护,因为再生的。

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

有人能确认我是否在正确的轨道上吗?也是唯一的我能找到的这个算法的重要在线参考是以上链接,是否有人知道任何其他代码或任何现有代码? 实施它?

2 回复 | 直到 15 年前

1

0

Charlie Martin 16 年前

这看起来似乎完全合理;有些Google没有任何明显的实现。我同意,你想看到代表之间的平等,而不是同一性。

2

0

rwallace 15 年前

结果发现Kowalski算法并不像我想象的那样有用。基本上,您需要保留生成的所有内容,这样就不必花费几乎所有的CPU时间反复生成相同的子句。保留所有内容意味着要发现重复项,这意味着要散列所有内容,这有一个有用的副作用,即可以通过简单的指针比较来检查标识(因为每个表达式只有一个副本)。