| dbo:abstract
|
- イェール射撃問題（イェールしゃげきもんだい、英: Yale shooting problem）とは、形式的状況分析におけるあるシナリオであり、フレーム問題に対する初期の論理学的アプローチが解けなかった難問である。名称はこの問題の発案者、がイェール大学に所属していたことにちなむ。シナリオは次のとおりである。最初の時点で、フレッド（後に七面鳥であるとされた）は生きていて、銃には弾丸が装填されていないものとする。銃に弾丸を装填し、少し待機し、フレッドに向けて発砲すれば、フレッドは殺されるものと想定される。ところが、変化が最小化されるべく論理学的な定式化がなされたとすると（慣性（inertia）の表現）、装填・待機・発砲という一連の動作の後にフレッドが死亡しているという結論が必ずしも導かれない。一つの帰結は、フレッドが実際に死亡しているというものである。もう一つの（論理的には正しい）帰結は、銃から弾丸が不思議と抜かれていて、フレッドは生存しているというものである（本項において「発砲（shooting）」は空砲の場合も含む）。 技術的には、このシナリオは2つの（時間の経過とともに真理値が変化し得る項）： と で記述できる。最初、前者は真で後者は偽である。その後弾丸が装填され、しばし時間が経過し、銃が発砲される。これを論理学的に定式化するには , , , という4つの時刻と、時刻に依存した述語 , を考えればよい。直接的に定式化すると次のようになる： 最初の2つの論理式は初期状態を表す。3番目の論理式は時刻0で弾丸が装填されることを表す。4番目の論理式は時刻2でフレッドに向けて銃が発砲されること及びその帰結を表す。これは行為の名称が省略され、行為の影響がその実行時刻において直接的に特定されるような、最も単純化された定式化である（詳細は（situation calculus）を参照）。 これらの論理式は事実を直接的に定式化したものであるが、シナリオを満足に記述できていない。実際、 はこれらすべての論理式と整合的であるが、銃の発砲前にフレッドが死亡すると考えなければならない理由は全くない。問題なのは、上記の定式化には行為とその帰結しか含まれておらず、「全てのフルーエント（の真理値）は行為がなされない限り変化しない」ことが明示されていない点である。言い換えれば「弾丸の装填という行為はフルーエント の値のみを変えるのであって、フルーエント の値を変えない」という暗黙の仮定を定式化するためには、追加の論理式 が必要である。「行為によって状態が変えられない限り、状態は変わらない」という明白な事実を述べるのに無数の論理式が必要となるこの問題は、フレーム問題（の一種）として知られている。 フレーム問題への初期の解決策の一つは、変化の最小化に基づくものであった。言い換えると、上記のような定式化（行為とその帰結のみの記述）に、時間経過に伴うフルーエントの変化は可能な限り少なくあるべしという仮定を追加するというものである。論理式群によって全ての行為の実行とその結果の惹起を記述し、一方で最小化によって、全ての変化は何らかの行為によって引き起こされるものに限定する、という発想である。 イェール射撃問題では、変化数が最小となるようなフルーエントへの付値の一つは次のようなものである。 これが期待される解であり、フルーエントの変化は2回である： が時刻1で真になり、 が時刻3で偽になる。 ところが次の付値も同じ条件を満たす。 この場合もフルーエントの変化は2回である： が時刻1で真になり、時刻2で偽になる。 結果的にこのような評価も状態変化の有効な記述ではあるが、しかし、時刻2で が偽になることを説明する妥当な理由は何もない。変化の最小化という制約が「誤った」解を導き得るというこの事実が、イェール射撃問題が提案される動機となった。 イェール射撃問題は動的なシナリオの形式化に論理学を用いるにあたっての深刻な障壁だと考えられてきたが、1980年代後半から解決策が知られ始めた。その一つが、動作の特定に（predicate completion）を用いるものである。この解決策によれば、「発砲がフレッドに死をもたらす」という事実は次の前提の下で定式化されている： と が真で、発生する帰結は が真理値を変えること（つまり偽になること）であること。ここでの論理包含を同値（if and only if）に変更することで、発砲の帰結が適切に定式化できる（論理包含が複数ある場合、述語完備化はもっと複雑になる）。 が提出した解決案は、新しい状態、オクルージョン（occlusion、直訳すれば包蔵）を採り入れるものである。これはフルーエントに対する「変化の許可（permission to change）」を定式化したものである。この案に従うと、フルーエントの値を変え得るようなある行為の帰結は、フルーエントが新しい値をとり、オクルージョンが（一時的に）真にされることである。最小化されるべきなのは変化の集合ではなく、真であるオクルージョンの集合である。これに「オクルージョンが真でない限り、フルーエントは値を変えない」という追加条件を補完することで、問題は解決される。 イェール射撃問題のシナリオは、版の状況計算、（fluent calculus）、（action description language,ADL）によっても適切に定式化できる。 2005年、イェール射撃問題が初めて記述された1985年の論文が に選ばれた。この問題には解決策が既に与えられているものの、最近の研究論文においてもなお言及される。問題というよりは理解に役立つ例（例えば、動作の推論のための新しい論理に関するの説明）として用いられるのである (ja)
- The Yale shooting problem is a conundrum or scenario in formal situational logic on which early logical solutions to the frame problem fail. The name of this problem derives from its inventors, and Drew McDermott, working at Yale University when they proposed it. In this scenario, Fred (later identified as a turkey) is initially alive and a gun is initially unloaded. Loading the gun, waiting for a moment, and then shooting the gun at Fred is expected to kill Fred. However, if inertia is formalized in logic by minimizing the changes in this situation, then it cannot be uniquely proved that Fred is dead after loading, waiting, and shooting. In one solution, Fred indeed dies; in another (also logically correct) solution, the gun becomes mysteriously unloaded and Fred survives. Technically, this scenario is described by two fluents (a fluent is a condition that can change truth value over time): and . Initially, the first condition is true and the second is false. Then, the gun is loaded, some time passes, and the gun is fired. Such problems can be formalized in logic by considering four time points , , , and , and turning every fluent such as into a predicate depending on time. A direct formalization of the statement of the Yale shooting problem in logic is the following one: The first two formulae represent the initial state. The third formula formalizes the effect of loading the gun at time . The fourth formula formalizes the effect of shooting at Fred at time . This is a simplified formalization in which action names are neglected and the effects of actions are directly specified for the time points in which the actions are executed. See situation calculus for details. The formulae above, while being direct formalizations of the known facts, do not suffice to correctly characterize the domain. Indeed, is consistent with all these formulae, although there is no reason to believe that Fred dies before the gun has been shot. The problem is that the formulae above only include the effects of actions, but do not specify that all fluents not changed by the actions remain the same. In other words, a formula must be added to formalize the implicit assumption that loading the gun only changes the value of and not the value of . The necessity of a large number of formulae stating the obvious fact that conditions do not change unless an action changes them is known as the frame problem. An early solution to the frame problem was based on minimizing the changes. In other words, the scenario is formalized by the formulae above (that specify only the effects of actions) and by the assumption that the changes in the fluents over time are as minimal as possible. The rationale is that the formulae above enforce all effect of actions to take place, while minimization should restrict the changes to exactly those due to the actions. In the Yale shooting scenario, one possible evaluation of the fluents in which the changes are minimized is the following one. This is the expected solution. It contains two fluent changes: becomes true at time 1 and becomes false at time 3. The following evaluation also satisfies all formulae above. In this evaluation, there are still two changes only: becomes true at time 1 and false at time 2. As a result, this evaluation is considered a valid description of the evolution of the state, although there is no valid reason to explain being false at time 2. The fact that minimization of changes leads to wrong solution is the motivation for the introduction of the Yale shooting problem. While the Yale shooting problem has been considered a severe obstacle to the use of logic for formalizing dynamical scenarios, solutions to it are known since the late 1980s. One solution involves the use of in the specification of actions: according to this solution, the fact that shooting causes Fred to die is formalized by the preconditions: alive and loaded, and the effect is that alive changes value (since alive was true before, this corresponds to alive becoming false). By turning this implication into an if and only if statement, the effects of shooting are correctly formalized. (Predicate completion is more complicated when there is more than one implication involved.) A solution proposed by Erik Sandewall was to include a new condition of occlusion, which formalizes the “permission to change” for a fluent. The effect of an action that might change a fluent is therefore that the fluent has the new value, and that the occlusion is made (temporarily) true. What is minimized is not the set of changes, but the set of occlusions being true. Another constraint specifying that no fluent changes unless occlusion is true completes this solution. The Yale shooting scenario is also correctly formalized by the Reiter version of the situation calculus, the fluent calculus, and the action description languages. In 2005, the 1985 paper in which the Yale shooting scenario was first described received the . In spite of being a solved problem, that example is still sometimes mentioned in recent research papers, where it is used as an illustrative example (e.g., for explaining the syntax of a new logic for reasoning about actions), rather than being presented as a problem. (en)
|
| rdfs:comment
|
- The Yale shooting problem is a conundrum or scenario in formal situational logic on which early logical solutions to the frame problem fail. The name of this problem derives from its inventors, and Drew McDermott, working at Yale University when they proposed it. In this scenario, Fred (later identified as a turkey) is initially alive and a gun is initially unloaded. Loading the gun, waiting for a moment, and then shooting the gun at Fred is expected to kill Fred. However, if inertia is formalized in logic by minimizing the changes in this situation, then it cannot be uniquely proved that Fred is dead after loading, waiting, and shooting. In one solution, Fred indeed dies; in another (also logically correct) solution, the gun becomes mysteriously unloaded and Fred survives. (en)
- イェール射撃問題（イェールしゃげきもんだい、英: Yale shooting problem）とは、形式的状況分析におけるあるシナリオであり、フレーム問題に対する初期の論理学的アプローチが解けなかった難問である。名称はこの問題の発案者、がイェール大学に所属していたことにちなむ。シナリオは次のとおりである。最初の時点で、フレッド（後に七面鳥であるとされた）は生きていて、銃には弾丸が装填されていないものとする。銃に弾丸を装填し、少し待機し、フレッドに向けて発砲すれば、フレッドは殺されるものと想定される。ところが、変化が最小化されるべく論理学的な定式化がなされたとすると（慣性（inertia）の表現）、装填・待機・発砲という一連の動作の後にフレッドが死亡しているという結論が必ずしも導かれない。一つの帰結は、フレッドが実際に死亡しているというものである。もう一つの（論理的には正しい）帰結は、銃から弾丸が不思議と抜かれていて、フレッドは生存しているというものである（本項において「発砲（shooting）」は空砲の場合も含む）。 イェール射撃問題では、変化数が最小となるようなフルーエントへの付値の一つは次のようなものである。 これが期待される解であり、フルーエントの変化は2回である： が時刻1で真になり、 が時刻3で偽になる。 ところが次の付値も同じ条件を満たす。 (ja)
|
