Проблема со стрельбой в Йельском университете

Проблема стрельбы в Йельском университете — это головоломка или сценарий формальной ситуационной логики , в котором ранние логические решения проблемы фрейма терпят неудачу. Название этой проблемы происходит от сценария, предложенного ее изобретателями Стивом Хэнксом и Дрю Макдермоттом , работавшими в Йельском университете , когда они предложили ее. В этом сценарии Фред (позже идентифицированный как индейка ) изначально жив, а оружие изначально разряжено. Ожидается, что зарядка пистолета, ожидание момента и последующая стрельба по Фреду убьют Фреда. Однако если инерцию формализовать логически путем минимизации изменений в этой ситуации, то нельзя однозначно доказать, что Фред мертв после заряжания, ожидания и стрельбы. В одном из решений Фред действительно умирает; в другом (также логически правильном) решении пистолет загадочным образом разряжается, и Фред выживает.

Технически этот сценарий описывается двумя флюентами (флюэнт — это состояние, которое может изменить значение истинности ): со временем $alive$ и $loaded$ . Изначально первое условие истинно, а второе ложно. Затем ружье заряжается, проходит некоторое время и производится выстрел. Такие проблемы можно формализовать логически, рассмотрев четыре временные точки. $0$ , $1$ , $2$ , и $3$ , и превращая каждого бегло говорящего, такого как $alive$ в предикат $alive(t)$ в зависимости от времени. Прямая формализация постановки Йельской задачи о стрельбе в логике следующая:

alive(0)

\neg loaded(0)

true\rightarrow loaded(1)

loaded(2)\rightarrow \neg alive(3)

Первые две формулы представляют исходное состояние. Третья формула формализует эффект от заряжания орудия во времени. $0$ . Четвертая формула формализует эффект от стрельбы по Фреду во времени. $2$ . Это упрощенная формализация, в которой имена действий игнорируются, а эффекты действий прямо указываются для моментов времени, в которые действия выполняются. см. в расчете ситуации Подробности .

Приведенные выше формулы, хотя и являются прямой формализацией известных фактов, недостаточны для правильной характеристики области. Действительно, $\neg alive(1)$ согласуется со всеми этими формулами, хотя нет никаких оснований полагать, что Фред умрет до того, как будет произведен выстрел. Проблема в том, что приведенные выше формулы включают только эффекты действий, но не указывают, что все флюенты, не измененные действиями, остаются прежними. Другими словами, формула $alive(0)\equiv alive(1)$ необходимо добавить, чтобы формализовать неявное предположение о том, что заряжание ружья меняет только значение $loaded$ а не ценность $alive$ . Необходимость большого количества формул, констатирующих очевидный факт, что условия не изменяются, пока их не изменяет действие, известна как проблема фрейма .

Раннее решение проблемы фрейма было основано на минимизации изменений. Другими словами, сценарий формализуется приведенными выше формулами (которые определяют только последствия действий) и предположением, что изменения флюентов с течением времени минимально возможны. Обоснование состоит в том, что приведенные выше формулы обеспечивают все последствия действий, в то время как минимизация должна ограничивать изменения именно теми, которые происходят в результате действий.

В сценарии стрельбы в Йельском университете одна из возможных оценок беглости, в которой изменения минимизированы, следующая.

$alive(0)$	$alive(1)$	$alive(2)$	$\neg alive(3)$
$\neg loaded(0)$	$loaded(1)$	$loaded(2)$	$loaded(3)$

Это ожидаемое решение. Он содержит два плавных изменения: $loaded$ становится истинным в момент времени 1 и $alive$ становится ложным в момент 3. Следующая оценка также удовлетворяет всем приведенным выше формулам.

$alive(0)$	$alive(1)$	$alive(2)$	$alive(3)$
$\neg loaded(0)$	$loaded(1)$	$\neg loaded(2)$	$\neg loaded(3)$

В этой оценке пока есть только два изменения: $loaded$ становится истинным в момент 1 и ложным в момент 2. В результате эта оценка считается достоверным описанием эволюции состояния, хотя нет веской причины объяснять $loaded$ быть ложным в момент времени 2. Тот факт, что минимизация изменений приводит к неправильному решению, является мотивацией для введения Йельской задачи о стрельбе.

Хотя проблема стрельбы в Йельском университете считалась серьезным препятствием для использования логики для формализации динамических сценариев, ее решения были известны с конца 1980-х годов. Одно из решений предполагает использование завершения предиката в спецификации действий: в этом решении тот факт, что стрельба приводит к смерти Фреда, формализуется предварительными условиями: жив и загружен , а эффект заключается в том, что живой меняет значение (поскольку жив был истинным до того, как , это соответствует тому, что живое становится ложным). Превратив это импликацию в утверждение « если и только если» , мы правильно формализуем эффекты стрельбы. (Завершение предиката более сложное, если задействовано более одного импликации.)

Решение, предложенное Эриком Сандеволлом, заключалось в включении нового условия окклюзии, которое формализует «разрешение на изменение» для беглого языка. Таким образом, эффект действия, которое может изменить Fluent, заключается в том, что Fluent приобретает новое значение и что окклюзия становится (временно) истинной. Минимизируется не набор изменений, а набор истинных окклюзий. Еще одно ограничение, указывающее, что никакие плавные изменения не выполняются, если окклюзия не является истинной, завершает это решение.

Сценарий стрельбы в Йельском университете также правильно формализуется с помощью райтеровской версии ситуационного исчисления , беглого исчисления и языков описания действий .

В 2005 году статья 1985 года, в которой впервые был описан сценарий стрельбы в Йельском университете, получила награду AAAI Classic Paper . Несмотря на то, что проблема решена, этот пример все же иногда упоминается в недавних исследовательских работах, где он используется как иллюстративный пример (например, для объяснения синтаксиса новой логики рассуждений о действиях), а не представляется как проблема.

См. также

Ссылки

М. Гельфонд и В. Лифшиц (1993). Представление действий и изменений с помощью логических программ. Журнал логического программирования , 17:301–322.
С. Хэнкс и Д. Макдермотт (1987). Немонотонная логика и временная проекция. Искусственный интеллект , 33(3):379–412.
Дж. Маккарти (1986). Применение ограничений для формализации здравого смысла. Искусственный интеллект , 28:89–116.
Т. Митчелл и Х. Левеск (2006). Награды AAAI Classic Paper 2005 года. «Журнал AI», 26(4):98–99.
Р. Рейтер (1991). Проблема фрейма в ситуационном исчислении: простое решение (иногда) и результат полноты целевой регрессии. Владимир Лифшиц, редактор журнала « Искусственный интеллект и математическая теория вычислений: статьи в честь Джона Маккарти» , страницы 359–380. Академик Пресс, Нью-Йорк.
Э. Сандеволл (1994). Особенности и Fluents . Издательство Оксфордского университета.