Временные многоагентные логики и проблема унификации

Модальные логики знания и времени являются одним из наиболее ин-
тенсивно развивающихся направлений исследования многомодальных ло-
гик, расположенным на стыке математической логики и информатики.
Особое внимание исследователей в данной теории, как и в целом в нестан-
дартных логиках, привлекает вопрос унификации формул. Ознакомиться
с наиболее важными результатами в данных областях исследования можно
по работам С. А. Крипке [43], Я. Хинтикка [34], С. Гиларди [27–31], В. В.
Рыбакова [8; 9; 46; 53; 60–63; 66; 67], Ф. Баадера [5–7], Д. Габбая [22–26], Э.
Ерабека [38–40] и В. Джика [15–17].
Теория модальных логик является сравнительно новым разделом ма-
тематической логики, хотя идея модальностей и изучения их свойств ухо-
дит своими корнями в античные времена. Вплоть до середины XX века
отдельные части данной дисциплины рассматривались только в области
философии. Образованию логического модального исчисления теория обя-
зана работам К. Льюиса [44; 45], позже — интенсивным исследованиям А.
Тарского [72], Дж. Маккинси [50], И. Йоханссона [41], С. Крипке [43], К.
Сегерберга [69; 70] и других.
Кратко модальные логики можно охарактеризовать, как логики, язык
которых, помимо стандартных логических связок, включает символы мо-
дальных операторов, имеющие различную интерпретацию в зависимости
от выбранной логической системы. Тем не менее, стандартными модальны-
ми операторами являются «необходимо, что» (символьно ) и «возможно,
что» (♦ соответственно) [14].
Модальные логики играют важную роль при проектировании систем,
предусматривающих элементы рассуждений о знаниях и времени [18]. В
последние десятилетия активное развитие получило направление много-
модальных логик, призванное обогатить выразительную способность клас-
сического модального языка как множеством новых логических операто-
ров, так и ограничением действия известных на определенные области дей-
ствия. Примером такой системы может служить временная логика, расши-
ренная посредством добавления операторов, представляющих будущее и
прошлое [26].
Временные логики являются особым типом модальных, предусмат-
ривающим качественное описание и рассуждение о том, как истинностное
значение определенного утверждения изменяется с течением времени, ис-
пользуя множество временных операторов или «модальностей». Стандарт-
ными временными операторами, соответствующими модальным, являются
«иногда», означающий истинность утверждения в какой-то доступный мо-
мент времени в будущем, и «всегда», гарантирующий истинность в любой
доступный в будущем момент. Временные логики активно развиваются в
областях математической логики, философии, Computer Science [23–25].
Первым исследование временных логик как модальных систем пред-
ложил в 1950-е А. Прайор [54], за последующие полвека данная область
стала сложной технической дисциплиной [24]. Значительные приложения
в области Computer Science имеет, в частности, линейная временная ло-
гика ℒ ℒ [47; 48; 74; 75]. Аксиоматизация для ℒ ℒ была впервые пред-
ложена Д. Габбаем [22], решение проблемы допустимости правил в ℒ ℒ
было найдено В. В. Рыбаковым [61], базис допустимых правил — С. В. Ба-
бёнышевым и В. В. Рыбаковым [8]. Наиболее распространенным является
подход к моделированию модального времени как транзитивной процеду-
ры [9;27–31;60;66], при котором любое временное состояние в будущем (или
в прошлом и будущем) является доступным из текущего момента времени.
Имеет место, однако, и идея возможного существования нетранзитивного
времени, исходящая, в информационном аспекте, из наблюдения, что пе-
реход знаний из прошлого в будущее может не всегда проходить гладко:
имеющееся знание в прошлом может не быть передано в настоящее. По-
дробное рассмотрение разных точек зрения на нетранзитивное время и его
выражение при помощи логических систем предложено в работах [67; 68].
Другим примером многомодальных логик являются логики Знания
[19; 20]: логики, дополненные модальностями , представляющими зна-
ния особых элементов, интерпретируемых как агенты, предназначенными
для моделирования эффектов и свойств знаний агентов в изменяющей-
ся среде. Одной из наиболее знаковых работ, положивших начало идеи
моделирования знания в терминах символической логики является книга
Я. Хинтикка [34], в которой было предложено использование модально-
стей для описания семантики знания. Значительные приложения агент-
ных логик найдены в различных областях знаний, таких как социология
(для изучения и моделирования когнитивного мышления и условий неопре-
деленности), биология и медицина (моделирование работы органов и си-
стем в организме, эволюционных процессов), и, конечно, информатика.
В работах [64; 65] В. В. Рыбаковым рассматривалась концепция ℎ
в многоагентной среде; исследовалась логика, моделирующая
неопределенность с точки зрения агентов [51]. В 1990-е активное разви-
тие получила концепция (общего знания), наиболее
полная формализация которой приведена в книге Р. Фагина [19]. В таком
подходе в качестве базового было принято знание агентов, представлен-
ное как 5-подобная модальность. В данной работе рассматриваются как
чисто временные, так и временные многоагентные логики, т.е. сочетаю-
щие в себе одновременно операторы времени и знания. Подобные системы
активно исследуются в последние десятилетия. В частности, Р. ван дер
Мэйден и Н. В. Шилов [73] показали неразрешимость линейной модаль-
ной логики знания и времени с операторами и
при возможной разрешимости некоторых ее фрагментов, в [32] исследова-
лась комбинация -логики с линейной временной логикой (при помо-
щи техники расслоения) в отношении моделей многоагентных систем, эво-
люционирующих с течением времени. В работах В. Ф. Юн [2–4] рассмат-
ривались вопросы аксиоматизируемости, финитной аппроксимируемости,
разрешимости в линейных временных логиках индуктивных фреймов, рас-
сматривался полимодальный случай [4]. В серии работ В. В. Рыбакова и
Э. Калардо [11–13] изучалась логика ℒ с операторами знаний агентов
, ∼ и линейного времени : построена аксиома-
тизация, доказана разрешимость по доказуемости формул и допустимости
правил вывода. В. В. Рыбаковым и С. В. Бабёнышевым рассматривалась
версия с оператором знания по взаимодействию с агентами ♦ℛ [62].
В основе используемых в работе методов и подходов лежит реляци-
онная семантика (иначе — семантика Крипке [43], в честь знаменитого
логика и философа С. А. Крипке) исследуемых логик. Это наиболее из-
вестная и (за исключением, возможно, алгебраической семантики) самая
изученная модальная семантика. Идеи потока времени, переходов между
вычислительными состояниями, сетей возможных миров могут быть пред-
ставлены в виде простых графических структур. При этом, модальная ло-
гика, интерпретациями которой являются такие идеи, предоставляет ин-
тересный инструментарий для работы с этими структурами и выражения
их внутренней информации. Такими графическими структурами являют-
ся фреймы (или шкалы) Крипке, представляющие собой множества с на-
борами отношений, используемыми для интерпретации логических симво-
лов [10; 14; 59], являющиеся центральным объектом семантики Крипке.
Одной из наиболее важных проблем, исследуемых в области нестан-
дартных логик, является допустимость правил вывода. Правило называ-
ется допустимым в логике , если для любой подстановки , из 1 , . . . , ∈
следует ∈ . Наиболее значительные результаты в этой области при-
надлежат В. В. Рыбакову, положительно решившему в 1984 г. проблему
Х. Фридмана [21] о существовании алгоритма, распознающего допусти-
мость правил вывода интуиционистской логики [56]; а позднее проблему
допустимости в широком классе модальных логик [57; 58] (все основные
результаты до 1997 г. описаны в монографии [59]).
Теория унификации является важным приложением логики в
Computer Science, на котором, в частности, основываются многие методы
автоматической дедукции и баз данных [5; 71]. В очень упрощенном виде,
унификация это попытка идентифицировать два символических выраже-
ния путем замены некоторых подвыражений (переменных) другими. Для
более полного определения обычно используются формулы, построенные
из функциональных символов [6] (к примеру , и , где — двумест-
ный, а и — нульместные). В этих терминах унификационная проблема
для формулы = ( , ) и = ( , ) формулируется в виде вопроса:
возможно произвести замену переменных , в и на другие перемен-
ные таким образом, что и стали бы (синтаксически) эквивалентными.
В данном конкретном примере, при подстановке вместо и вместо
, мы получим унифицирующую формулу ( , ). Такая подстановка обо-
значается как := { ↦→ , ↦→ } и применяется суффиксная запись:
= ( , ) = . Отметим, что различные вхождения тех же переменных
в унификационную проблему должны всегда заменяться теми же форму-
лами. По этой причине, формулы ′ = ( , ) и ′ = ( , ) не могут быть
унифицированы, т.к. это бы потребовало замены вхождения в ′ на , и
вхождения в ′ на иную константу .
С описанной точки зрения, с момента своего формирования в области
Computer Science, унификационная проблема состояла в ответе на вопрос:
возможна ли трансформация двух термов в один синтаксически эквива-
лентный заменой переменных другими термами [55]? Ключевые понятия
«унификация» и «наиболее общий унификатор» были предложены в рабо-
те Д. Кнута и П. Бендикса 1970 г. [42] в качестве инструментов тестиро-
вания Term Rewriting Systems для локального слияния путем вычисления
критических пар. Позже теория унификации вышла далеко за пределы
описанных дисциплин и, в настоящее время, играет важную роль во мно-
гих областях информатики и математики.
В частности, применительно к алгебраической интерпретации, име-
ет место классификация эквациональных теорий или переменных алгебр,
относительно типов унификации [15].
Пусть дана эквациональная теория Е и конечное множество пар пе-
ременных, называемое Е-унификационной проблемой:
(П): ( 1 , 1 ), . . . ,( , ).
Унификатор (решение) для (П) это подстановка , такая что
( 1 ) = ( 1 ), . . . , ( ) = ( ).
(П) называется унифицируемой (разрешимой), если существует по
крайней мере один унификатор. Подстановка называется более общей,
чем , если существует подстановка такая, что ∘ = .
Наиболее общий унификатор (сокр. mgu — most general unifier) ин-
терпретируется как «лучшее» решение унификационной проблемы (П).
Говорят, что эквациональная теория Е имеет унитарную унифика-
цию (или унификацию типа =1), если для любых двух унифицируемых
переменных 1 , 2 , существует mgu такой, что ( 1 ) = ( 2 ).
Другие унификационные типы принимаются «худшими» вариантами:
если существует конечно (бесконечно) много максимальных унификаторов
в стандартной формализации и в формализации со строгой импликацией,
для некоторых переменных, тогда Е имеет финитарный (инфинитарный)
тип унификации. Если же не существует максимального унификатора, то-
гда Е имеет унификационный тип = 0 (наихудший из возможных, нуль-
арный тип). Следовательно, символьно типы унификации могут быть за-
писаны как = 1 (унитарный), = (финитарный), = inf (инфинитарный) и
= 0 (нульарный).
Вопросы унификации и унификационных типов многообразия алгебр
могут быть переформулированы для многообразия соответствующих ло-
гик [28]. С этой точки зрения, в языке логики ℒ рассматривается формула
, унификатором для которой в ℒ называется подстановка такая, что
ℒ ( ). Таким образом, в нестандартных логиках формула называется
унифицируемой, если такой унификатор существует, а базовая проблема
унификациии эквивалентна (и чаще рассматривается в виде) возможности
формулы стать теоремой после замены переменных, с сохранением значе-
ний коэффициентов-параметров [27; 28; 53; 57].
Классическое пропозициональное исчисление обладает лучшим уни-
фикационным типом — унитарной унификацией [49] (соответственно с уни-
тарным типом Е-унификации для булевых алгебр): для любой формулы А,
если существует подстановка такая, что ( ) доказуема, тогда также су-
ществует «лучшая» подстановка с этим свойством, т.е. такая , что ( )
доказуема и любая подстановка такая, что ( ) доказуема, относительно
эквивалентности является конкретизацией . Унификационные алгоритмы
поиска mgu в булевых алгебрах описаны в работе [49].
Существуют ли другие логические исчисления, обладающие тем же
свойством, в частности модальные исчисления? Отрицательный ответ на
этот вопрос был дан для всех модальных логик, обладающих дизъюнктив-
ным свойством [35]: формула ∨ ¬ унифицируема в соответствующей
логике ℒ и имеет следующие унификаторы: