El problema del tiroteo de Yale es un enigma o escenario en lógica situacional formal en el que fallan las primeras soluciones lógicas al problema del marco . El nombre de este problema proviene de un escenario propuesto por sus inventores, Steve Hanks y Drew McDermott , que trabajaban en la Universidad de Yale cuando lo propusieron. En este escenario, Fred (más tarde identificado como un pavo ) está inicialmente vivo y un arma está inicialmente descargada. Se espera que cargar el arma, esperar un momento y luego disparar el arma a Fred mate a Fred. Sin embargo, si la inercia se formaliza en la lógica minimizando los cambios en esta situación, entonces no se puede probar de manera única que Fred está muerto después de cargar, esperar y disparar. En una solución, Fred muere de hecho; en otra solución (también lógicamente correcta), el arma se descarga misteriosamente y Fred sobrevive.
Técnicamente, este escenario se describe mediante dos fluidos (un fluido es una condición que puede cambiar su valor de verdad con el tiempo): y . Inicialmente, la primera condición es verdadera y la segunda es falsa. Luego, se carga el arma, pasa un tiempo y se dispara. Estos problemas se pueden formalizar en lógica considerando cuatro puntos temporales , , y , y convirtiendo cada fluido como en un predicado que depende del tiempo. Una formalización directa del enunciado del problema de tiro de Yale en lógica es la siguiente:
Las dos primeras fórmulas representan el estado inicial. La tercera fórmula formaliza el efecto de cargar el arma en el momento . La cuarta fórmula formaliza el efecto de dispararle a Fred en el momento . Se trata de una formalización simplificada en la que se ignoran los nombres de las acciones y los efectos de las acciones se especifican directamente para los puntos de tiempo en los que se ejecutan las acciones. Consulte el cálculo de situaciones para obtener más detalles.
Las fórmulas anteriores, si bien son formalizaciones directas de los hechos conocidos, no son suficientes para caracterizar correctamente el dominio. De hecho, es consistente con todas estas fórmulas, aunque no hay razón para creer que Fred muere antes de que se haya disparado el arma. El problema es que las fórmulas anteriores solo incluyen los efectos de las acciones, pero no especifican que todos los fluidos no modificados por las acciones permanecen iguales. En otras palabras, se debe agregar una fórmula para formalizar la suposición implícita de que cargar el arma solo cambia el valor de y no el valor de . La necesidad de una gran cantidad de fórmulas que establezcan el hecho obvio de que las condiciones no cambian a menos que una acción las cambie se conoce como el problema del marco .
Una solución temprana al problema del marco se basó en minimizar los cambios. En otras palabras, el escenario se formaliza mediante las fórmulas anteriores (que especifican solo los efectos de las acciones) y mediante el supuesto de que los cambios en los fluidos a lo largo del tiempo son lo mínimos posibles. La lógica es que las fórmulas anteriores obligan a que se produzcan todos los efectos de las acciones, mientras que la minimización debería restringir los cambios exactamente a los que se deben a las acciones.
En el escenario del tiroteo de Yale, una posible evaluación de los fluidos en la que se minimizan los cambios es la siguiente.
Esta es la solución esperada. Contiene dos cambios fluidos: se vuelve verdadera en el momento 1 y se vuelve falsa en el momento 3. La siguiente evaluación también satisface todas las fórmulas anteriores.
En esta evaluación, todavía hay solo dos cambios: se vuelve verdadero en el tiempo 1 y falso en el tiempo 2. Como resultado, esta evaluación se considera una descripción válida de la evolución del estado, aunque no hay una razón válida para explicar que sea falso en el tiempo 2. El hecho de que la minimización de los cambios conduzca a una solución incorrecta es la motivación para la introducción del problema de tiro de Yale.
Aunque el problema del tiroteo de Yale se ha considerado un grave obstáculo para el uso de la lógica para formalizar escenarios dinámicos, se conocen soluciones desde finales de los años 1980. Una solución implica el uso de la compleción de predicados en la especificación de acciones: en esta solución, el hecho de que el tiroteo provoque la muerte de Fred se formaliza mediante las precondiciones: alive y charged , y el efecto es que alive cambia de valor (ya que alive era verdadero antes, esto corresponde a que alive se vuelva falso). Al convertir esta implicación en una declaración if y only if , los efectos del tiroteo se formalizan correctamente. (La compleción de predicados es más complicada cuando hay más de una implicación involucrada).
Una solución propuesta por Erik Sandewall fue incluir una nueva condición de oclusión, que formaliza el “permiso para cambiar” para un fluido. El efecto de una acción que podría cambiar un fluido es, por lo tanto, que el fluido tiene el nuevo valor y que la oclusión se hace (temporalmente) verdadera. Lo que se minimiza no es el conjunto de cambios, sino el conjunto de oclusiones verdaderas. Otra restricción que especifica que ningún fluido cambia a menos que la oclusión sea verdadera completa esta solución.
El escenario del tiroteo de Yale también está correctamente formalizado por la versión Reiter del cálculo de situaciones , el cálculo fluido y los lenguajes de descripción de acciones .
En 2005, el artículo de 1985 en el que se describió por primera vez el escenario del tiroteo de Yale recibió el premio AAAI Classic Paper. A pesar de ser un problema resuelto, ese ejemplo todavía se menciona a veces en artículos de investigación recientes, donde se utiliza como ejemplo ilustrativo (por ejemplo, para explicar la sintaxis de una nueva lógica para razonar sobre acciones), en lugar de presentarse como un problema.
