後方連鎖推論(または後方推論)は、一般的に目標から逆算して推論を行うと説明される推論手法です。自動定理証明器、推論エンジン、証明支援システム、その他の人工知能アプリケーションで使用されています。[ 1 ]
ゲーム理論では、研究者はそれを(より単純な)部分ゲームに適用してゲームの解を見つけ出す。このプロセスは後方帰納法と呼ばれる。チェスでは、これは逆行分析と呼ばれ、コンピュータチェスの終盤戦の表を作成するために用いられる。
逆連鎖は、論理プログラミングではSLD 解決によって実装されます。どちらのルールも、モーダス ポネンス推論ルールに基づいています。これは、推論ルールと論理的含意を用いた推論で最も一般的に使用される 2 つの方法の 1 つであり、もう 1 つは順連鎖です。逆連鎖システムは通常、深さ優先探索戦略を採用します(例: Prolog )。[ 2 ]
バックワードチェイニングは、目標のリスト(または仮説)から始まり、結果から前件へと逆方向に進み、これらの結果のいずれかを裏付けるデータがあるかどうかを確認します。 [ 3 ]バックワードチェイニングを使用する推論エンジンは、望ましい目標に一致する結果( Then節)を持つ推論ルールが見つかるまで、推論ルールを検索します。そのルールの前件(If節)が真であると知られていない場合は、目標のリストに追加されます(目標を確認するには、この新しいルールを確認するデータも提供する必要があります)。
例えば、新しいペットのフリッツが不透明な箱に入れられて届けられ、フリッツに関する2つの情報が添えられていたとしましょう。
目標は、以下の4つのルールを含むルールベースに基づいて、フリッツが緑色かどうかを判断することです。

逆推論を用いると、推論エンジンは4つのステップでフリッツが緑色かどうかを判断できます。まず、証明すべき目標の主張としてクエリが表現されます。「フリッツは緑色である」。
1. ルール3において、Xの代わりにフリッツを用いて、その結果が目標と一致するかどうかを確認する。したがって、ルール3は次のようになる。
フリッツがカエルなら、フリッツは緑色だ
結論が目標(「フリッツは緑色である」)と一致するため、ルールエンジンは次に前提(「フリッツはカエルである」)が証明できるかどうかを確認する必要があります。したがって、前提が新たな目標となります。
フリッツはカエルです
2. 再びXをフリッツに置き換えると、ルール1は次のようになります。
フリッツが鳴いて、フリッツがハエを食べるなら、フリッツはカエルだ
結論が現在の目標(「フリッツはカエルである」)と一致するため、推論エンジンは前提(「フリッツは鳴き、ハエを食べる」)が証明できるかどうかを確認する必要があります。したがって、前提が新たな目標となります。
フリッツはカエルのように鳴き、フリッツはハエを食べる
3. この目標は2つの命題の論理積であるため、推論エンジンはそれを2つのサブ目標に分割し、両方とも証明する必要がある。
フリッツが死ぬ フリッツはハエを食べる
4. これら2つの副目標を証明するために、推論エンジンはこれら2つの副目標が初期事実として与えられていることを認識します。したがって、次の論理積は真です。
フリッツはカエルのように鳴き、フリッツはハエを食べる
したがって、規則1の前件は真であり、後件も真でなければならない。
フリッツはカエルです
したがって、規則3の前件は真であり、後件も真でなければならない。
フリッツは緑色です
したがって、この導出により、推論エンジンはフリッツが緑色であることを証明できる。ルール2とルール4は使用されなかった。
目標は常に、含意の帰結の肯定バージョンと一致します(modus tollensのように否定バージョンではありません)。さらに、その前提は新しい目標として考慮されます(帰結を肯定する場合の結論ではありません)。そして、最終的には既知の事実(通常、前提が常に真である帰結として定義されます)と一致しなければなりません。したがって、使用される推論規則はmodus ponensです。
目標リストによって選択・使用されるルールが決定されるため、この方法は目標駆動型と呼ばれ、データ駆動型の順方向推論とは対照的である。逆方向推論は、エキスパートシステムでよく用いられる手法である。
Prolog、Knowledge Machine、ECLiPSeなどのプログラミング言語は、推論エンジン内で後方連鎖をサポートしています。[ 4 ]