SLD解像度

SLD 解決(選択的線状定節解決)は、論理プログラミングで使用される基本的な推論規則です。これは解決の改良版であり、ホーン節に対して健全かつ反駁完全なものとなっています。

解決すべき問題の否定として表される目標節が与えられた場合:

${\displaystyle \neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}}$

選択されたリテラルと入力された明確な節: ${\displaystyle \neg L_{i}}$

${\displaystyle L\lor \neg K_{1}\lor \cdots \lor \neg K_{m}}$

正のリテラル（アトム）が選択されたリテラルのアトムと統合される場合、SLD解決は別の目標節を導出し、その中で選択されたリテラルは入力節の負のリテラルに置き換えられ、統合置換が適用されます。 ${\displaystyle L\,}$ ${\displaystyle L_{i}\,}$${\displaystyle \neg L_{i}\,}$${\displaystyle \theta \,}$

${\displaystyle (\neg L_{1}\lor \cdots \lor \neg K_{1}\lor \cdots \lor \neg K_{m}\ \lor \cdots \lor \neg L_{n})\theta }$

最も単純なケース、つまり命題論理では、アトムとが同一であり、統一置換は無意味です。しかし、より一般的なケースでは、2 つのリテラルを同一にするために統一置換が必要です。 ${\displaystyle L_{i}\,}$${\displaystyle L\,}$${\displaystyle \theta \,}$

「SLD解決」という名前は、ロバート・コワルスキーによって導入された無名の推論規則に対して、マールテン・ファン・エムデンによって付けられました。^[1]その名前は、無制限の節形式の論理に対して健全かつ反駁完全なSL解決^[2]に由来しています。「SLD」は「確定節付きSL解決」の略です。

SL と SLD の両方において、「L」は解決証明が節の線形シーケンスに制限されるという事実を表します。

${\displaystyle C_{1},C_{2},\cdots ,C_{l}}$

ここで、「最上位の節」は入力節であり、他のすべての節は、その親が前の節である解決節です。最後の節が空節である 場合、証明は反証になります。${\displaystyle C_{1}\,}$${\displaystyle C_{i+1}\,}$${\displaystyle C_{i}\,}$${\displaystyle C_{l}\,}$

SLD では、シーケンス内のすべての節が目標節であり、もう一方の親は入力節です。SL 解決では、もう一方の親は入力節か、シーケンスの前の祖先節のいずれかです。

SL と SLD の両方において、「S」は、任意の節で解決される唯一のリテラルは、選択規則または選択関数によって一意に選択されたものであるという事実を表します。SL 解決では、選択されるリテラルは、節に最後に導入されたものに制限されます。最も単純なケースでは、このような後入れ先出し選択関数は、 Prologのように、リテラルが記述される順序によって指定できます。ただし、SLD 解決の選択関数は、SL 解決や Prolog よりも一般的です。選択できるリテラルに制限はありません。 ${\displaystyle C_{i}\,}$

節論理では、SLD 反駁は入力された節のセットが満たされないことを実証します。ただし、論理プログラミングでは、SLD 反駁には計算的解釈もあります。最上位の節は、サブゴールの連言の否定として解釈できます。からの節の導出は 、後方推論によって、入力節をゴール削減手順として使用して、新しいサブゴールのセットを導出することです。統合置換は、選択されたサブゴールからの入力を手順の本体に渡すと同時に、手順の先頭からの出力を残りの選択されていないサブゴールに渡します。空の節は単にサブゴールの空のセットであり、最上位の節のサブゴールの最初の連言が解決されたことを示します。 ${\displaystyle \neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}}$${\displaystyle L_{1}\land \cdots \land L_{i}\land \cdots \land L_{n}}$${\displaystyle C_{i+1}\,}$${\displaystyle C_{i}\,}$${\displaystyle \theta \,}$

SLD 解決は、代替計算の検索ツリーを暗黙的に定義し、初期目標節はツリーのルートに関連付けられます。ツリー内のすべてのノードと、ノードに関連付けられた目標節内の選択されたリテラルと統合される正のリテラルを持つプログラム内のすべての確定節に対して、SLD 解決によって取得された目標節に関連付けられた子ノードが存在します。

