安定したモデルセマンティクス

安定したモデル、または回答セットの概念は、否定を失敗とする論理プログラムの宣言的意味を定義するために使用されます。これは、プログラム完了やwell-founded semanticsとともに、論理プログラミングにおける否定の意味に対するいくつかの標準的なアプローチの 1 つです。安定したモデル意味は、回答セットプログラミングの基礎です 。

論理プログラミングにおける否定の宣言的意味論に関する研究は、SLDNF解決（ルール本体に否定が存在する場合にPrologで使用されるSLD解決の一般化）の挙動が、古典的な命題論理でおなじみの真理値表と完全には一致しないという事実に動機づけられました。たとえば、次のプログラムを考えてみましょう 。

${\displaystyle p}$

${\displaystyle r\leftarrow p,q}$

${\displaystyle s\leftarrow p,\operatorname {not} q.}$

このプログラムでは、クエリp は成功します。これは、プログラムにp が事実として含まれているためです。クエリq は失敗します。これは、どのルールのヘッドにも出現しないためです。クエリrも失敗します。これは、ヘッドにrがある唯一のルールの本体にサブゴールq が含まれているためです。すでに説明したように、そのサブゴールは失敗します。最後に、クエリs は成功します。これは、各サブゴールpが成功するためです。(後者は、対応する肯定的なゴールqが失敗するため成功します。) まとめると、指定されたプログラムでの SLDNF 解決の動作は、次の真理値の割り当てによって表すことができます。 ${\displaystyle \operatorname {not} q}$

一方、与えられたプログラムの規則は、コンマを接続詞、記号を否定 と同一視し、含意を逆に書いたものとして扱うことに同意すれば、命題式として見ることができる。例えば、与えられたプログラムの最後の規則は、この観点からは、命題式の別の表記である。 ${\displaystyle \land}$${\displaystyle \operatorname {not} }$${\displaystyle \neg}$${\displaystyle F\leftarrow G}$${\displaystyle G\rightarrow F}$

${\displaystyle p\land \neg q\rightarrow s.}$

上に示した真理値割り当てのプログラムのルールの真理値を計算すると、各ルールが値Tを取得することがわかります。言い換えると、その割り当てはプログラムのモデルです。しかし、このプログラムには他のモデルもあります。たとえば、

したがって、与えられたプログラムのモデルの 1 つは、SLDNF 解決の動作を正しく表すという意味で特別です。そのモデルを特別にする数学的特性は何でしょうか? この質問に対する答えは、安定したモデルの定義によって提供されます。

論理プログラムにおける否定の意味は、非単調推論の 2 つの理論、つまり自己認識論理とデフォルト論理に密接に関連しています。これらの関係の発見は、安定したモデル意味論の発明に向けた重要なステップでした。

自己認識論理の構文では、真実と既知のものを区別できる様相演算子を使用します。Michael Gelfond [1987] は、ルールの本体を「知られていない」と読み、否定を含むルールを自己認識論理の対応する式として理解することを提案しました。安定したモデル意味論は、その基本形式では、自己認識論理への明示的な参照を回避するこのアイデアを再定式化したものと考えることができます。 ${\displaystyle \operatorname {not} p}$${\displaystyle p}$

デフォルト論理では、デフォルトは推論規則に似ていますが、前提と結論の他に正当化と呼ばれる式のリストが含まれています。デフォルトは、その正当化が現在知られているものと一貫しているという仮定の下で結論を導き出すために使用できます。Nicole BidoitとChristine Froidevaux [1987]は、規則本体の否定されたアトムを正当化として扱うことを提案しました。たとえば、規則

${\displaystyle s\leftarrow p,\operatorname {not} q}$

は、一貫していると仮定して導出できるデフォルトとして理解できます。安定したモデルのセマンティクスでも同じ考え方が使われていますが、デフォルトのロジックを明示的に参照するわけではありません。 ${\displaystyle s}$${\displaystyle p}$${\displaystyle \neg q}$

[Gelfond and Lifschitz, 1988]から引用した以下の安定モデルの定義では、2つの慣例が用いられている。まず、真理値の割り当ては、値Tを取得する原子の集合と同一視される。例えば、真理値の割り当ては、

