イェール大学銃乱射事件

Problem in formal logic

イェール銃乱射事件問題（イェールしゅうしんじけん）は、形式状況論理における難問またはシナリオであり、フレーム問題に対する初期の論理的解決法が失敗する問題である。この問題の名前は、イェール大学で働いていたスティーブ・ハンクスとドリュー・マクダーモットという発明者がこの問題を考案した際に提唱したシナリオに由来する。このシナリオでは、フレッド（後に七面鳥であると特定される）は最初は生きており、銃は最初は弾が抜かれている。銃に弾を込め、少し待ってからフレッドに向けて発砲すると、フレッドは死亡すると予想される。しかし、この状況の変化を最小化するように論理において慣性を形式化すると、弾を込め、待ち、発砲した後にフレッドが死亡していることを一意に証明できなくなる。ある解決法ではフレッドは実際に死亡するが、別の（これも論理的に正しい）解決法では、銃は不思議なことに弾が抜かれ、フレッドは生き残る。

技術的には、このシナリオは2つのフルーエント（フルーエントとは、時間の経過とともに真理値が変化する条件）とで記述されます。最初は、最初の条件は真で、2番目の条件は偽です。その後、銃に弾が込められ、しばらく時間が経過し、銃が発砲されます。このような問題は、4つの時点、、、、を考慮し、などのすべてのフルーエントを時間に依存する述語に変換することで、論理的に形式化できます。エール大学銃乱射事件の問題の記述を論理的に直接形式化すると、次のようになります。 $alive$ $loaded$ $0$ $1$ $2$ $3$ $alive$ $alive(t)$

alive(0)

\neg loaded(0)

true\rightarrow loaded(1)

loaded(2)\rightarrow \neg alive(3)

最初の2つの式は初期状態を表します。3番目の式は、時刻における銃の装填の効果を定式化します。4番目の式は、時刻におけるフレッドへの射撃の効果を定式化します。これは、アクション名を無視し、アクションが実行された時点におけるアクションの効果を直接指定する簡略化された定式化です。詳細については、状況計算を参照してください。 $1$ $2$

上記の式は、既知の事実を直接的に形式化したものではあるが、ドメインを正しく特徴付けるには不十分である。確かに、銃が撃たれる前にフレッドが死ぬと信じる理由はないが、はこれらすべての式と矛盾しない。問題は、上記の式がアクションの効果のみを含み、アクションによって変化しないすべてのフルーエントが同じままであることを指定していないことである。言い換えれば、銃を装填することはの値のみを変化させ、の値は変化させないという暗黙の仮定を形式化するために、式を追加する必要がある。アクションによって条件が変化しない限り条件は変化しないという明白な事実を述べる式が多数必要となることは、フレーム問題として知られている。 $\neg alive(1)$ $alive(0)\equiv alive(1)$ $loaded$ $alive$

フレーム問題に対する初期の解決策は、変化の最小化に基づいていました。言い換えれば、シナリオは上記の式（アクションの効果のみを規定する）と、時間経過に伴う流暢性の変化が可能な限り最小であるという仮定によって定式化されます。その根拠は、上記の式はアクションのすべての効果が発生することを強制するのに対し、最小化は変化をアクションに起因するものだけに限定するべきであるということです。

イェール大学銃乱射事件のシナリオでは、変化が最小限に抑えられた流暢性の評価として次のようなものが考えられます。

$alive(0)$	$alive(1)$	$alive(2)$	$\neg alive(3)$
$\neg loaded(0)$	$loaded(1)$	$loaded(2)$	$loaded(3)$

これは期待される解です。2つの流動的な変化が含まれています。1番目の時点では真になり、3番目の時点では偽になります。次の評価も上記のすべての式を満たします。 $loaded$ $alive$

$alive(0)$	$alive(1)$	$alive(2)$	$alive(3)$
$\neg loaded(0)$	$loaded(1)$	$\neg loaded(2)$	$\neg loaded(3)$

この評価では、まだ 2 つの変更のみがあります。つまり、時刻 1 では真になり、時刻 2 では偽になります。結果として、時刻 2で偽であることを説明する正当な理由はありませんが、この評価は状態の進化の有効な説明であると考えられます。変更の最小化が間違った解決につながるという事実は、イェール射撃問題が導入された動機です。 $loaded$ $loaded$

イェール大学銃乱射事件は、動的なシナリオを論理的に形式化する上で大きな障害と考えられてきましたが、その解決策は1980年代後半から知られていました。解決策の一つは、アクションの指定において述語補完を用いるというものです。この解決策では、銃乱射によってフレッドが死亡するという事実は、前提条件aliveとloadedによって形式化され、その結果としてalive の値が変化します（以前はalive が真であったため、これはaliveが偽になることに対応します）。この含意をif and only if文に変換することで、銃乱射事件の影響が正しく形式化されます。（複数の含意が関係する場合、述語補完はより複雑になります。）

Erik Sandewallが提案した解決策は、新たな閉塞条件を組み込むというものでした。これは、fluent の「変更許可」を形式化するものです。fluent を変更する可能性のあるアクションの効果は、fluent が新しい値を持ち、閉塞が（一時的に）真になることです。最小化されるのは、変更の集合ではなく、閉塞が真である集合です。閉塞が真でない限り fluent は変更されないという別の制約を追加することで、この解決策は完成します。

イェール大学銃乱射事件のシナリオは、ライター版の状況計算、流暢性計算、および行動記述言語によっても正しく形式化されています。

2005年、イェール大学銃乱射事件のシナリオを初めて記述した1985年の論文がAAAIクラシック論文賞を受賞しました。この事例は既に解決済みの問題であるにもかかわらず、近年の研究論文では依然として時折言及されており、問題として提示されるのではなく、説明例として（例えば、行動に関する推論のための新しいロジックの構文を説明するために）用いられています。

参照

参考文献

M. GelfondとV. Lifschitz (1993). 論理プログラムによる動作と変化の表現. Journal of Logic Programming , 17:301–322.
S. ハンクス、D. マクダーモット (1987). 非単調論理と時間的射影.人工知能, 33(3):379–412.
J. マッカーシー(1986). 限界制約の常識的知識の形式化への応用.人工知能, 28:89–116.
T. ミッチェルとH. レベスク (2006). 2005年AAAIクラシック論文賞. AI Magazine, 26(4):98–99.
R. ライター (1991). 状況計算におけるフレーム問題：単純な解（場合によっては）と目標回帰の完全性の結果．ウラジミール・リフシッツ編著『人工知能と計算の数学的理論：ジョン・マッカーシー記念論文集』 359-380ページ．アカデミック・プレス，ニューヨーク．
E. サンデウォール (1994). 『特徴と流暢さ』オックスフォード大学出版局.