Ситуационное исчисление - Situation calculus

Ситуация исчисление представляет собой логический формализм предназначен для представления и рассуждения о динамических доменах. Впервые он был представлен Джоном Маккарти в 1963 году. Основная версия ситуационного исчисления, представленная в этой статье, основана на версии, представленной Рэем Рейтером в 1991 году. За ней следуют разделы о версии Маккарти 1986 года и формулировке логического программирования .

Обзор

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

Действия, которые можно совершать в мире
В флюэнты , которые описывают состояние мира
Ситуации

Область формализуется рядом формул, а именно:

Аксиомы предусловия действия, по одной для каждого действия
Аксиомы государства-преемника, по одной для каждого свободно владеющего
Аксиомы, описывающие мир в различных ситуациях
Основные аксиомы ситуационного исчисления

Простой мир роботов будет смоделирован в качестве работающего примера. В этом мире есть один робот и несколько неодушевленных предметов. Мир выложен в соответствии с сеткой, так что местоположения могут быть указаны в виде координатных точек. Робот может перемещаться по миру, а также поднимать и бросать предметы. Некоторые предметы могут быть слишком тяжелыми, чтобы робот мог их поднять, или хрупкими, поэтому они ломаются при падении. Робот также может ремонтировать любые сломанные предметы, которые он держит. ${\ Displaystyle (х, у)}$

Элементы

Основными элементами ситуационного исчисления являются действия, беглость и ситуации. Ряд объектов также обычно участвует в описании мира. Исчисление ситуаций основано на отсортированном домене с тремя видами: действия, ситуации и объекты, где объекты включают в себя все, что не является действием или ситуацией. Могут использоваться переменные каждого вида. В то время как действия, ситуации и объекты являются элементами предметной области, флюэнты моделируются либо как предикаты, либо как функции.

Действия

Действия образуют своего рода домен. Можно использовать переменные действия сортировки. Действия можно выразить количественно. В примере мира роботов возможными условиями действия могут быть моделирование робота, перемещающегося в новое место , и моделирование робота, поднимающего объект . Специальный предикат используется, чтобы указать, когда действие выполняется. ${\ displaystyle move (x, y)}$ ${\ Displaystyle (х, у)}$ ${\ displaystyle pickup (o)}$ ${\ displaystyle o}$ ${\ displaystyle Poss}$

Ситуации

В исчислении ситуаций динамический мир моделируется как прогрессирующий через серию ситуаций в результате различных действий, совершаемых в этом мире. Ситуация представляет собой историю возникновения действий. В описанной здесь версии ситуационного исчисления Райтера ситуация не представляет состояние, что противоречит буквальному значению термина и первоначальному определению Маккарти и Хейса. Этот момент был резюмирован Рейтером следующим образом:

Ситуация - это конечная последовательность действий. Период. Это не состояние, это не снимок, это история [1] .

Ситуация до выполнения каких-либо действий обычно обозначается и называется исходной ситуацией. Новая ситуация, возникающая в результате выполнения действия, обозначается с помощью символа функции (в некоторых других ссылках также используется ). Этот функциональный символ имеет ситуацию и действие в качестве аргументов и ситуацию как результат, причем последний является ситуацией, которая возникает в результате выполнения данного действия в данной ситуации. ${\ displaystyle S_ {0}}$ ${\ displaystyle do}$ ${\ displaystyle result}$

Тот факт, что ситуации представляют собой последовательности действий, а не состояний, подтверждается аксиомой, утверждающей, что равняется тогда и только тогда, когда и . Это условие не имеет смысла, если ситуации были состояниями, поскольку два разных действия, выполненные в двух разных состояниях, могут привести к одному и тому же состоянию. ${\ displaystyle do (а, s)}$ ${\ displaystyle do (а ', s')}$ ${\ Displaystyle а = а '}$ ${\ displaystyle s = s '}$

