Loading article…
アブダクティブ論理プログラミング（ALP ）は、アブダクティブ推論に基づいて問題を宣言的に解決するために使用できる高レベルの知識表現フレームワークです。これは、一部の述語を不完全に定義し、アブダクティブ述語として宣言することを許容することで、通常の論理プログラミングを拡張したものです。問題解決は、解決すべき問題の解決策として、これらのアブダクティブ述語に関する仮説（アブダクティブ仮説）を導出することによって行われます。これらの問題は、説明が必要な観察（古典的なアブダクションの場合と同様）または達成すべき目標（通常の論理プログラミングの場合と同様）のいずれかです。診断、計画、自然言語処理、機械学習における問題解決に使用できます。また、アブダクティブ推論の一形態として、否定を失敗として解釈するためにも使用されています。
アブダクション論理プログラムには3つの構成要素があります。どこ：
通常、論理プログラム P には、ヘッド (または結論) が推論可能な述語を参照する節は含まれません。(この制限は一般性を損なうことなく行うことができます。) また、実際には、 IC の整合性制約は、多くの場合、否定の形式、つまり次の形式の節に限定されます。
false:- A1,...,An、B1,...,Bm ではない。
このような制約は、A1,...,An がすべて真であると同時に、B1,...,Bm がすべて偽であるということはあり得ないことを意味します。
Pの節は、推論不可能な述語の集合を定義し、それを通して問題領域の記述（またはモデル）を提供する。ICの整合性制約は、問題のあらゆる解において尊重されるべき問題領域の一般的な特性を指定する。
説明が必要な観察結果、または望ましい目標を表す問題Gは、正負（NAF）リテラルの論理積によって表されます。このような問題は、Gの「アブダクションによる説明」を計算することによって解決されます。
問題Gのアブダクション的説明とは、論理プログラム P にこれらを追加すると問題Gと整合性制約 IC の両方が成り立つような、アブダクション可能な述語の正（場合によっては負も含む）な基礎インスタンスの集合である。したがって、アブダクション的説明は、アブダクション可能な述語の完全または部分的な定義を追加することによって論理プログラム P を拡張する。このようにして、アブダクション的説明は、P および IC における問題領域の記述に従って問題の解を形成する。アブダクション的説明によって与えられる問題記述の拡張または補完は、これまで問題の解に含まれていなかった新しい情報を提供する。整合性制約によって表現されることが多い、ある解を別の解よりも優先するための品質基準は、問題Gの特定のアブダクション的説明を選択するために適用できる。
ALPにおける計算は、通常の論理プログラミングにおける逆算推論（問題を部分問題に分解するため）と、アブダクションによる説明が整合性制約を満たしていることを示す一種の整合性チェックを組み合わせたものである。
以下の2つの例は、ALPの厳密な構文ではなく、簡潔で構造化された英語で記述されており、ALPにおけるアブダクション的説明の概念と、それが問題解決にどのように関係しているかを示しています。
アブダクション論理プログラム、、以下の文：
雨が降れば 草は濡れている。スプリンクラーが作動していれば 草は濡れている。 太陽が照っていた。
推論可能な述語「雨が降った」と「スプリンクラーが作動していた」であり、唯一の整合性制約はは：
雨が降っていて太陽が照っていた場合 は偽となる。
草が濡れているという観察結果には、「雨が降った」と「スプリンクラーが作動していた」という2つの説明が考えられ、どちらも観察結果を導き出す。しかし、整合性制約を満たすのは、後者の「スプリンクラーが作動していた」という説明のみである。
次の（簡略化された）節から構成されるアブダクション論理プログラムを考えてみましょう。
Xは、Xが米国で生まれた場合、 市民権を持つ。X は、 Xが米国以外で生まれ、 Xが米国居住者であり、 Xが帰化している場合、市民権を持つ。Xは、 Xが米国以外で生まれ、 YがXの母親であり、 Yが市民権を持ち、 Xが登録されている場合、 市民権を持つ。 メアリーはジョンの母親である。 メアリーは市民権を持つ。
5 つの推論可能な述語「米国で生まれた」、「米国以外で生まれた」、「米国の居住者である」、「帰化している」、「登録されている」と、整合性制約とともに：
ジョンがアメリカ合衆国の居住者である場合は 偽となります。
目標「ジョンは市民である」には、2つのアブダクション解が存在する。1つは「ジョンは米国で生まれた」であり、もう1つは「ジョンは米国以外で生まれ、かつ登録されている」である。居住と帰化によって市民権を取得するという潜在的な解は、整合性制約に違反するため、失敗に終わる。
より複雑な例で、ALPのより正式な構文で記述されたものを以下に示します。
以下のアブダクション論理プログラムは、細菌E. coliの乳糖代謝の単純なモデルを記述しています。プログラムPは、（最初のルールで）E. coliが2つの酵素パーミアーゼとガラクトシダーゼを生成すれば、糖である乳糖を栄養源として利用できることを記述しています。すべての酵素と同様に、これらの酵素は、発現する遺伝子（Gene）によってコードされている場合に生成されます（2番目のルールで説明）。パーミアーゼとガラクトシダーゼの2つの酵素は、それぞれlac(y)とlac(z)という2つの遺伝子によってコードされており（プログラムの5番目と6番目のルールで説明）、オペロンと呼ばれる遺伝子クラスター（lac(X)）の中にあります。このオペロンは、グルコースの量（amt）が少なく乳糖の量が多い場合、または両方が中程度のレベルにある場合に発現します（4番目と5番目のルールを参照）。アブダクティブAは、述語「amount」のすべての基本インスタンスを仮定可能と宣言します。これは、モデルにおいて、各時点における各種物質の量が不明であることを反映しています。これは、各問題ケースで決定する必要のある不完全な情報です。整合性制約ICは、任意の物質(S)の量が1つの値しか取らないことを示しています。
feed ( lactose ) :- make ( permease ), make ( galactosidase ). make ( Enzyme ) :- code ( Gene , Enzyme ), express ( Gene ). express ( lac ( X )) :- amount ( glucose , low ), amount ( lactose , hi ). express ( lac ( X )) :- amount ( glucose , medium ), amount ( lactose , medium ). code ( lac ( y ), permease ). code ( lac ( z ), galactosidase ). temperature ( low ) :- amount ( glucose , low ).false :- amount ( S , V1 ), amount ( S , V2 ), V1 ≠ V2 。abducible_predicate ( amount )。問題の目標はこれは、説明すべき観察結果として生じる場合もあれば、計画を見つけることで達成すべき状況として生じる場合もある。この目標には、2つのアブダクションによる説明がある。
どちらを採用するかは、入手可能な追加情報によって決まる可能性がある。例えば、グルコースレベルが低いと生物が特定の行動を示すことがわかっている場合、モデルでは、そのような追加情報は生物の温度が低いことである。そして、この情報の真偽を観察することで、それぞれ最初の説明または2番目の説明を選択することが可能となる。
いったん説明が選択されると、それは理論の一部となり、新たな結論を導き出すために用いられる。その説明、そしてより一般的にはこれらの新たな結論が、問題の解決策となる。
Theorist システムで示されているように、[ 1 ] [ 2 ]アブダクションはデフォルト推論にも使用できます。さらに、ALP のアブダクションは、通常の論理プログラミングにおける失敗として否定をシミュレートできます。
鳥が異常であることが証明できない場合、その鳥は飛べるとデフォルトで推論するという古典的な例を考えてみましょう。以下は、否定を失敗として用いた例の変形です。
canfly ( X ) :- bird ( X ), not ( abnormal_flying_bird ( X )). abnormal_flying_bird ( X ):- wounded ( X ). bird ( john ). bird ( mary ). wounded ( john ).以下は、 ALPにおいて整合性制約を持つ推論可能な述語を使用した同じ例です。normal_flying_bird(_)
canfly ( X ) :- bird ( X ), normal_flying_bird ( X ). false :- normal_flying_bird ( X ), wounded ( X ). bird ( john ). bird ( mary ). wounded ( john ).推論可能な述語は、述語の反対である。normal_flying_bird(_),abnormal_flying_bird(_)
ALP でアブダクションを使用すると、仮定の下で結論を導き出すことができます。この結論は、整合性制約が違反されていることを示すことができないため、仮定から導き出すことができます。これは、を示すことができないためです。対照的に、仮定と事実が整合性制約に違反するため、結論を導き出すことはできません。ALP におけるこの推論方法は、否定を失敗として推論することをシミュレートします。[ 3 ]canfly(mary)normal_flying_bird(mary)wounded(mary).canfly(john),normal_flying_bird(john)wounded(john)
逆に、安定モデル意味論では、否定を失敗として用いることで、ALPにおけるアブダクションをシミュレートすることが可能です。[ 4 ]これは、アブダクション可能な述語ごとに、追加の反対述語と節のペアを追加することで実現できます。p,negp,
p :- not ( negp ). negp :- not ( p ).この2つの節には2つの安定モデルがあり、1つはが真 、もう1つはが真です。このアブダクションをシミュレートする手法は、生成とテストの方法論を用いて問題を解決するために、解答集合プログラミング でよく用いられます。p,negp,
ALPにおけるアブダクション的説明という中心概念の形式意味論は、以下のように定義できる。
アブダクション論理プログラムが与えられた場合、問題に対するアブダクションによる説明セット導出可能な述語上の基底原子の以下の条件を満たすもの：
この定義では、論理プログラミングの基礎となる意味論の選択が残されており、それによって含意関係の正確な意味を与えることができる。そして、（拡張された）論理プログラムの一貫性の概念。完全性、安定性、または正則性といった論理プログラミングのさまざまな意味論は、（実際に使用されてきたように）さまざまなアブダクションの説明の概念を与え、したがってさまざまな形式のALPフレームワークを与えることができる。
上記の定義は、整合性制約の役割の形式化に関して特定の見解に基づいている。可能なアブダクション解に対する制約として。これは、アブダクション解で拡張された論理プログラムによってこれらが必然的に含まれることを要求する。したがって、拡張された論理プログラムの任意のモデル（これは、与えられた世界から導かれると考えることができる）において、）整合性制約の要件が満たされている。場合によっては、これは不必要に厳しく、より弱い一貫性の要件、すなわち一貫性があり、十分であるということは、拡張プログラムの少なくとも 1 つのモデル (可能な結果世界) が存在し、そこで整合性制約が満たされることを意味します。実際には、多くの場合、論理プログラムとその拡張は常に一意のモデルを持つため、整合性制約の役割を形式化するこの 2 つの方法は一致します。多くの ALP システムでは、整合性制約の含意ビューを使用します。これは、このビューが制約を問題の目標と同じように扱うため、整合性制約を満たすための特別な手順を必要とせずに簡単に実装できるためです。多くの実際的なケースでは、ALP におけるアブダクション説明のこの形式的定義の 3 番目の条件は、自明に満たされるか、一貫性を捉える特定の整合性制約を使用することで 2 番目の条件に含まれています。
ALPの実装のほとんどは、SLD解決に基づく論理プログラミングの計算モデルを拡張したものです。ALPは、 ASP（ Answer Set Programming）との連携によっても実装でき、その場合はASPシステムが利用できます。前者のアプローチを採用したシステムの例としては、ACLP、A-system、CIFF、SCIFF、ABDUAL、ProLogICAなどがあります。
