Задача о стрельбе в Йеле — это головоломка или сценарий в формальной ситуативной логике , в котором ранние логические решения проблемы фрейма терпят неудачу. Название этой задачи происходит от сценария, предложенного ее изобретателями Стивом Хэнксом и Дрю Макдермоттом , работавшими в Йельском университете, когда они ее предложили. В этом сценарии Фред (позже идентифицированный как индейка ) изначально жив, а пистолет изначально разряжен. Ожидается, что зарядка пистолета, ожидание в течение момента, а затем выстрел из пистолета во Фреда убьют Фреда. Однако, если инерция формализуется в логике путем минимизации изменений в этой ситуации, то нельзя однозначно доказать, что Фред мертв после зарядки, ожидания и выстрела. В одном решении Фред действительно умирает; в другом (также логически правильном) решении пистолет загадочным образом становится разряженным, и Фред выживает.
Технически этот сценарий описывается двумя флюентами (флюент — это условие, которое может менять истинностное значение с течением времени): и . Изначально первое условие истинно, а второе ложно. Затем ружье заряжается, проходит некоторое время, и ружье стреляет. Такие задачи можно формализовать в логике, рассмотрев четыре временные точки , , , и , и превратив каждый флюент, такой как , в предикат, зависящий от времени. Прямая формализация постановки задачи о стрельбе в Йеле в логике следующая:
Первые две формулы представляют начальное состояние. Третья формула формализует эффект заряжания ружья в момент времени . Четвертая формула формализует эффект стрельбы по Фреду в момент времени . Это упрощенная формализация, в которой имена действий игнорируются, а эффекты действий напрямую указываются для моментов времени, в которых эти действия выполняются. Подробности см. в исчислении ситуаций .
Формулы выше, хотя и являются прямыми формализациями известных фактов, недостаточны для правильной характеристики области. Действительно, согласуется со всеми этими формулами, хотя нет никаких оснований полагать, что Фред умирает до того, как выстрелит ружье. Проблема в том, что формулы выше включают только эффекты действий, но не указывают, что все флюенты, не измененные действиями, остаются прежними. Другими словами, необходимо добавить формулу для формализации неявного предположения, что заряжение ружья изменяет только значение , а не значение . Необходимость большого количества формул, утверждающих очевидный факт, что условия не изменяются, если действие не изменяет их, известна как проблема фрейма .
Раннее решение проблемы фрейма основывалось на минимизации изменений. Другими словами, сценарий формализуется приведенными выше формулами (которые определяют только эффекты действий) и предположением, что изменения во флюентах с течением времени минимальны. Обоснование заключается в том, что приведенные выше формулы обеспечивают реализацию всех эффектов действий, в то время как минимизация должна ограничивать изменения только теми, которые вызваны действиями.
В сценарии стрельбы в Йельском университете возможна следующая оценка беглостей, в которой изменения минимальны.
Это ожидаемое решение. Оно содержит два плавных изменения: становится истинным в момент времени 1 и становится ложным в момент времени 3. Следующая оценка также удовлетворяет всем формулам выше.
В этой оценке по-прежнему есть только два изменения: становится истинным в момент времени 1 и ложным в момент времени 2. В результате эта оценка считается допустимым описанием эволюции состояния, хотя нет никаких веских причин, объясняющих, почему она ложна в момент времени 2. Тот факт, что минимизация изменений приводит к неверному решению, является мотивацией для введения Йельской задачи о стрельбе.
Хотя проблема стрельбы в Йеле считалась серьезным препятствием для использования логики для формализации динамических сценариев, ее решения были известны с конца 1980-х годов. Одно из решений предполагает использование завершения предиката в спецификации действий: в этом решении тот факт, что стрельба приводит к смерти Фреда, формализуется предварительными условиями: alive и load , и эффект заключается в том, что alive меняет значение (поскольку alive было true ранее, это соответствует тому, что alive становится false). Превращая это следствие в утверждение if and only if , последствия стрельбы корректно формализуются. (Завершение предиката сложнее, когда задействовано более одного следствия.)
Решение, предложенное Эриком Сандеваллом, состояло во включении нового условия окклюзии, которое формализует «разрешение на изменение» для флюента. Эффект действия, которое может изменить флюент, заключается в том, что флюент имеет новое значение, и что окклюзия становится (временно) истинной. Минимизируется не набор изменений, а набор окклюзии, являющийся истинным. Другое ограничение, указывающее, что флюент не изменяется, если окклюзия не является истинной, завершает это решение.
Сценарий стрельбы в Йеле также правильно формализован с помощью версии исчисления ситуаций Рейтера , текучего исчисления и языков описания действий .
В 2005 году статья 1985 года, в которой впервые был описан сценарий стрельбы в Йеле, получила премию AAAI Classic Paper. Несмотря на то, что это решенная проблема, этот пример все еще иногда упоминается в недавних исследовательских работах, где он используется как иллюстративный пример (например, для объяснения синтаксиса новой логики для рассуждений о действиях), а не представляется как проблема.
