Временная интранзитивная мульти-агентная логика тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

На правах рукописи

Лукьянчук Александра Николаевна

ВРЕМЕННАЯ ИНТРАНЗИТИВНАЯ

МУЛЬТИ-АГЕНТНАЯ ЛОГИКА; АЛГОРИТМЫ РАЗРЕШИМОСТИ, ПРАВИЛА ВЫВОДА

01.01.06 - математическая логика, алгебра и теория чисел

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

г■■ мг ?015

00556160В

Красноярск 2015

005561606

Работа выполнена в ФГАОУ ВПО «Сибирский федеральный университет»

Научный руководитель: доктор физико-математических наук, профессор

Рыбаков Владимир Владимирович

Официальные оппоненты: Яшин Александр Данилович,

доктор физико-математических наук, доцент, ГБОУ ВПО «Московский городской психолого-педагогический университет» кафедра прикладной математики, профессор;

Юн Вета Федоровна, кандидат физико-математических наук, Федеральное государственной бюджетное учреждение науки «Институт математики им. С.Л. Соболева Сибирского отделения Российской академии наук»

лаборатория теории вычислимости и прикладной логики, старший научный сотрудник;

Ведущая организация: ФГБОУ ВПО «Иркутский государственный университет»

Защита состоится 2 октября 2015 г. в 11.00 часов на заседании диссертационного совета Д 212.099.02 при ФГАОУ ВПО «Сибирский федеральный университет» по адресу: 660041, г. Красноярск, пр. Свободный, 79, ауд. 8-06.

С диссертацией можно ознакомиться в библиотеке ФГАОУ ВПО «Сибирский федеральный университет» и на сайте http://www.sfu-kras.ru.

Автореферат разослан « августа 2015 г.

Ученый секретарь диссертационного совета

/

Федченко Дмитрий Петрович

Общая характеристика работы

Актуальность темы

С начала 2000-х годов перспективным и быстро развивающимся стало направление модальных и много-модальных пропозициональных логик, описывающих рассуждения, доказательства и процессы вычислений. Такие логики позволяют перейти от языка, выражающего простые факты и утверждения, к более богатому и выразительному. Они имеют дело с высказываниями, содержащими в себе такие модальности, как возможно, необходимо, до тех пор, пока ... и т.д., которые нельзя выразить с помощью языка классических пропозициональных логик. Более широкая выразительность достигается посредством добавления к классической пропозициональной системе одного или нескольких модальных операторов (обычно □ или «СО-

Обычно модальные операторы читаются как «необходимо, что...», «возможно, что...», однако, существует великое множество различных интерпретаций. В случае временных логик, модальное выражение □ р может быть истолковано как «всегда в будущем верно р», а 0р- «существует момент в будущем, когда верно р». Такой язык эффективен при описании процессов во времени. Причем любую временную логику можно расширить до много-модальной посредством добавления операторов, представляющих будущее и прошлое. Такие логики нашли широкое применение при изучении искусственного интеллекта (А1) и в компьютерных науках (СБ), для проверки корректности вычислительных программ.

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

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

использующих пошаговые стратегии, имитирующие время. Изучение подобных систем активно развивается с середины 90-х годов. Например, Р. ван дер Мэйден и Н.В. Шилов исследовали линейную модальную логику Знания и Времени с модальными операторами until и common knowledge в работе

В серии статей 2' 3' 4 Э. Калардо и В.В. Рыбаков рассмотрели линейную много-модальную логику Знания и Времени LTK с операторами знания агентов Ki, оператором common knowledge CL и оператором времени true from now on □ т- В статье В.В. Рыбакова и С.В. Бабёнышева 5 рассматривается много-модальная логика с оператором knowledge by interaction with agents <)и-В книге 6 (Глава 4.3, Knowledge and Multi-Agent Systems: Incorporating time) предложено сочетание логики LTL (Linear Time Logic) и оператора knowledge base Ккв- Полная аксиоматизация целого ряда различных логик с условиями на знание и время (с операторами next, until, и операторами знания агентов) представлена в работе И. Халперна и др. 7.

