解決定理証明にKowalskiグラフアルゴリズムを使用しようとしています。http://www.doc.ic.ac.uk/~rak/でのアルゴリズムの説明は、 生成される多数の重複句について何をすべきかについては言及していません。それらに対処するためのよく知られたテクニックがあるかどうか疑問に思いますか？
特に、重複する句の生成を単純に抑制することはできません。これは、それらに付随するリンクが関連しているためです。
これまでに生成されたすべての句のセットを追跡する必要があるように思われます。複製が生成されたら、代わりに既存のインスタンスに新しいリンクを追加します。これは、句が名目上削除された場合でも、再生成された場合のために、おそらく維持する必要があります。
異なる句のリテラルは、同一であっても別個のオブジェクトであるため、重複は、オブジェクトの同等性ではなく、テキスト表現の観点から定義する必要があります。
私がここで正しい方向に進んでいるかどうかを誰かが確認できますか？また、このアルゴリズムについて私が見つけた唯一の重要なオンラインリファレンスは上記のリンクでした。他の誰か、またはそれを実装している既存のコードを知っている人はいますか？