子を持たないリーフ ノードは、関連付けられた目標節が空の節である場合は成功ノードになります。関連付けられた目標節が空ではないが、選択されたリテラルがプログラム内の確定節のどの正のリテラルとも統合しない場合は失敗ノードになります。

SLD 解決は、検索ツリーを探索するための検索戦略を決定しないという意味で非決定的です。Prolog は、失敗ノードに遭遇したときにバックトラッキングを使用して、一度に 1 つのブランチずつ、深さ優先でツリーを検索します。深さ優先検索は、コンピューティング リソースの使用において非常に効率的ですが、検索空間に無限ブランチが含まれており、検索戦略が有限ブランチよりもこれらを優先して検索する場合は不完全です。つまり、計算は終了しません。幅優先、最良優先、分枝限定検索などの他の検索戦略も可能です。さらに、検索は、一度に 1 つのノードで順次実行することも、複数のノードを同時に並列実行することもできます。

SLD 解決は、前述のように、選択規則が推論規則によって決定されるのではなく、プログラム実行プロセスのダイナミクスに敏感な別の決定手順によって決定されるという意味で非決定的です。

SLD 解決検索空間は or ツリーであり、異なるブランチが代替計算を表します。命題論理プログラムの場合、SLD は、検索空間がand-or ツリーになるように一般化できます。and-or ツリーのノードはサブゴールを表す単一のリテラルでラベル付けされ、ノードは論理積または論理和によって結合されます。結合サブゴールが変数を共有する一般的なケースでは、and-or ツリーの表現はより複雑になります。

Prolog言語の論理プログラムが与えられます:

q  :-  p .
p .

そしてトップレベルの目標:

q .

探索空間は単一のブランチで構成され、その中でがqに縮小されp、さらに がサブゴールの空集合に縮小され、計算が成功したことを示します。この場合、プログラムは非常に単純なので、選択関数の役割はなく、探索の必要もありません。

節論理では、プログラムは節の集合によって表されます。

${\displaystyle q\lor \neg p}$

${\displaystyle p\,}$

最上位レベルの目標は、単一の否定リテラルを含む目標句によって表されます。

${\displaystyle \neg q}$

検索空間は単一の反論で構成されます:

${\displaystyle \neg q,\neg p,{\mathit {false}}}$

where は空の節を表します。 ${\displaystyle {\mathit {false}}\,}$

プログラムに次の句が追加された場合:

q  :-  r .

すると、探索空間に、葉ノードがr失敗ノードである追加の分岐が存在することになります。Prolog では、この節が元のプログラムの先頭に追加されると、Prolog は節が記述されている順序を使用して、探索空間の分岐が調査される順序を決定します。Prolog は最初にこの新しい分岐を試して失敗し、その後、元のプログラムの単一の分岐を調査するためにバックトラックして成功します。

条項が

p  :-  p .

プログラムにこの節が追加されると、検索ツリーには無限の分岐が含まれることになります。この節が最初に試されると、Prolog は無限ループに入り、成功する分岐が見つかりません。

SLDNF ^[3]は、否定を失敗として 扱うためのSLD解決の拡張である。SLDNFでは、目標節に、たとえば という形式の失敗リテラルとしての否定を含めることができ、これは変数を含まない場合にのみ選択できる。このような変数を含まないリテラルが選択されると、対応する否定されていないリテラルを最上位節としてSLDNF反証があるかどうかを判断するためのサブ証明（またはサブ計算）が試行される。選択されたサブ目標は、サブ証明が失敗した場合は成功し、サブ証明が成功した場合は失敗する。 ${\displaystyle not(p)\,}$${\displaystyle p\,}$${\displaystyle not(p)\,}$

• ジョン・アラン・ロビンソン

• Jean Gallier、SLD-Resolution と論理プログラミング、Logic for Computer Science: Foundations of Automatic Theorem Provingの第 9 章、2003 年オンライン改訂版 (ダウンロード無料)、Wiley 社 (1986 年) より初版発行
• John C. Shepherdson、SLDNF-Resolution with Equality、Journal of Automated Reasoning 8: 297-306、1992; SLDNF-Resolution with Equalityが健全かつ完全である意味論を定義する

• [1] 無料のオンラインコンピューティング辞書からの定義