С развитием компьютерных наук возрос интерес к изучению допустимых правил вывода для неклассических логик. Изучение искусственного интеллекта нуждается в языке, приспособленном для описания различных динамических систем, и язык много-модальных логик успешно справляется с этим. Изначально, факты и утверждения описываются с помощью формул, которые не способны выразить изменяющиеся условия и предпосылки. На помощь приходит применение правил вывода или секвентов, которые выражают логическое следование от условий (посылок) к заключениям, представляющим собой выводы или факты, которые можно получить из имеющихся предпосылок. Тем самым, правила вывода предоставляют нам более тонкий и выразительный аппарат для моделирования процессов мышления и вычислений.

Правило вывода - это схема, регламентирующая допустимые способы перехода от некоторой совокупности формул Qi,..., ап, называемых посылками, к некоторой определенной формуле j3, называемой заключением. Непосредственным изучением правил вывода впервые занялись Е. Лось (1955), А. Тар-ский (1956) и Р. Сушко (1958). Правило вывода называется истинным в логике А, если из того, что ап G А следует (3 S А. Правило выводимо (дока-

'Van der Meyden R., Shilov N.V. Model chccking knowledge and time in systems with perfect recall // Lecture Notes in Computer Science, Springer, 1999, V. 1738, P. 432^(45.

2Calardo E., Rybakov V. V. Combining time and knowledge, semantic approach // Bulletin of the Section of Logic,

2005, V. 34, № 1, P. 13-21.

3Calardo E., Admissible inference rules in the linear logic of knowledge and time LTK // Logic Journal of the IGPL,

2006, V. 14, № 1, P. 15-34.

4Calardo E., Rybakov V.V. An axiomatisation for the multi-modal logic of knowledge and linear time LTKЛ Logic Journal of the IGPL, 2007, V. 15, № 3, P. 239-254.

5Rybakov V.V., Babenyshev S.V. A Hybrid of Tencse Logic S&t and Multi-Agent Logic with Interacting Agents // Journal of Siberian Federal University. Mathematics & Physics, 2008, V. 1, № 4, P. 399^409.

'Fagin R„ Halpern J.Y., Moses Y., Vardi M.Y. Reasoning About Knowledge // Massachussets, Cambridge, MIT Press. 1995, 491 p.

'Halpern J.Y., Shore R„ Vardi M.Y. Complete Axiomatization for Reasoning About Knowledge and Time// SIAM Journal on Computing, 2004, V. 33, № 3, P. 674-703.

зуемо) в А, если заключение ß выводится из посылок cii,..., ап с помощью аксиом и постулированных правил логики Л. Понятие допустимого правила вывода было впервые введено П. Лоренценем в 1955 г. Для произвольной логики допустимыми являются те правила, которые не изменяют множество доказуемых теорем данной логики (т.е. правила, относительно которых логика замкнута). Формально, правило считается допустимым в А, если при любой подстановке е, из ,..., £ А следует, что ߣ £ А. Понятно, что любое доказуемое правило является допустимым в заданной логике. Таким образом, множество всех допустимых в логике А правил образует наибольший класс правил вывода, которыми мы можем расширить аксиоматическую систему А, не изменяя множества доказуемых теорем.

Начало истории изучения допустимых правил может быть датировано 1975 г. с появления проблемы X. Фридмана о существовании алгоритмического критерия допустимости правил в интуиционистской логике Int. В классической логике вопрос допустимости решался тривиально - допустимы только доказуемые правила. Однако, в логиках первого порядка, модальных и суперинтуиционистских логиках существуют допустимые, но не доказуемые правила вывода. В 1960 г. П. Харроп в работе 8 показал, что в логике Int допустимо, но не доказуемо ->х —> (у V z)/(->x —» у) V (-а —> z). Г. Е. Минц в 9 доказал, что если правило г допустимо в Int и не содержит связок —> или V, то г выводимо в Int, и показал, что правило ((ж —> у) —> (х V у))/({(х —> у) —> х) V ((х —» у) —> z)) допустимо, но не доказуемо в Int. В модальных логиках 54, 54.1, Grz допустимо, но не доказуемо правило Леммона-Скотта □(□(□фШр -> üp) (□pVD-'Dp))/DOüpVD-'Dp. Таким образом, возникли вопросы алгоритмической разрешимости задачи распознавания допустимых правил вывода.

Положительное решение проблемы Фридмана о существовании алгоритма, распознающего допустимость правил вывода интуиционистской логики Int, было получено В.В. Рыбаковым в 1984 г. При развитии теории допустимых правил вывода для неклассических логик В.В. Рыбаков положительно решил проблему допустимости в широком классе модальных логик, в частности для КА, 54, Grz, GL и многих других.

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

8Нагтор R. Concerning Formulas of the Types A В V С, A -> 3xB(x) II Journal of Symbolic Logic, 1960, V. 25, № 1, P. 27-32.

9Минц Г.Е. Производность допустимых правил // Записки научного семинара ЛОМИ АН СССР, 1972, № 32, С. 85-99.

10Rybakov V.V. A criterion for admissibility of rules in the modal system S4 and the intuitionistic logic // Algebra and Logic (Eng. Ed.), 1984, V. 23, № 5, P. 369-384.

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

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

Несмотря на активные исследования допустимых правил вывода, большая часть результатов получена для транзитивных логик. При этом особый интерес представляют нетранзитивные логики, так как они более востребованы в computer science. Выяснилось, что для нетранзитивных логик не удается напрямую применять основные результаты и техники, используемые при исследовании допустимых правил вывода логик с транзитивными отношениями достижимости. Как было отмечено в работе 10, при исследовании допустимых правил вывода центральную роль играют так называемые п-характеристические модели Крипке. Однако, построение таких моделей является достаточно ясным только для расширений модальной логики К А и интуиционистской логики. В нетранзитивном случае модели описаны только для очень малого списка логик. В работе 11 была представлена n-характеристическая модель для минимальной логики К. В 12 описана схема построения п-характеристической модели временной логики с нетранзитивным оператором времени завтра, и найден критерий допустимости правил вывода рассматриваемой логики. Также проблема допустимости правил вывода была решена для нетранзитивной временной логики конечных интервалов и логики LTLpast, которая сочетает в себе операторы знания агентов и нетранзитивный временной оператор since.

Результаты, представленные в диссертации, продолжают серию работ В.В. Рыбакова и Э. Калардо по исследованию свойств мульти-агентной логики Знания и Времени LTK. Ими была исследована логика LTK с транзитивным и рефлексивным отношением времени. Было доказано, что данная логика обладает свойством финитной аппроксимируемости и является разрешимой относительно доказуемости формул и допустимости правил вывода. Также представлена конечная аксиоматизация LTK. Однако, если предположить, что отношение времени не является транзитивным, то полученные ре-

"Chagrov А.V., Zakharyaschev M.V. Modal Logic // London, Cambridge Press, 1997, 589 p.

,2Golovanov M.I., Rybakov V.V., Yurasova E.M. A necessary condition for mies to be admissible in temporal tomorrow-logic II Bulletin of the section of Logic, 2003, V. 32, № 4, P. 213-220.

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

В диссертационной работе представлена мульти-агентная логика Знания и Времени ЬТКт с интранзитивным и рефлексивным отношением времени. Язык ЬТКГ содержит временной оператор сегодня и завтра Пт, оператор всеобщего знания (common knowledge) CL и несколько операторов знания агентов □,. Интранзитивность времени в данном случае понимается следующим образом: на информационном узле актуальна только та информация, которая доступна либо в данный момент, либо будет доступна в следующий. Данная логика подходит для описании моделей, в которых время рассматривается как линейная дискретная последовательность состояний, содержащих в себе набор информационных узлов. Такие модели применимы в программном обеспечении, в области Интернет и в алгоритмах поиска.

Цель диссертации

Семантически определить линейную много-модальную логику Знания и Времени ЬТКГ с интранзитивным и рефлексивным отношением времени и выяснить:

1. является ли логика LTKT финитно-аппроксимируемой и разрешимой;

2. разрешима ли проблема допустимости правил вывода LTKr. Предоставить алгоритм, который по заданному правилу г определяет, допустимо ли г в LTKr.

Методика исследования

Используются языки модальных и много-модальных логик, в том числе язык временных логик. В качестве основного инструмента исследования применяется семантика Крипке, расширенная на много-модальный и временной случаи. Также применяются общие методы теоретико-модельной семантики для пропозициональных нестандартных логик. Например, метод фильтрации, метод редуцирования правил вывода, семантический критерий допустимости правил вывода с помощью n-характеристических моделей.

Научная новизна

Все результаты, представленные в диссертации, являются новыми и снабжены подробными доказательствами. Результаты совместных работ получены в нераздельном соавторстве.

Теоретическая и практическая ценность

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

Практическое применение полученных результатов состоит в их внедрении в учебный процесс в виде материала для проведения специальных курсов кафедры алгебры и математической логики Института математики и фундаментальной информатики Сибирского федерального университета.

Степень достоверности и апробация работы

Достоверность научных результатов обеспечена опорой на современные методы исследования много-модальных неклассических логик: р-морфизмы и подмодели, метод канонических моделей, метод фильтрации для перехода от бесконечных моделей к конечным, критерий Рыбакова допустимости правил вывода.

Основные результаты диссертации обсуждались и докладывались на следующих конференциях: VIII всероссийской научно-технической конференции студентов, аспирантов и молодых ученых, посвященной 155-летию со дня рождения К.Э. Циолковского (Красноярск, 2012); VII всесибирском конгрессе женщин-математиков (Красноярск, 2012); международной конференции серии "Мальцевские чтения"(Новосибирск, 2012, 2013, 2015); международной конференции, посвященной памяти В.П. Шункова "Алгебра и Логика: Теория и Приложения"(Красноярск, 2013); международной конференции "Алгебра и математическая логика: теория и приложения"(Казань, 2014).

Основные публикации

Основные результаты диссертации опубликованы в работах [1] - [9], из них 2 работы [1], [2] в ведущих рецензируемых изданиях, рекомендованных ВАК.

В нераздельном соавторстве выполнены четыре работы [2], [5], [6], [9].

Структура и объем работы

Диссертация состоит из введения, четырех глав, разбитых на разделы, и списка литературы из 64 наименований. Общее число страниц диссертационной работы - 73. Все утверждения (теоремы, леммы, следствия, определения и используемые формулы) пронумерованы двумя числами: первое является номером главы, второе - порядковым номером утверждения в рамках главы.

Содержание работы

Во введении обосновывается актуальность выбранной в диссертационной работе темы. Дается краткий обзор истории исследования много-модальных логик и допустимых правил вывода. Сформулирован предмет, цель и методы проведения исследования, указаны основные его результаты. Приведен список конференций, на которых была проведена апробация работ по изучаемой теме, также дается обзор основных разделов диссертационной работы.

Первая глава посвящена необходимым предварительным сведениям.

В §1 даются общие сведения из области модальных и много-модальных логик, приводятся основные факты семантики Крипке для модальных и многомодальных логик. Также приведены необходимые определения и утверждения о канонических моделях и методе фильтрации моделей Крипке.

В §2 включены основные необходимые определения и теоремы теории допустимых правил вывода.

Вторая глава посвящена семантическому описанию логики ЬТКГ, как множества формул, истинных на фреймах специального вида, называемых ¿Т/Сг-фреймами.

В §3 дано определение ЬТКГ-фреймов и указаны наиболее важные их свойства. На основе этих свойств приводится одна из возможных интерпретаций моделей такого вида.

В §4 рассмотрены фреймы, содержащие конечные циклы сгустков. Изначально, определение ЬТКт-фрейма не предусматривает наличие циклов в линейной цепи ЬТКт-фрейма, однако, в Леммах 2.1 и 2.1 доказано, что фреймы, содержащие циклы сгустков конечной длины, являются р-морфными образами ЬТКГ-фреймов и адекватны ЬТКГ.

В §5 вводится много-модальный язык С.ьтк и стандартным образом определяется множество формул соответствующего языка. Логикой ЬТКГ называем множество всех формул в языке Сьтк, истинных на /уТЛ",.-фреймах. Также в §5 отмечено свойство перестановочности модальных операторов Шу и Си, а также От и в логике ЬТКГ.

В §6 приводится некоторая система аксиом АБ1ткг- Доказывается, что фрейм п-канонической модели, построенной на основе данной системы, обладает основными свойствами ЬТКт-фрейма. Сформулирована гипотеза о том, что АБ1ткг является конечной аксиоматизацией логики ЬТКГ.

Глава 3 целиком посвящена вопросу разрешимости логики ЬТКт относительно доказуемости формул. В Теореме 3.1 доказано, что ЬТКГ обладает свойством финитной аппроксимируемости. На основе этого строится алгоритм, с помощью которого можно для произвольной формулы в языке

С1ТК

за конечное количество шагов установить, принадлежит ли формула логике. Таким образом, имеет место первый из основных результатов диссертационной работы:

Теорема 3.2 Логика LTKT разрешима.

В главе 4 решается задача разрешимости логики LTKr относительно допустимости правил вывода. Её решение основано на семантическом критерии допустимости правил вывода с помощью n-характеристических моделей.

В §7 строится специальная модель ChiTKr{n) и доказывается, что она является n-характеристической для логики LTKr.

Однако, в Лемме 4.2 установлено, что элементы данной модели не является формульными, что не позволяет напрямую применять метод из 10. Чтобы обойти данную проблему, в §8 строится специальная конечная LTA^-модель, особое строение которой позволило сформулировать и доказать необходимое и достаточное условия недопустимости произвольного правила вывода в редуцированной нормальной форме в логике ЬТКт. Таким образом, доказан второй основной результат диссертации:

Теорема 4.1 Логика LTKr разрешима относительно допустимости правил вывода.

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

Основные результаты

В диссертационной работе семантически определена линейная интранзи-тивная много-модальная логика LTKT, сочетающая модальные операторы знания и времени, получены следующие основные результаты:

1. Доказана финитная аппроксимируемость и, как следствие, разрешимость линейной много-модальной логики Знания и Времени LTKr с интранзитив-ным и рефлексивным отношением времени.

2. Получены необходимое и достаточное условия допустимости правил вывода в логике ЬТКГ.

Первый из основных результатов получен автором самостоятельно, второй результат получен совместно с В.В. Рыбаковым при равном участии обеих сторон.

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

Публикации по теме диссертации Статьи в журналах из перечня ВАК

[1] Lukyanchuk A.N. Decidability of multi-modal logic LTK of linear time and knowledge // Journal of Siberian Federal University. Mathematics & Physics 2013. V. 6. № 2. P. 220-226.

[2] Лукьянчук А.Н., Рыбаков В.В. Допустимые правила вывода линейной логики знания и времени ЬТКт с интранзитивным отношением времени // Сибирский математический журнал. 2015. Т. 56. № 3. С. 573-593.

Прочие публикации

[3] Лукьянчук А.Н. Некоторые свойства линейной логики знания и времени LTK II Материалы VIII всерос. научно-технической конф. студ., аспир. и мол. ученых, посвящ. 155-летию со дня рождения К.Э.Циолковского. [Электронный ресурс] Красноярск : СФУ. 2012. № заказа 7880/отв. ред. О.А.Краев.

[4] Лукьянчук А.Н. Разрешимость линейной логики знания и времени // Сборник тезисов VII всесибирского конгресса женщин-математиков. Красноярск : СФУ. 2012. С.128-129.

[5] Лукьянчук А.Н., Римацкий В.В. О конечной аксиоматизации линейной логики знания и времени ЬТКт с интранзитивным отношением времени // Тезисы докладов междунар. конф. «Мальцевские чтения». [Электронный ресурс] Новосибирск: НГУ. 2013. С.53.

[6] Лукьянчук А.Н., Римацкий В.В. Аксиоматизация линейной логики Знания и Времени LTKr I/ Тезисы докладов междунар. конф. «Алгебра и Логика: Теория и Приложения», посвящ. памяти В.П. Шункова. Красноярск: СФУ. 2013. С.87.

[7] Лукьянчук А.Н. О допустимости правил вывода линейной логики знания и времени ЬТКт с интранзитивным отношением времени // Материалы междунар. конф. «Алгебра и математическая логика: теория и приложения» и сопут. мол. летн. шк. «Вычислимость и вычислимые структуры». Казань: КФУ. 2014. С.97.

[8] Лукьянчук А.Н. Допустимые правила вывода линейной логики Знания и Времени ЬТКт с интранзитивным отношением времени. Гипотеза о конечной аксиоматизируемости LTKT II Тезисы докладов междун. конф. «Мальцевские чтения», посвя. 75-летию Ю. Л. Ершова. Новосибирск: НГУ. 2015. С. 214.

[9] Lukyanchuk A.N., Rybakov V.V. Linear Intransitive Temporal Logic of Knowledge LTKr, Decision Algorithms, Inference Rules // Cornell University Library, AzXiv.org, arXiv:1407.7136 [cs.LO],

Подписано в печать 04.08.2015. Печать плоская. Формат 60x84/16 Бумага офсетная. Усл. печ. л. 0,85. Тираж 100 экз. Заказ 2342

Отпечатано Библиотечно-издательскнм комплексом Сибирского федерального университета 660041, Красноярск, пр. Свободный, 82а Тел. (391) 206-26-67; http://bik.sfu-kras.ru E-mail: publishing_house@sfu-kras.ru