Тип публикации: диссертация
Год издания: 2018
Ключевые слова: ВРЕМЕННЫЕ МНОГОАГЕНТНЫЕ ЛОГИКИ, многомодальные логики, унификация, пассивные правила вывода, проективные формулы
Аннотация: Объект исследования - теория унификации многомодальных логик знания и времени. Цель исследования - решение унификационных проблем в ряде временных и многоагентных логик. Задачи исследования - поиск критериев неунифицируемости логик LTK, LFPK и всех полных по Крипке с выразимой универсальной модальностью; доказательство проективной Показать полностьюунификации в LFPK, ULITL, поиск алгоритмов построения наиболее общего унификатора (mgu). Используются реляционная семантика Крипке, отрицание унифицируемости, проективные и граунд унификаторы, методы теоретико-модельной и алгебраической семантики. Найдены критерии неунифицируемости и базисы пассивных правил логик LTK и LFPK, полных по Крипке логик с выразимой универсальной модальностью. Доказана проективная унификация для ULITL, LFPK и ее обогащений операторами Until+/-, Next/Previous, предложены алгоритмы построения mgu. Доказана возможность эффективно устанавливать унифицируемость в ULITL. Все результаты получены впервые, носят теоретический характер и применимы в исследованиях нестандартных логик, теории моделей, информатики и при составлении программ курсов по математической логике.