は集合 と同一視されます。この規則により、集合の包含関係を使用して真理の割り当てを相互に比較できます。すべての真理の割り当てのうち最小のものは、すべての原子を偽にするものです。最大の真理の割り当ては、すべての原子を真にします。 ${\displaystyle \{p,s\}}$${\displaystyle \emptyset}$

第二に、変数を含む論理プログラムは、そのルールのすべての基本インスタンスの集合、つまり、プログラムのルール内の変数を変数のない用語にあらゆる可能な方法で置き換えた結果の省略形として見なされます。たとえば、偶数の論理プログラミング定義は、

${\displaystyle \operatorname {even} (0)}$

${\displaystyle \operatorname {even} (s(X))\leftarrow \operatorname {not} \operatorname {even} (X)}$

このプログラム中のXを基底項に 置き換えた結果として理解される。

${\displaystyle 0,s(0),s(s(0)),\dots .}$

あらゆる方法で。その結果、無限の地上プログラムが生まれました

${\displaystyle \operatorname {even} (0)}$

${\displaystyle \operatorname {even} (s(0))\leftarrow \operatorname {not} \operatorname {even} (0)}$

${\displaystyle \operatorname {even} (s(s(0)))\leftarrow \operatorname {not} \operatorname {even} (s(0))}$

${\displaystyle \dots }$

Pを次の形式の規則の集合と する。

