Временная интранзитивная мульти-агентная логика; алгоритмы разрешимости, правила вывода

Актуальность темы. С начала 2000-х годов перспективным и быстро
развивающимся стало направление модальных и много-модальных пропози-
циональных логик, описывающих рассуждения, доказательства и процессы
вычислений. Такие логики позволяют перейти от языка, выражающего про-
стые факты и утверждения, к более богатому и выразительному. Они имеют
дело с высказываниями, содержащими в себе такие модальности, как воз-
можно, необходимо, до тех пор, пока . . . и т.д., которые нельзя выразить с
помощью языка классических пропозициональных логик. Более широкая вы-
разительность достигается посредством добавления к классической пропози-
циональной системе одного или нескольких модальных операторов (обычно
или ♦).
Обычно модальные операторы читаются как «необходимо, что…», «воз-
можно, что…», однако, существует великое множество различных интерпре-
таций. В случае временных логик, модальное выражение p может быть
истолковано как «всегда в будущем верно p», а ♦p – «существует момент в
будущем, когда верно p». Такой язык эффективен при описании процессов
во времени. Причем любую временную логику можно расширить до много-
модальной посредством добавления операторов, представляющих будущее и
прошлое [20]. Такие логики нашли широкое применение при изучении ис-
кусственного интеллекта (AI) и в компьютерных науках (CS), для проверки
корректности вычислительных программ [31, 32, 34, 35, 22, 15].
Еще одним примером много-модальных логик являются логики Знания
[18, 17, 25] с модальностями, представляющими знания агентов. Они приме-
нимы для формализации утверждений об агентах, обладающих некоторой
неполной информацией. Такие эпистемические модели имеют свой предел
выразимости: с их помощью трудно описать процесс изменения информации,
доступной агенту. Добавление временной модальности в таком случае рас-
ширяет описательные возможности языка. Наиболее естественным является
внедрение логики знания в рамки временной логики. Таким образом, получим
много-модальную систему, сочетающую временные операторы и операторы
знания. Хорошо известно, что такие системы образуют богатый, выразитель-
ный и интуитивно понятный язык [18], [54], [26].
Модели, порожденные сочетанием операторов, представляющих время и
знание агентов эффективно зарекомендовали себя в описании взаимодей-
ствия между различными агентами в потоке времени [18], [20], [26], [13], [12],
[16]. Они получены добавлением к классической пропозициональной системе
двух видов модальностей: для моделирования потока времени и для опи-
сания знания агентов. Полученный язык позволяет описывать ситуации, в
которых агенты, обладающие определенными знаниями, оперируют ими в
процессах рассуждений и вычислений, использующих пошаговые стратегии,
имитирующие время. Изучение подобных систем активно развивается с се-
редины 90-х годов. Например, Р. ван дер Мэйден и Н.В. Шилов [55] изучали
линейную модальную логику Знания и Времени с модальными оператора-
ми until и common knowledge и показали (Теорема 1 [55]), что эта логика не
разрешима. В серии работ В.В. Рыбакова и Э. Калардо [11], [13] изучалась
линейная много-модальная логика Знания и Времени LT K с операторами
знания агентов Ki , оператором common knowledge ∼ и оператором време-
ни true from now on T . Было доказано, что такая логика разрешима от-
носительно доказуемости формул и допустимости правил вывода. В статье
В.В. Рыбакова и С.В. Бабёнышева [46] рассматривается много-модальная ло-
гика с оператором knowledge by interaction with agents ♦R . В книге Р. Фагина
и др. [18] (Глава 4.3, Knowledge and Multi-Agent Systems: Incorporating time)
предложено сочетание логики LT L (Linear Time Logic) и оператора knowledge
base KKB . Полная аксиоматизация целого ряда различных логик с условиями
на знание и время (с операторами next, until, и операторами знания агентов)
представлена в работе Й. Халперна [25]. В [33] рассмотрено вычислительное
дерево логики знания (computation tree logic of knowledge (CTLK)), применя-
емое для проверки эпистемических свойств мульти-агентных систем.
С развитием компьютерных наук возрос интерес к изучению допустимых
правил вывода для неклассических логик. Изучение искусственного интел-
лекта нуждается в языке, приспособленном для описания различных динами-
ческих систем, и язык много-модальных логик успешно справляется с этим.
Изначально, факты и утверждения описываются с помощью формул в этом
языке, которые не способны выразить изменяющиеся условия и предпосыл-
ки. На помощь приходит применение правил вывода или секвентов, кото-
рые выражают логическое следование от условий (посылок) к заключениям,
представляющим собой выводы или факты, которые можно получить из име-
ющихся предпосылок. Тем самым, правила вывода предоставляют нам более
тонкий и выразительный аппарат для моделирования процессов мышления
и вычислений.
Правило вывода – это схема, регламентирующая допустимые способы пе-
рехода от некоторой совокупности формул α1 , . . . , αn , называемых посылка-
ми, к некоторой определенной формуле β, называемой заключением. Непо-
средственным изучением правил вывода впервые занялись Е. Лось (1955),
А. Тарский (1956) и Р. Сушко (1958). Правило вывода называется истинным
в логике λ, если из того, что α1 , . . . , αn ∈ λ следует β ∈ λ. Правило выво-
димо (доказуемо) в λ, если заключение β выводится из посылок α1 , . . . , αn с
помощью аксиом и постулированных правил логики λ. Понятие допустимо-
го правила вывода было впервые введено П. Лоренценем [30] в 1955 г. Для
произвольной логики допустимыми являются те правила, которые не изменя-
ют множество доказуемых теорем данной логики (т.е. правила, относитель-
но которых логика замкнута). Формально, правило считается допустимым
в λ, если при любой подстановке ε, из α1ε , . . . , αnε ∈ λ следует, что β ε ∈ λ.
Понятно, что любое доказуемое правило является допустимым в заданной
логике. Таким образом, множество всех допустимых в логике λ правил об-
разует наибольший класс правил вывода, которыми мы можем расширить
аксиоматическую систему λ, не изменяя множества доказуемых теорем.
Начало истории изучения допустимых правил может быть датировано
1975 г. с появления проблемы Х. Фридмана о существовании алгоритмиче-
ского критерия допустимости правил в интуиционистской логике Int [19]. В
классической логике вопрос допустимости решался тривиально – допустимы
только доказуемые правила. Однако, в логиках первого порядка, модальных
и суперинтуиционистских логиках существуют допустимые, но не доказуемые
правила вывода. В 1960 г. П. Харроп в работе [27] показал, что в логике Int
допустимо, но не доказуемо ¬x → (y ∨ z)/(¬x → y) ∨ (¬x → z). Г. Е. Минц в
[2] доказал, что если правило r допустимо в Int и не содержит связок → или
∨, то r выводимо в Int, и показал, что правило ((x → y) → (x ∨ y))/(((x →
y) → x) ∨ ((x → y) → z)) допустимо, но не доказуемо в Int. В модальных
логиках S4, S4.1, Grz допустимо, но не доказуемо правило Леммона-Скотта
( ( ♦ p → p) → ( p ∨ ¬ p))/ ♦ p ∨ ¬ p, [28, 29, 43]. Таким об-
разом, возникли вопросы алгоритмической разрешимости задачи распозна-
вания допустимых правил вывода.
Положительное решение проблемы Фридмана о существовании алгорит-
ма, распознающего допустимость правил вывода интуиционистской логики
Int, было получено В.В. Рыбаковым в 1984 г. [36]. При развитии теории до-
пустимых правил вывода для неклассических логик, В.В. Рыбаков положи-
тельно решил проблему допустимости правил вывода в широком классе мо-
дальных логик, в частности для K4, S4, Grz, GL и многих других [8] – [6],
[38] – [42].
В работе [36] В.В. Рыбаковым был использован специальный метод для
разрешения проблемы допустимости правил вывода, который нашел свое
применение во многих последующих исследованиях. Суть его заключается
в том, что для всякого правила вывода существует конечное, с точностью до
изоморфизма, множество конечных моделей Крипке специального вида, на
элементах которых можно проверять истинность правила, для выяснения его
допустимости. Несмотря на успехи в решении проблем допустимости правил
вывода в различных логиках, данный метод имеет свои ограничения: он при-
меним только для финитно-аппроксимируемых логик, поскольку только в
этом случае можно эффективно описать n-характеристическую модель логи-
ки. Одним из условий существования алгоритмов разрешимости допустимых
правил вывода логики является ее обычная разрешимость относительно до-
казуемости формул [43]. Напомним, что логика разрешима, если существует
процедура, позволяющая по произвольной формуле определить, принадле-
жит ли она логике. Во многих случаях доказательство разрешимости логики
сводится к доказательству того, что она обладает свойством конечных моде-
лей (так называемым свойством финитной аппроксимируемости), т.е. что
она полна относительно некоторого класса конечных фреймов Крипке (Тео-
рема Харропа).
Совместно со своими учениками В.В. Рыбаков исследовал вопрос разре-
шимости относительно доказуемости формул и допустимости правил вывода
многих много-модальных логик, в том числе и логик, использующих опера-
торы знания и времени [48], [23], [47]. В работе Э. Калардо и В.В. Рыбакова
[11] было показано, что много-модальная логика LT K с транзитивным и ре-
флексивным отношением времени является разрешимой относительно дока-
зуемости формул. А в [12] доказано, что данная логика является разрешимой
относительно допустимости правил вывода. А.В. Кошелева в своей работе [1]
изучила проблемы разрешимости много-модальных S5t -логик. В [46] С.В. Ба-
бёнышев и В.В. Рыбаков доказали, что временная транзитивная логика S4T
с добавлением операторов знания агентов разрешима.
Несмотря на активные исследования в сфере допустимых правил выво-
да, большая часть результатов получена для транзитивных логик. При этом
особый интерес представляют нетранзитивные логики, так как они более вос-
требованы в computer science. Выяснилось, что для нетранзитивных логик
не удается напрямую применять основные результаты и техники, использу-
емые при исследовании допустимых правил вывода логик с транзитивными
отношениями достижимости. Как было отмечено, при исследовании допусти-
мых правил вывода центральную роль играют n-характеристические моде-
ли Крипке. Однако, построение таких моделей является достаточно ясным
только для расширений модальной логики K4 и интуиционистской логики.
В нетранзитивном случае модели описаны только для очень малого списка
логик. В работе [14] была представлена n-характеристическая модель для ми-
нимальной логики K. В [24] описана схема построения n-характеристической
модели временной логики с нетранзитивным оператором времени завтра, и
найден критерий допустимости правил вывода рассматриваемой логики. Так-
же проблема допустимости правил вывода была решена для нетранзитивной
временной логики конечных интервалов [45] и логики LT LP ast , которая соче-
тает в себе операторы знания агентов и нетранзитивный временной оператор
since [53].
Результаты, представленные в диссертации, продолжают серию работ
В.В. Рыбакова по исследованию свойств мульти-агентной логики Знания и
Времени LT K. В работах [11] – [13] исследована логика LT K c транзитивным
и рефлексивным отношением времени. Было доказано, что данная логика
обладает свойством финитной аппроксимируемости и является разрешимой
относительно доказуемости формул и допустимости правил вывода. Также
в [11] представлена конечная аксиоматизация LT K. Однако, если предпо-
ложить, что отношение времени не является транзитивным, то полученные
результаты и технику исследования нельзя перенести на данный случай. Ме-
тоды, используемые в [11] – [13] оказываются явным образом не применимы
при интранзитивном отношении достижимости по времени.
В диссертационной работе представлена мульти-агентная логика Знания
и Времени LT Kr с интранзитивным и рефлексивным отношением времени.
Язык LT Kr содержит временной оператор сегодня и завтра T , оператор
всеобщего знания (common knowledge) ∼ и несколько операторов знания
агентов i . Такая логика применима при описании моделей, в которых время
рассматривается как линейная дискретная последовательность состояний, со-
держащих в себе набор информационных узлов. Интранзитивность времени в
данном контексте понимается следующим образом: на информационном узле
актуальна только та информация, которая доступна либо в данный момент,
либо будет доступна в следующий. Такие модели применимы в программном
обеспечении, в области Интернет и в алгоритмах поиска.
Цель работы.
1. Выяснить, является ли линейная много-модальная логика Знания и
Времени LT Kr с интранзитивным и рефлексивным отношением времени
финитно-аппроксимируемой и разрешимой.
2. Исследовать разрешимость проблемы допустимости правил вывода ло-
гики LT Kr . Предоставить алгоритм, который по заданному правилу r опре-
деляет, допустимо ли правило вывода r в LT Kr .
Методика исследования.
Используются языки модальных и много-модальных логик, в том числе
язык временных логик. В качестве основного инструмента исследования при-
меняется семантика Крипке, расширенная на много-модальный и временной
случаи. Также применяются общие методы теоретико-модельной семантики
для пропозициональных нестандартных логик. Например, метод фильтра-
ции, метод редуцирования правил вывода, семантический критерий допусти-
мости правил вывода с помощью n-характеристических моделей.
Научная новизна. Все результаты, представленные в диссертации, яв-
ляются новыми и снабжены подробными доказательствами. Результаты сов-
местных работ получены в нераздельном соавторстве.
Основные результаты. В диссертационной работе семантически опре-
делена линейная интранзитивная много-модальная логика LT Kr , сочетаю-
щая модальные операторы знания и времени, получены следующие основные
результаты:
1. Доказана финитная аппроксимируемость и, как следствие, разреши-
мость линейной много-модальной логики Знания и Времени LT Kr с интран-
зитивным и рефлексивным отношением времени.
2. Получены необходимое и достаточное условия допустимости правил
вывода в логике LT Kr .
Первый из основных результатов получен автором самостоятельно, вто-
рой результат получен совместно с В.В. Рыбаковым при равном участии обе-
их сторон.
Теоретическая и практическая ценность. Результаты, представлен-
ные в диссертации, носят теоретический характер и могут быть использованы
в дальнейших исследованиях свойств много-модальных интранзитивных ло-
гик, а также в таких областях, как теория моделей, теория графов и computer
science.
Апробация работ. Результаты диссертации докладывались на