Семинары
RUS  ENG    ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB  
Календарь
Поиск
Регистрация семинара

RSS
Ближайшие семинары




Семинары отдела математической логики "Теория доказательств" и "Logic Online Seminar"
25 сентября 2023 г. 18:30, г. Москва, МИАН (ул. Губкина, 8), ауд. 313 + Zoom
 


О проблеме унификации для полимодальной логики доказуемости

Н. Лукашов

Национальный исследовательский университет "Высшая школа экономики", г. Москва
Видеозаписи:
MP4 3,933.7 Mb

Количество просмотров:
Эта страница:119
Видеофайлы:30



Аннотация: Проблема унификации для данной модальной логики тесно связана с проблемой характеризации ее допустимых правил вывода. Хорошо известно, что логика GL имеет конечный унификационный тип (С. Гилярди), проблема допустимости правил вывода в GL алгоритмически разрешима (В.В. Рыбаков) и ее допустимые правила вывода имеют естественную аксиоматизацию (Э. Ержабек). Для полимодальной логики доказуемости GLP, в том числе и для языка всего с двумя модальностями, эти вопросы пока остаются открытыми.
Мы докажем, что финитно аппроксимируемый фрагмент J полимодальной логики доказуемости GLP (в языке с конечным числом модальностей) имеет конечный унификационный тип, то есть множество унификаторов любой формулы порождается конечным числом максимальных. В то же время унификационный тип самой логики GLP уже для языка с двумя модальностями - нулевой, то есть существует унифицируемая формула, множество унификаторов которой не имеет максимального.
Совместная работа с Л.Д. Беклемишевым.
 
  Обратная связь:
 Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2024