The Yale shooting problem is a conundrum or scenario in formal situational logic on which early logical solutions to the frame problem fail.
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.
Such problems can be formalized in logic by considering four time points
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
The formulae above, while being direct formalizations of the known facts, do not suffice to correctly characterize the domain.
is consistent with all these formulae, although there is no reason to believe that Fred dies before the gun has been shot.
must be added to formalize the implicit assumption that loading the gun only changes the value of
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.
In the Yale shooting scenario, one possible evaluation of the fluents in which the changes are minimized is the following one.
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 have been known since the late 1980s.
By turning this implication into an if and only if statement, the effects of shooting are correctly formalized.
A solution proposed by Erik Sandewall was to include a new condition of occlusion, which formalizes the “permission to change” for a fluent.
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 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.