一次論理推論に関する人工知能の最新のアプローチという本から引用した次の段落を理解するのに苦労しています。
命題化の手法は、完全に一般的なものにすることができます。つまり、すべての一次知識ベースとクエリは、含意が保持されるような方法で命題化できます。したがって、含意の完全な決定手順が得られます....またはそうでないかもしれません。問題があります: 知識ベースに関数記号が含まれている場合、可能な基底用語の置換のセットは無限です! たとえば、知識ベースが父のシンボルに言及している場合、 Father(Father(Father(John)))などの無限に多くのネストされた用語を構築できます。私たちの命題アルゴリズムは、無限大の文のセットを処理するのが困難になります。
幸いなことに、Jacques Herbrand (1930) による有名な定理があり、文が元の 1 階の知識ベースによって含意されている場合、命題化された知識ベースの有限部分集合のみを含む証明が存在するという趣旨です。そのようなサブセットは、その基本用語間で最大のネストの深さを持ちます。最初に定数シンボル ( RichardとJohn ) を持つすべてのインスタンス化を生成し、次に深さ 1 のすべての用語 ( Father(Richard)とFather(John) )を生成するサブセット y を見つけることができます。 )、次に深さ 2 のすべての用語など、含意文の命題証明を構築できるようになるまで続きます。
置換中に無限のネストされた項が生成されることは理解していますが、次のパラグラフで定理について話していると頭がいっぱいです。