В приведенном в качестве примера мире роботов, если первое действие робота - переместиться в определенное место , то первое действие - это, а результирующая ситуация - . Если его следующее действие - поднять мяч, возникает ситуация . Ситуации такие термины, как и обозначают последовательности выполняемых действий, а не описание состояния, которое возникает в результате выполнения. ${\ Displaystyle (2,3)}$ ${\ displaystyle move (2,3)}$ ${\ displaystyle do (переместить (2,3), S_ {0})}$ ${\ displaystyle do (pickup (мяч), do (move (2,3), S_ {0}))}$ ${\ displaystyle do (переместить (2,3), S_ {0})}$ ${\ displaystyle do (pickup (мяч), do (move (2,3), S_ {0}))}$

Свободно

Утверждения, истинностное значение которых может измениться, моделируются реляционными плавными средствами , предикатами, которые принимают ситуацию в качестве последнего аргумента. Также возможны функциональные флюенты , функции, которые принимают ситуацию в качестве последнего аргумента и возвращают значение, зависящее от ситуации. Флюенты можно рассматривать как «свойства мира» ».

В этом примере беглое слово может использоваться, чтобы указать, что робот несет определенный объект в конкретной ситуации. Если робот изначально ничего не несет, это ложь, пока верно. Местоположение робота можно смоделировать с помощью функционального флюента, который возвращает местоположение робота в конкретной ситуации. ${\ displaystyle is \ _carrying (o, s)}$ ${\ displaystyle is \ _carrying (Ball, S_ {0})}$ ${\ displaystyle is \ _carrying (Ball, do (pickup (Ball), S_ {0}))}$ ${\ displaystyle location (s)}$ ${\ Displaystyle (х, у)}$

Формулы

Описание динамического мира кодируется в логике второго порядка с использованием трех видов формул: формул о действиях (предусловиях и следствиях), формулах о состоянии мира и основных аксиомах.

Предпосылки действий

Некоторые действия могут быть невыполнимы в данной ситуации. Например, невозможно положить предмет, если он действительно не несет его. Ограничения на выполнение действий моделируются литералами вида , где - действие, ситуация, а также специальный бинарный предикат, обозначающий выполнимость действий. В этом примере условие, что падение объекта возможно только при его переноске, моделируется следующим образом: ${\ displaystyle Poss (a, s)}$ ${\ displaystyle a}$ ${\ displaystyle s}$ ${\ displaystyle Poss}$

${\ displaystyle Poss (drop (o), s) \ leftrightarrow is \ _carrying (o, s)}$

В качестве более сложного примера приведем следующие модели, согласно которым робот может нести только один объект за раз, и что некоторые объекты слишком тяжелы для робота, чтобы их поднять (обозначено предикатом ): ${\ displaystyle heavy}$

${\ Displaystyle Посс (пикап (о), s) \ leftrightarrow (\ forall z \ neg is \ _carrying (z, s)) \ клин \ neg heavy (o)}$

Эффекты действия

Учитывая, что действие возможно в ситуации, необходимо указать влияние этого действия на флюэнты. Это делается с помощью аксиом эффекта. Например, тот факт, что робот поднимает объект, несет его, можно смоделировать следующим образом:

${\ displaystyle Poss (подобрать (o), s) \ rightarrow is \ _carrying (o, do (pickup (o), s))}$

Также можно указать условные эффекты, которые являются эффектами, зависящими от текущего состояния. Следующие модели показывают, что некоторые объекты хрупкие (обозначены предикатом ) и их падение приводит к их поломке (обозначено беглым ): ${\ displaystyle fragile}$ ${\ displaystyle broken}$

${\ Displaystyle Посс (капля (о), s) \ клин хрупкий (о) \ rightarrow сломанный (о, делать (капля (о), s))}$

Хотя эта формула правильно описывает эффект действий, ее недостаточно для правильного описания действия в логике из-за проблемы с фреймом .

Проблема с рамой

Хотя приведенные выше формулы кажутся подходящими для рассуждений о последствиях действий, у них есть критический недостаток - они не могут использоваться для определения отсутствия последствий действий. Например, невозможно сделать вывод, что после поднятия объекта местоположение робота остается неизменным. Для этого требуется так называемая аксиома фрейма, формула вроде:

${\ displaystyle Poss (подобрать (о), s) \ место клина (s) = (x, y) \ положение правой стрелки (do (подобрать (o), s)) = (x, y)}$

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

Аксиомы государства-преемника

