Введение

Проблема искусственного интеллекта и категорической алгебры

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

Решение

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

Раствор для окклюзионной жидкости

Это решение было предложено Эриком Сандвалом, который также определил формальный язык для спецификации динамических доменов; поэтому такой домен можно сначала выразить на этом языке, а затем автоматически перевести в логику. В этой статье представлено только выражение в логике, и только в упрощенном языке без названий действий. Обоснование этого решения заключается в том, чтобы представлять не только значение условий во времени, но и то, могут ли они быть изменены последним выполненным действием. Последнее представляется другим условием, называемым окклюзией. Условие считается окклюдированным в данный момент времени, если только что было выполнено действие, которое делает это условие истинным или ложным в качестве результата. Окклюзию можно рассматривать как «разрешение на изменение»: если условие окклюдировано, оно освобождается от соблюдения принципа инерции. В упрощенном примере с дверью и светом окклюзию можно формализовать двумя предикатами и . Обоснование состоит в том, что условие может изменить свое значение только в том случае, если соответствующий предикат окклюзии истинен в следующий момент времени. В свою очередь, предикат окклюзии истинен только тогда, когда выполняется действие, влияющее на это условие. В общем случае, любое действие, делающее условие истинным или ложным, также делает соответствующий предикат окклюзии истинным. В этом случае, истинно, что делает антецедент четвертой формулы выше ложным для ; следовательно, ограничение, что не выполняется для . Поэтому, может изменить свое значение, что также обеспечивается третьей формулой. Для того чтобы это условие работало, предикаты окклюзии должны быть истинными только тогда, когда они становятся истинными в результате действия. Этого можно достичь либо с помощью ограничений, либо с помощью полноты предикатов. Стоит отметить, что окклюзия не обязательно подразумевает изменение: например, выполнение действия открытия двери, когда она уже открыта (в приведенной выше формализации), делает предикат истинным и делает истинным; однако, не изменило свое значение, так как оно уже было истинным.

Предсказание решения

Это кодирование аналогично решению для плавного окклюдирования, но дополнительные предикаты обозначают изменение, а не разрешение на изменение. Например, обозначает тот факт, что предикат изменится от момента времени до . В результате, предикат меняется тогда и только тогда, когда соответствующий предикат изменения истинен. Действие приводит к изменению, если и только если оно делает истинным условие, которое ранее было ложным, или наоборот. Третья формула – это другой способ сказать, что открытие двери приводит к открытию двери. Точнее, она утверждает, что открытие двери изменяет состояние двери, если она была ранее закрыта. Последние два условия утверждают, что условие меняет свое значение в момент времени , если и только если соответствующий предикат изменения истинен в этот момент времени. Для завершения решения необходимо, чтобы моменты времени, в которые предикаты изменения истинны, были минимальными, и этого можно достичь, применив завершение предиката к правилам, определяющим эффекты действий.

Логическое решение по умолчанию

Проблема фрейма может рассматриваться как проблема формализации принципа, согласно которому по умолчанию "все предполагается оставаться в том состоянии, в котором оно находится" (Лейбниц, "Введение в секретную энциклопедию", ок. 1679 г.). Этот принцип по умолчанию, иногда называемый здравым смыслом инерции, был выражен Раймондом Райтером в логике по умолчанию: (если истинно в ситуации , и можно предположить, что остается истинным после выполнения действия , то можно заключить, что остается истинным). Стив Хэнкс и Дрю Макдермот утверждали, основываясь на их примере со стрельбой в Йельском университете, что это решение проблемы фрейма неудовлетворительно. Однако Хадсон Тернер показал, что оно работает корректно при наличии соответствующих дополнительных постулатов.

Логическое решение разделения

Логика разделения — это формализм для рассуждений о компьютерных программах, использующий предусловия и постусловия вида. Логика разделения является расширением логики Хоара, ориентированным на рассуждения об изменяемых структурах данных в компьютерной памяти и других динамических ресурсах, и она имеет специальный связующий оператор *, произносимый как "и раздельно", для поддержки независимого рассуждения о непересекающихся областях памяти. Логика разделения использует строгую интерпретацию предусловий и постусловий, утверждающих, что код может обращаться только к ячейкам памяти, существование которых гарантируется предусловием. Это обеспечивает корректность важнейшего правила логики — правила рамки.

Правило рамки позволяет добавлять описания произвольной памяти, находящейся вне области действия кода (обращаемой памяти), к спецификации: это позволяет исходной спецификации концентрироваться исключительно на области действия. Например, вывод

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