イェール大学銃撃事件

イェール射撃問題は、形式的状況論理における難問またはシナリオであり、フレーム問題に対する初期の論理的解法では解決できない問題である。この問題の名前は、考案者であるスティーブ・ハンクスとドリュー・マクダーモットが、イェール大学で研究していた際に提案したシナリオに由来する。このシナリオでは、フレッド（後に七面鳥と判明）は最初は生きており、銃は最初は弾が入っていない。銃に弾を装填し、しばらく待ってからフレッドに向けて発砲すれば、フレッドは死ぬと予想される。しかし、この状況の変化を最小化することで慣性を論理的に形式化すると、弾を装填し、待ってから発砲した後にフレッドが死んだことを一意に証明することはできない。ある解法では、フレッドは実際に死ぬ。別の（これも論理的に正しい）解法では、銃は不可解にも弾が入っておらず、フレッドは生き残る。

技術的には、このシナリオは2つのフルーエント（フルーエントとは、時間の経過とともに真偽値が変化する可能性のある条件）によって記述されます。${\displaystyle 生きている}$そして${\displaystyle loaded}$最初は、最初の条件は真で、2番目の条件は偽です。次に、銃に弾が装填され、時間が経過し、銃が発射されます。このような問題は、4つの時点を考慮することで論理的に定式化できます。${\displaystyle 0}$、${\displaystyle 1}$、${\displaystyle 2}$、 そして${\displaystyle 3}$、そしてあらゆる流暢なものを${\displaystyle 生きている}$述語に${\displaystyle alive(t}$時間によって異なる。イェール射撃問題の論理的定式化は、次のようになる。

${\displaystyle alive(0)}$

${\displaystyle \neg loaded(0)}$

${\displaystyle true\rightarrow loaded(1)}$

${\displaystyle loaded(2)\rightarrow \neg alive(3)}$

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

上記の式は既知の事実を直接形式化したものであるが、領域を正しく特徴付けるには不十分である。実際、${\displaystyle \neg alive(1)}$フレッドが銃撃前に死亡すると考える理由はないが、これはこれらの公式すべてと矛盾しない。問題は、上記の公式には行動の影響のみが含まれており、行動によって変化しないすべての流体が同じままであるとは明記されていないことである。言い換えれば、公式は${\displaystyle alive(0)\equiv alive(1}$銃を装填すると値が変わるという暗黙の仮定を形式化するために追加する必要がある。${\displaystyle loaded}$そしてその価値ではない${\displaystyle 生きている}$行動によって状況が変わらない限り状況は変わらないという明白な事実を述べる多数の公式が必要となることは、枠組み問題として知られています。

フレーム問題に対する初期の解決策は、変化を最小限に抑えることに基づいていた。言い換えれば、シナリオは上記の式（行動の効果のみを指定する式）と、時間経過に伴う流体の変化が可能な限り最小限であるという仮定によって定式化される。その根拠は、上記の式は行動のすべての効果が発生することを強制する一方、最小化は変化を行動によるものだけに限定するはずだという点にある。

イェール大学銃乱射事件のシナリオにおいて、変化が最小限に抑えられる流速を評価する一つの方法として、以下のようなものが考えられる。

これは期待される解決策です。以下の2つのスムーズな変更が含まれています。${\displaystyle loaded}$時刻 1 で真となり、${\displaystyle 生きている}$時刻 3 で偽となる。以下の評価も上記のすべての式を満たす。

今回の評価では、変更点はわずか2点のみです。${\displaystyle loaded}$時刻 1 では真となり、時刻 2 では偽となる。結果として、この評価は状態の進化の有効な記述とみなされるが、それを説明する有効な理由はない。${\displaystyle loaded}$時刻2において偽である。変化の最小化が誤った解につながるという事実が、イェール射撃問題導入の動機となっている。

イェール射撃問題は、動的なシナリオを形式化するための論理の使用における深刻な障害と考えられてきたが、その解決策は1980年代後半から知られている。一つの解決策は、行動の仕様に述語補完を用いるものである。この解決策では、射撃によってフレッドが死亡するという事実は、前提条件「生存」と「装填済み」によって形式化され、結果として「生存」の値が変化する（以前は「生存」が真であったため、これは「生存」が偽になることに対応する）。この含意をif and only if文に変換することで、射撃の効果が正しく形式化される。（複数の含意が関係する場合、述語補完はより複雑になる。）

エリック・サンデウォールが提案した解決策は、流暢な表現に対する「変更の許可」を形式化する、新たなオクルージョン条件を導入することだった。流暢な表現を変更する可能性のあるアクションの効果は、流暢な表現が新しい値を持つことと、オクルージョンが（一時的に）真になることである。最小化されるのは変更の集合ではなく、オクルージョンが真となる集合である。オクルージョンが真でない限り流暢な表現は変更されないという別の制約を加えることで、この解決策は完成する。

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

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

• 限定（論理）
• フレーム問題
• 状況計算

• M. GelfondおよびV. Lifschitz (1993). 論理プログラムによる動作と変化の表現. Journal of Logic Programming , 17:301–322.
• S. ハンクスと D. マクダーモット (1987). 非単調論理と時間的射影.人工知能, 33(3):379–412.
• J. McCarthy (1986). 常識的知識の形式化への限定の応用。人工知能、28:89–116。
• T. Mitchell および H. Levesque (2006). 2005 年 AAAI クラシック論文賞。「AI Magazine」、26(4):98–99。
• R. Reiter (1991). 状況計算におけるフレーム問題：簡単な解決策（場合による）と目標回帰の完全性結果。Vladimir Lifschitz 編『人工知能と計算の数学的理論：John McCarthy 教授記念論文集』、359-380 ページ。Academic Press、ニューヨーク。
• E. サンデウォール (1994).特徴と流暢性. オックスフォード大学出版局.