Аксиомы состояния преемника «решают» проблему фрейма в ситуационном исчислении. Согласно этому решению, разработчик должен перечислить в качестве аксиом эффекта все способы, которыми можно изменить значение конкретного fluent. Аксиомы эффекта, влияющие на значение fluent, могут быть записаны в обобщенном виде как аксиома положительного и отрицательного эффекта: ${\ Displaystyle F ({\ overrightarrow {x}}, s)}$

${\ displaystyle Poss (a, s) \ wedge \ gamma _ {F} ^ {+} ({\ overrightarrow {x}}, a, s) \ rightarrow F ({\ overrightarrow {x}}, do (a, s))}$

${\ displaystyle Poss (a, s) \ wedge \ gamma _ {F} ^ {-} ({\ overrightarrow {x}}, a, s) \ rightarrow \ neg F ({\ overrightarrow {x}}, do ( как))}$

Формула описывает условия, при которых действие в ситуации заставляет беглый язык стать истинным в ситуации преемника . Точно так же описывает условия, при которых выполнение действия в ситуации делает бегло ложным в ситуации преемника. ${\ displaystyle \ gamma _ {F} ^ {+}}$ ${\ displaystyle a}$ ${\ displaystyle s}$ ${\ displaystyle F}$ ${\ displaystyle do (а, s)}$ ${\ displaystyle \ gamma _ {F} ^ {-}}$ ${\ displaystyle a}$ ${\ displaystyle s}$ ${\ displaystyle F}$

Если эта пара аксиом описывает все способы, которыми fluent может изменять значение, их можно переписать в виде единой аксиомы: ${\ displaystyle F}$

