Kowalski圖定理證明

Question

我試圖使用Kowalski圖算法的分辨率定理 證明。 http://www.doc.ic.ac.uk/~rak/算法的描述沒有說明如何處理它產生的重複子句的大數量 。我想知道是否有一個 知名的技術來處理它們？

尤其是，您不能簡單地抑制生成重複的 子句，因爲它們附帶的鏈接是相關的。

在我看來，可能有必要跟蹤迄今爲止生成的所有 子句的集合，並且當生成副本時，請將 新鏈接添加到現有實例。這可能需要在 即使名義上刪除一個子句時仍保留，因爲它是在 時重新生成的。

複製可能需要以文本 表示，而不是對象相等的術語來定義，因爲 不同條款文本是即使當它們是相同的不同的對象。

任何人都可以確認我是否在正確的軌道上嗎？另外，我能找到的唯一 重要的在線參考資料是上面的鏈接 ，有沒有人知道任何其他人，或任何現有的代碼 實現它？

Answer 1

原來，Kowalski算法沒有我想象的那麼有用。基本上你需要保留你生成的所有東西，以免花費幾乎所有的CPU時間一遍又一遍地生成相同的子句。保持一切意味着你想要找到重複的東西，這意味着你想要散列所有東西，這有副作用，可以通過簡單的指針比較來檢查標識符（因爲你只有每個表達式的一個副本）。

Answer 2

這大多看起來完全合理;一些谷歌搜索沒有提出任何明顯的實現。我同意，你想看看錶示之間的平等而不是身份。