ロビンソンの解決手順の欠点は何でしたか？
Aug 16 2020
Paulson etalii。LCFからIsabelle / HOLへのコメント：
一階述語論理の解決。原則として完全ですが、実際にはしばしばがっかりします。
完全とは、一階述語論理で真の公式を正しく証明できることを意味すると思います。自動推論のハンドブックで私は見つけます：
解決は、反論的に完全な定理証明方法です。矛盾（つまり、空の句）は、満足できない一連の句から推測できます。
ウィキペディアから：
充足可能な一次式を充足できないものとして証明しようとすると、計算が終了しない場合があります。
なぜそれが残念なのですか？
回答
1 cody Aug 20 2020 at 00:26
「実際に失望する」は確かに正式に定義することはできませんが、「完全」（実際には「最終的にすべての真の公式を証明できる」という意味）とは異なり、素朴な解決策がリモートでさえ適切でない例、つまり必要な例を見つけるのは非常に簡単です。証明するのは簡単ですが、どの解像度が非常に遅いか。
有名な例は、鳩の巣原理のエンコーディングです。$n$ 命題論理の穴（これはステートメントです "$n+1$ ハトは収まりません $n$重複のない穴）。で指数関数的でない時間の解決のみを使用したこのステートメントの証拠はありません$n$。
述語論理では事態はさらに悪化し、高速解決の証明がなくてもステートメントを見つけるのは非常に簡単です。
定理証明のほとんどの実用的なアルゴリズムは、ハイパーレゾリューションなどのナイーブレゾリューションの拡張であるため、レゾリューションの実装には、すでに非常に難しい問題である分解方程式を選択するための戦略と活発な研究領域を実装する必要があることに注意してください。