${\ displaystyle Poss (a, s) \ rightarrow \ left [F ({\ overrightarrow {x}}, do (a, s)) \ leftrightarrow \ gamma _ {F} ^ {+} ({\ overrightarrow {x} }, a, s) \ vee \ left (F ({\ overrightarrow {x}}, s) \ wedge \ neg \ gamma _ {F} ^ {-} ({\ overrightarrow {x}}, a, s) \верно-верно]}$

Словами, эта формула гласит: «при условии, что действие в ситуации возможно , беглое владение будет истинным в результирующей ситуации, если и только если выполнение в действии сделает его правдой, или оно будет верным в ситуации, а выполнение в ситуации - не сделай это ложным ". ${\ displaystyle a}$ ${\ displaystyle s}$ ${\ displaystyle F}$ ${\ displaystyle do (а, s)}$ ${\ displaystyle a}$ ${\ displaystyle s}$ ${\ displaystyle s}$ ${\ displaystyle a}$ ${\ displaystyle s}$

В качестве примера, значение введенного выше fluent задается следующей аксиомой состояния преемника: ${\ displaystyle broken}$

${\ displaystyle Poss (a, s) \ rightarrow \ left [сломанный (o, do (a, s)) \ leftrightarrow a = drop (o) \ клин хрупкий (o) \ vee сломанный (o, s) \ клин a \ neq repair (o) \ right]}$

состояния

Свойства исходной или любой другой ситуации можно указать, просто указав их в виде формул. Например, факт о начальном состоянии формализуется путем утверждения о (что является не состоянием, а ситуацией ). Следующие утверждения моделируют, что изначально робот ничего не несет, находится на месте и не имеет сломанных объектов: ${\ displaystyle S_ {0}}$ ${\ displaystyle (0,0)}$

${\ displaystyle \ forall z \, \ neg - это \ _carrying (z, S_ {0})}$

${\ Displaystyle местоположение (S_ {0}) = (0,0) \,}$

${\ displaystyle \ forall o \, \ neg broken (o, S_ {0})}$

Основополагающие аксиомы

Фундаментальные аксиомы ситуационного исчисления формализуют идею о том, что ситуации становятся историей благодаря наличию . Они также включают в себя другие свойства, такие как индукция второго порядка по ситуациям. ${\ displaystyle do (a, s) = do (a ', s') \ iff a = a '\ land s = s'}$

Регресс

Регрессия - это механизм доказательства последствий при исчислении ситуации. Он основан на выражении формулы, содержащей ситуацию, в виде формулы, содержащей действие и ситуацию , но не ситуацию . Повторяя эту процедуру, можно получить эквивалентную формулу, содержащую только начальную ситуацию . Доказательство следствий из этой формулы якобы проще, чем из исходной. ${\ displaystyle do (а, s)}$ ${\ displaystyle a}$ ${\ displaystyle s}$ ${\ displaystyle do (а, s)}$ ${\ displaystyle S_ {0}}$

ГОЛОГ

GOLOG - это язык логического программирования, основанный на ситуационном исчислении.

Исходная версия ситуационного исчисления

Основное отличие исходного ситуационного исчисления Маккарти и Хейса от используемого сегодня - это интерпретация ситуаций. В современной версии ситуационного исчисления ситуация - это последовательность действий. Первоначально ситуации определялись как «полное состояние Вселенной в определенный момент времени». С самого начала было ясно, что такие ситуации невозможно полностью описать; идея заключалась в том, чтобы просто дать некоторые утверждения о ситуациях и вывести из них последствия. Это также отличается от подхода, применяемого в беглом исчислении , где состояние может быть совокупностью известных фактов, то есть, возможно, неполным описанием вселенной.

В исходной версии ситуационного исчисления флюенты не реифицируются. Другими словами, условия, которые могут измениться, представлены предикатами, а не функциями. Фактически, Маккарти и Хейс определили беглость как функцию, которая зависит от ситуации, но затем они всегда использовали предикаты для представления беглых языков. Например, тот факт, что на каком-то месте в ситуации идет дождь, обозначается буквой . В версии ситуационного исчисления Маккарти 1986 года используются функциональные беглые языки. Например, положение объекта в ситуации представлено значением , где - функция. Утверждения о таких функциях могут быть даны с использованием равенства: означает, что расположение объекта одинаково в двух ситуациях и . ${\ displaystyle x}$ ${\ displaystyle s}$ ${\ Displaystyle дождь (х, s)}$ ${\ displaystyle x}$ ${\ displaystyle s}$ ${\ displaystyle location (x, s)}$ ${\ displaystyle location}$ ${\ displaystyle location (x, s) = location (x, s ')}$ ${\ displaystyle x}$ ${\ displaystyle s}$ ${\ displaystyle s '}$

Выполнение действий представлено функцией : выполнение действия в ситуации есть ситуация . Эффект от действий выражается формулами, связывающими свободное владение ситуацией и свободное владение ситуацией . Например, то, что действие открытия двери приводит к тому, что дверь открывается, если она не заперта, представлено следующим образом: ${\ displaystyle result}$ ${\ displaystyle a}$ ${\ displaystyle s}$ ${\ displaystyle result (a, s)}$ ${\ displaystyle s}$ ${\ displaystyle result (a, s)}$

{\ displaystyle \ neg closed (дверь, s) \ rightarrow open (дверь, результат (открывается, s))}

Предикаты и представляют условия закрытия и открытия двери соответственно. Поскольку эти условия могут меняться, они представлены предикатами с аргументом ситуации. Формула гласит, что если дверь не заперта в ситуации, то дверь открывается после выполнения действия открытия, это действие представлено константой . ${\ displaystyle заблокировано}$ ${\ displaystyle open}$ ${\ displaystyle opens}$

Этих формул недостаточно, чтобы вывести все, что считается правдоподобным. Действительно, беглое владение разными ситуациями связано только в том случае, если они являются предпосылками и следствием действий; если на беглого не влияет действие, невозможно сделать вывод, что оно не изменилось. Например, приведенная выше формула не подразумевает того, что следует из , чего можно было бы ожидать (дверь не запирается, открывая ее). Для сохранения инерции необходимы формулы, называемые аксиомами системы координат . Эти формулы определяют все не-эффекты действий: ${\ displaystyle \ neg locked (дверь, результат (открывается, s))}$ ${\ displaystyle \ neg locked (дверь, s)}$

{\ displaystyle \ neg closed (дверь, s) \ rightarrow \ neg locked (дверь, результат (открывается, s))}

В исходной формулировке ситуационного исчисления исходная ситуация, позже обозначенная как , не идентифицируется явно. Исходная ситуация не нужна, если ситуации воспринимаются как описания мира. Например, для представления сценария, в котором дверь была закрыта, но не заперта, и действие по ее открыванию формализуется путем принятия константы для обозначения исходной ситуации и утверждения о ней (например, ). То, что дверь открыта после изменения, отражается в приведенной формуле . Вместо этого необходима исходная ситуация, если, как в современном ситуационном исчислении, ситуация рассматривается как история действий, поскольку исходная ситуация представляет собой пустую последовательность действий. ${\ displaystyle S_ {0}}$ ${\ displaystyle s}$ ${\ displaystyle \ neg locked (дверь, s)}$ ${\ displaystyle open (дверь, результат (открывается, s))}$

Версия ситуационного исчисления, представленная Маккарти в 1986 году, отличается от первоначальной для использования функциональных беглых слов (например, это термин, представляющий положение в ситуации ) и для попытки использовать ограниченность для замены аксиом фрейма. ${\ displaystyle location (x, s)}$ ${\ displaystyle x}$ ${\ displaystyle s}$

Ситуационное исчисление как логическая программа

Также возможно (например, Ковальски, 1979, Апт и Безем, 1990, Шанахан, 1997) записать ситуационное исчисление в виде логической программы:

${\ displaystyle Удерживает (f, do (a, s)) \ leftarrow Poss (a, s) \ клин Посвященных (a, f, s)}$

${\ displaystyle Удерживает (f, do (a, s)) \ leftarrow Poss (a, s) \ wedge Holds (f, s) \ wedge \ neg Завершает (a, f, s)}$

Вот мета-предикат, и переменная варьируется в пределах беглых языков. Предикаты , и соответствуют предикатам , и соответственно. Левая стрелка - половина эквивалентности . Другая половина подразумевается при завершении программы, в которой отрицание интерпретируется как отрицание как сбой . Аксиомы индукции также неявны и нужны только для доказательства свойств программы. Обратное рассуждение, как в разрешении SLD , которое является обычным механизмом, используемым для выполнения логических программ, неявно реализует регрессию. ${\ displaystyle Holds}$ ${\ displaystyle f}$ ${\ displaystyle Poss}$ ${\ displaystyle Initiates}$ ${\ displaystyle Terminates}$ ${\ displaystyle Poss}$ ${\ displaystyle \ gamma _ {F} ^ {+} ({\ overrightarrow {x}}, a, s)}$ ${\ displaystyle \ gamma _ {F} ^ {-} ({\ overrightarrow {x}}, a, s)}$ ${\ displaystyle \ leftarrow}$ ${\ displaystyle \ leftrightarrow}$

Смотрите также

Ссылки

Дж. Маккарти и П. Хейс (1969). Некоторые философские проблемы с точки зрения искусственного интеллекта . В Б. Мельцер и Д. Мичи, редакторы, Machine Intelligence , 4: 463–502. Издательство Эдинбургского университета, 1969.
Р. Ковальский (1979). Логика решения проблем - Elsevier North Holland.
К. Р. Апт и М. Безем (1990). Ациклические программы. В кн .: 7-я Международная конференция по логическому программированию. MIT Press. Иерусалим, Израиль.
Р. Рейтер (1991). Проблема фрейма в ситуационном исчислении: простое решение (иногда) и результат полноты для регрессии цели. В Владимир Лифшиц, редактор, Искусственный интеллект и математическая теория вычислений: статьи в честь Джона Маккарти , страницы 359–380, Сан-Диего, Калифорния, США. Академик Пресс Профессионал, Инк. 1991.
М. Шанахан (1997). Решение проблемы фрейма: математическое исследование закона инерции здравого смысла. MIT Press.
Х. Левеск, Ф. Пирри и Р. Рейтер (1998). Основы ситуационного исчисления . Электронные транзакции по искусственному интеллекту , 2 (3–4): 159-178.
Ф. Пирри и Р. Рейтер (1999). Некоторые вклады в метатеорию ситуационного исчисления. Журнал ACM , 46 (3): 325–361. DOI : 10,1145 / 316542,316545
Р. Райтер (2001). Знания в действии: логические основы для определения и реализации динамических систем. MIT Press.

Languages

In other projects