${\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

ここで、 は基底原子です。Pが否定を含まない場合 (プログラムのすべてのルールで)、定義により、Pの唯一の安定したモデルは、集合包含に対して最小のモデルです。^[1] (否定のないプログラムには、正確に 1 つの最小モデルがあります。) この定義を否定を含むプログラムの場合に拡張するには、次のように定義される縮約の補助概念が必要です。 ${\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}$${\displaystyle n=0}$

基底原子の任意の集合Iに対して、 Iに対するPの縮約は、 Pから、その本体の 原子のうち少なくとも1つが${\displaystyle C_{i}}$

${\displaystyle B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

Iに属し、残りのすべてのルールの本体から部分を削除します。 ${\displaystyle \operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

I がPのIに対する縮約の安定モデルである場合、IはPの安定モデルであると言います。(縮約には否定が含まれていないため、その安定モデルはすでに定義されています。)「安定モデル」という用語が示すように、Pのすべての安定モデルはPのモデルです。

これらの定義を説明するために、プログラムの安定したモデルである ことを確認しましょう。${\displaystyle \{p,s\}}$

${\displaystyle p}$

${\displaystyle r\leftarrow p,q}$

${\displaystyle s\leftarrow p,\operatorname {not} q.}$

このプログラムの相対的な削減は ${\displaystyle \{p,s\}}$

${\displaystyle p}$

${\displaystyle r\leftarrow p,q}$

${\displaystyle s\leftarrow p.}$

(実際、 なので、部分 を削除することでプログラムから縮約が得られます) 縮約の安定モデルは です。(実際、この原子の集合は縮約のすべての規則を満たし、同じ特性を持つ適切な部分集合はありません。) したがって、縮約の安定モデルを計算した後、開始時と同じ集合に到達しました。したがって、その集合は安定モデルです。 ${\displaystyle q\not \in \{p,s\}}$${\displaystyle \operatorname {not} q.}$${\displaystyle \{p,s\}}$${\displaystyle \{p,s\}}$

同じ方法で原子を構成する他の15セットを調べると、このプログラムには他の安定したモデルがないことがわかります。たとえば、プログラムの に対する縮約は次のようになります。 ${\displaystyle p,q,r,s}$${\displaystyle \{p,q,r\}}$

${\displaystyle p}$

${\displaystyle r\leftarrow p,q.}$

縮約の安定モデルは であり、これは最初の セットとは異なります。${\displaystyle \{p\}}$${\displaystyle \{p,q,r\}}$

否定を含むプログラムには、安定モデルが多数存在する場合もあれば、全く存在しない場合もある。例えば、次のプログラム

${\displaystyle p\leftarrow \operatorname {not} q}$

${\displaystyle q\leftarrow \operatorname {not} p}$

には2つの安定したモデルがあります。1ルールプログラム ${\displaystyle \{p\}}$${\displaystyle \{q\}}$

${\displaystyle p\leftarrow \operatorname {not} p}$

安定したモデルはありません。

安定モデルセマンティクスを否定が存在する場合のPrologの動作の説明と考えると、一意の安定モデルを持たないプログラムは不十分であると判断できます。つまり、Prolog スタイルのクエリ回答の明確な仕様を提供しないからです。たとえば、上記の 2 つのプログラムは Prolog プログラムとしては妥当ではありません。SLDNF 解決はこれらのプログラムでは終了しません。

しかし、アンサーセットプログラミングで安定したモデルを使用すると、そのようなプログラムに対する別の視点が得られます。そのプログラミングパラダイムでは、特定の検索問題はロジックプログラムによって表現され、プログラムの安定したモデルがソリューションに対応します。すると、多くの安定したモデルを持つプログラムは多くのソリューションを持つ問題に対応し、安定したモデルを持たないプログラムは解決不可能な問題に対応します。たとえば、8 つのクイーンのパズルには 92 のソリューションがあります。アンサーセットプログラミングを使用してこれを解くには、92 の安定したモデルを持つロジックプログラムでエンコードします。この観点から、正確に 1 つの安定したモデルを持つロジックプログラムは、代数で正確に 1 つの根を持つ多項式のように、アンサーセットプログラミングではむしろ特別です。

このセクションでは、上記の安定モデルの定義と同様に、論理プログラムとは次のような形式のルールの集合を意味します。

${\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

基底原子はどこにありますか。 ${\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}$

ヘッドアトム

アトムA が論理プログラムPの安定したモデルに属する場合、A はPの規則の 1 つの先頭になります。

ミニマリズム

論理プログラムPの任意の安定モデルは、集合包含に関連するPのモデルの中で最小です。

反鎖特性

IとJが同じ論理プログラムの安定モデルである場合、 I はJの適切なサブセットではありません。言い換えると、プログラムの安定モデルの集合は反連鎖です。

NP完全性

有限基底論理プログラムが安定したモデルを持つかどうかをテストすることはNP 完全です。

有限基底プログラムの安定モデルは、プログラム自体のモデルであるだけでなく、その完了のモデルでもあります[Marek and Subrahmanian, 1989]。しかし、逆は真ではありません。たとえば、1ルールプログラムの完了は

${\displaystyle p\leftarrow p}$

はトートロジー です。このトートロジーのモデルは の安定したモデルですが、そのもう 1 つのモデルはそうではありません。François Fages [1994] は、このような反例を排除し、プログラムの完了のすべてのモデルの安定性を保証する論理プログラムに関する構文条件を発見しました。彼の条件を満たすプログラムは、タイトと呼ばれます。 ${\displaystyle p\leftrightarrow p}$${\displaystyle \emptyset }$${\displaystyle p\leftarrow p}$${\displaystyle \{p\}}$

Fangzhen LinとYuting Zhao[2004]は、非タイトプログラムの補完をより強力にして、その非安定モデルをすべて除去する方法を示しました。彼らが補完に追加した式はループ式と呼ばれます。

論理プログラムの整基礎モデルは、すべての基底原子を 3 つの集合、つまり真、偽、未知に分割します。 の整基礎モデルで原子が真である場合、その原子は のすべての安定モデルに属します。一般に、逆は成り立ちません。たとえば、プログラム ${\displaystyle P}$${\displaystyle P}$

${\displaystyle p\leftarrow \operatorname {not} q}$

${\displaystyle q\leftarrow \operatorname {not} p}$

${\displaystyle r\leftarrow p}$

${\displaystyle r\leftarrow q}$

には 2 つの安定したモデルがあり、と があります。は両方に属していますが、十分に根拠のあるモデルにおけるその値は不明です。 ${\displaystyle \{p,r\}}$${\displaystyle \{q,r\}}$${\displaystyle r}$

さらに、プログラムの well-founded モデルでアトムが偽である場合、そのアトムはどの安定モデルにも属しません。したがって、論理プログラムの well-founded モデルは、安定モデルの交差の下限とそれらの和集合の上限を提供します。

知識表現の観点からは、基底原子の集合は完全な知識の状態の記述として考えることができます。集合に属する原子は真であることが分かっており、集合に属さない原子は偽であることが分かっています。不完全な可能性のある知識の状態は、一貫性があるが不完全な可能性のあるリテラルの集合を使用して記述できます。原子が集合に属さず、その否定も集合に属さない場合、真か偽か は分かりません。${\displaystyle p}$${\displaystyle p}$

論理プログラミングの文脈では、この考え方は、上で議論した失敗としての否定と、ここで で表される強い否定の2種類の否定を区別する必要性を生じさせる。^[2] 2種類の否定の違いを示す次の例は、ジョン・マッカーシーによるものである。スクールバスは、列車が近づいていないという条件で線路を横切ることができる。列車が近づいているかどうかが必ずしもわからない場合、失敗としての否定を使用する規則は ${\displaystyle \sim }$

${\displaystyle {\hbox{Cross}}\leftarrow {\hbox{not Train}}}$

は、この考えを適切に表現していません。列車が近づいているという情報がない場合、横断しても大丈夫だと言っています。本文で強い否定を使用する、より弱いルールの方が望ましいです。

${\displaystyle {\hbox{Cross}}\leftarrow \,\sim {\hbox{Train}}.}$

電車が来ていないことが分かっていれば渡っても大丈夫だそうです。

安定モデルの理論に強い否定を組み込むために、GelfondとLifschitz [1991]は、各表現、を規則 ${\displaystyle A}$${\displaystyle B_{i}}$${\displaystyle C_{i}}$

${\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

原子または強い否定記号が前に付いた原子のいずれかになります。安定したモデルの代わりに、この一般化では、原子と強い否定記号が前に付いた原子の両方を含む可能性のある回答セットを使用します。

代替アプローチ [Ferraris and Lifschitz, 2005] では、強い否定をアトムの一部として扱い、安定モデルの定義を変更する必要はありません。この強い否定の理論では、正と負の2 種類のアトムを区別し、各負のアトムは の形式( は正のアトム)の式であると想定します。アトムの集合は、アトムの「補完的な」ペアを含まない場合、コヒーレントと呼ばれます。プログラムのコヒーレントな安定モデルは、[Gelfond and Lifschitz, 1991] の意味で、その一貫した回答集合と同一です。 ${\displaystyle {\sim }A}$${\displaystyle A}$${\displaystyle A,{\sim }A}$

例えば、プログラム

${\displaystyle p\leftarrow \operatorname {not} q}$

${\displaystyle q\leftarrow \operatorname {not} p}$

${\displaystyle r}$

${\displaystyle {\sim }r\leftarrow \operatorname {not} p}$

には と の2 つの安定モデルがあります。最初のモデルはコヒーレントですが、2 番目のモデルは原子と原子の両方を含んでいるためコヒーレントではありません。 ${\displaystyle \{p,r\}}$${\displaystyle \{q,r,{\sim }r\}}$${\displaystyle r}$${\displaystyle {\sim }r}$

[Gelfond and Lifschitz, 1991]によれば、述語の閉世界仮定は、次の規則で表現できる。 ${\displaystyle p}$

${\displaystyle \sim p(X_{1},\dots ,X_{n})\leftarrow \operatorname {not} p(X_{1},\dots ,X_{n})}$

（その関係は、それが成り立つという証拠がなければ、 タプルには成り立ちません）。例えば、プログラムの安定モデル${\displaystyle p}$${\displaystyle X_{1},\dots ,X_{n}}$

${\displaystyle p(a,b)}$

${\displaystyle p(c,d)}$

${\displaystyle \sim p(X,Y)\leftarrow \operatorname {not} p(X,Y)}$

2つの正の原子からなる

${\displaystyle p(a,b),p(c,d)}$

14個の負の原子

${\displaystyle \sim p(a,a),{\sim }p(a,c),\dots }$

つまり、から形成される他のすべての正の基底原子の強い否定です。 ${\displaystyle p,a,b,c,d}$

強い否定を持つ論理プログラムでは、一部の述語に閉世界仮定規則を含め、他の述語を開世界仮定の領域に残すことができます。

安定モデルの意味論は、上で議論した「伝統的な」ルールの集合以外の多くの種類の論理プログラムに一般化されている。

${\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

はアトムです。簡単な拡張により、プログラムに制約（空のヘッドを持つルール）を含めることができます。 ${\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}$

${\displaystyle \leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}.}$

伝統的な規則は、コンマを接続詞、記号を否定と同一視し、含意を逆に記述したものとして扱うことに同意すれば、命題式の代替表記法として見ることができることを思い出してください。この規則を制約に拡張するには、制約をその本体に対応する式の否定と同一視します。 ${\displaystyle \land }$${\displaystyle \operatorname {not} }$${\displaystyle \neg }$${\displaystyle F\leftarrow G}$${\displaystyle G\rightarrow F}$

${\displaystyle \neg (B_{1}\land \cdots \land B_{m}\land \neg C_{1}\land \cdots \land \neg C_{n}).}$

これで、安定モデルの定義を制約のあるプログラムに拡張できます。従来のプログラムの場合と同様に、安定モデルを定義するには、否定を含まないプログラムから始めます。このようなプログラムは矛盾している可能性があります。その場合、安定モデルがないと言います。このようなプログラムが矛盾していない場合、には一意の最小モデルがあり、そのモデルが の唯一の安定モデルであると見なされます。 ${\displaystyle P}$${\displaystyle P}$${\displaystyle P}$

次に、制約のある任意のプログラムの安定したモデルが、従来のプログラムの場合と同じ方法で形成された縮約を使用して定義されます (上記の安定したモデルの定義を参照)。 に対するの縮約に安定したモデルがあり、その安定したモデルがに等しい場合、アトムのセットは制約のあるプログラムの安定したモデルです。 ${\displaystyle I}$${\displaystyle P}$${\displaystyle P}$${\displaystyle I}$${\displaystyle I}$

従来のプログラムについて上で述べた安定したモデルセマンティクスの特性は、制約が存在する場合にも当てはまります。

制約は、解答セットプログラミングにおいて重要な役割を果たします。これは、制約を論理プログラムに追加すると、の安定モデルのコレクションに非常に単純な方法で影響を与えるためです。つまり、制約に違反する安定モデルが削除されます。言い換えると、制約 と任意の制約 を持つ任意のプログラムについて、 の安定モデルはを満たすの安定モデルとして特徴付けることができます。 ${\displaystyle P}$${\displaystyle P}$${\displaystyle P}$${\displaystyle C}$${\displaystyle P\cup \{C\}}$${\displaystyle P}$${\displaystyle C}$

選言規則では、ヘッドは複数の原子の選言である場合があります。

${\displaystyle A_{1};\dots ;A_{k}\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

（セミコロンは、選言 の代替表記法と見なされます）。従来のルールは、制約は に対応します。安定モデルの意味論を選言プログラムに拡張するために [Gelfond and Lifschitz, 1991]、まず、各ルールで否定（ ）がない場合、プログラムの安定モデルはその最小モデルであると定義します。選言プログラムの縮約の定義は、以前と同じです。が に対するの縮約の安定モデルである場合、アトムの集合はの安定モデルです。 ${\displaystyle \lor }$${\displaystyle k=1}$${\displaystyle k=0}$${\displaystyle n=0}$${\displaystyle I}$${\displaystyle P}$${\displaystyle I}$${\displaystyle P}$${\displaystyle I}$

例えば、集合は選言的プログラムの安定モデルである。 ${\displaystyle \{p,r\}}$

${\displaystyle p;q}$

${\displaystyle r\leftarrow \operatorname {not} q}$

これは縮約の2つの最小モデルのうちの1つである。

${\displaystyle p;q}$

${\displaystyle r.}$

上記のプログラムには、もう 1 つの安定したモデルがあります。 ${\displaystyle \{q\}}$

従来のプログラムの場合と同様に、選言プログラムの任意の安定モデルの各要素は、 の規則の 1 つの先頭に出現するという意味において、の先頭アトムです。従来の場合と同様に、選言プログラムの安定モデルは最小であり、反連鎖を形成します。有限の選言プログラムに安定モデルがあるかどうかをテストすることは、-完全です[Eiter および Gottlob、1993]。 ${\displaystyle P}$${\displaystyle P}$${\displaystyle P}$${\displaystyle \Sigma _{2}^{\rm {P}}}$

規則、さらには選言規則は、任意の命題式と比較すると、かなり特殊な構文形式を持っています。各選言規則は本質的には含意であり、その前件部(規則の本体) はリテラルの連言であり、後件部(ヘッド) はアトムの選言です。David Pearce [1997] と Paolo Ferraris [2005] は、安定モデルの定義を任意の命題式の集合に拡張する方法を示しました。この一般化は、回答集合プログラミングに応用できます。

ピアースの定式化は、安定モデルの元の定義とはかなり異なっています。縮約の代わりに、均衡論理、つまりクリプキ モデルに基づく非単調論理のシステムを参照しています。一方、フェラーリスの定式化は縮約に基づいていますが、縮約を構築するプロセスは上記のものとは異なります。命題式の集合に対して安定モデルを定義する 2 つのアプローチは、互いに同等です。

[Ferraris, 2005] によれば、アトムの集合に対する命題式の縮約は、 が満たさない各極大部分式を論理定数(偽) に置き換えることによってから得られる式です。に対する命題式の集合の縮約は、から に対するすべての式の縮約で構成されます。 選言プログラムの場合と同様に、に対するの縮約のモデルの中で が最小 (集合包含に関して) である場合、アトムの集合はの安定モデルであると言えます。 ${\displaystyle F}$${\displaystyle I}$${\displaystyle F}$${\displaystyle I}$${\displaystyle \bot }$${\displaystyle P}$${\displaystyle I}$${\displaystyle P}$${\displaystyle I}$${\displaystyle I}$${\displaystyle P}$${\displaystyle I}$${\displaystyle P}$${\displaystyle I}$

例えば、集合の縮約

${\displaystyle \{p,p\land q\rightarrow r,p\land \neg q\rightarrow s\}}$

相対的に​ ${\displaystyle \{p,s\}}$

${\displaystyle \{p,\bot \rightarrow \bot ,p\land \neg \bot \rightarrow s\}.}$

は縮約のモデルであり、その集合の適切な部分集合は縮約のモデルではないため、は与えられた式の集合の安定したモデルです。 ${\displaystyle \{p,s\}}$${\displaystyle \{p,s\}}$

は、元の定義の意味で、論理プログラミング表記法で記述された同じ式の安定したモデルでもあることがわかりました。これは一般的な事実の一例です。つまり、従来のルールのセット (に対応する式) に適用すると、Ferraris による安定したモデルの定義は元の定義と同等になります。より一般的には、制約のあるプログラムや選言プログラムについても同じことが言えます。 ${\displaystyle \{p,s\}}$

プログラムの任意の安定モデルのすべての要素が のヘッド アトムであるという定理は、ヘッド アトムを次のように定義すれば、命題式のセットに拡張できます。の式内のの少なくとも 1 つの出現が否定の範囲内にも含意の前提にもない場合、アトムは命題式のセットのヘッド アトムです。(ここでは、同値は基本接続詞ではなく略語として扱われると仮定します。) ${\displaystyle P}$${\displaystyle P}$${\displaystyle A}$${\displaystyle P}$${\displaystyle A}$${\displaystyle P}$

伝統的なプログラムの安定モデルの最小性と反連鎖性は、一般的な場合には成り立たない。例えば、（シングルトン集合は）次の式から構成される。

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

には 2 つの安定モデル、と があります。後者は最小ではなく、前者の適切なスーパーセットです。 ${\displaystyle \emptyset }$${\displaystyle \{p\}}$

命題式の有限集合が安定したモデルを持つかどうかをテストすることは、選言プログラムの場合と同様に、 -完全です。${\displaystyle \Sigma _{2}^{\rm {P}}}$

• 回答セットプログラミング
• 論理プログラミング
• 失敗としての否定

• Bidoit, N.; Froidevaux, C. (1987) 「ミニマリズムはデフォルト ロジックとサーカムスクリプションを包含する」Proceedings: Symposium on Logic in Computer Science、ニューヨーク州イサカ、1987 年 6 月 22 ～ 25 日。IEEE Computer Society Press。pp. 89 ～97。ISBN 978-0-8186-0793-687CH2464-6.
• Eiter, T.; Gottlob, G. (1993)。「選言論理プログラミングの計算量結果と非単調論理への応用」。ILPS '93: 1993 年国際論理プログラミングシンポジウムの議事録。MIT プレス。266 ～ 278 ページ。ISBN 978-0-262-63152-5。
• van Emden, M.; Kowalski, R. (1976). 「プログラミング言語としての述語論理の意味論」(PDF) . Journal of the ACM . 23 (4): 733–742. CiteSeerX  10.1.1.64.9246 . doi :10.1145/321978.321991. S2CID  11048276.
• Fages, F. (1994). 「クラークの完備化の一貫性と安定モデルの存在」.コンピュータサイエンスにおける論理方法ジャーナル. 1 : 51–60. CiteSeerX  10.1.1.48.2157 .
• Ferraris, P. (2005). 「命題理論の解答セット」.論理プログラミングと非単調推論. LPNMR 2005 . コンピュータサイエンスの講義ノート. Vol. 3662. Springer. pp. 119–131. CiteSeerX  10.1.1.129.5332 . doi :10.1007/11546207_10. ISBN 978-3-540-31827-9。
• Ferraris, P.; Lifschitz, V. (2005)。「解答セットプログラミングの数学的基礎」。私たちは彼らに見せます! Dov Gabbay を称えるエッセイ。King's College Publications。pp. 615–664。CiteSeerX  10.1.1.79.7622。
• Gelfond, M. (1987). 「階層化された自己認識理論について」(PDF) . AAAI'87: 第 6 回人工知能全国会議の議事録. pp. 207–211. ISBN 978-0-934613-42-2。
• Gelfond, M.; Lifschitz, V. (1988)。「論理プログラミングのための安定したモデル意味論」。第 5 回国際論理プログラミング会議 (ICLP) の議事録。MIT プレス。pp. 1070–80。ISBN 978-0-262-61054-4。
• Gelfond, M.; Lifschitz, V. (1991). 「論理プログラムと選言データベースにおける古典的な否定」. New Generation Computing . 9 (3–4): 365–385. CiteSeerX  10.1.1.49.9332 . doi :10.1007/BF03037169. S2CID  13036056.
• Hanks, S.; McDermott, D. (1987). 「非単調論理と時間的投影」.人工知能. 33 (3): 379–412. doi :10.1016/0004-3702(87)90043-9.
• Lin, F.; Zhao, Y. (2004). 「ASSAT: SAT ソルバーによる論理プログラムの解答セットの計算」(PDF) .人工知能. 157 (1–2): 115–137. doi :10.1016/j.artint.2004.04.004. S2CID  514581.
• Marek, V.; Subrahmanian, VS (1989)。「論理プログラムの意味論と非単調推論の関係」。論理プログラミング: 第 6 回国際会議の議事録。MIT プレス。pp. 600–617。ISBN 978-0-262-62065-9。
• Pearce, D. (1997)。「安定したモデルと回答セットの新しい論理的特徴付け」(PDF)。論理プログラミングの非単調拡張。人工知能の講義ノート。第 1216 巻。pp. 57–70。doi : 10.1007/ BFb0023801。ISBN 978-3-540-68702-3。
• Reiter, R. (1980). 「デフォルト推論のロジック」(PDF) .人工知能. 13 (1–2): 81–132. doi :10.1016/0004-3702(80)90014-4.