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

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




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


Неразрешимость логики решёток Клини с делениями

С. Л. Кузнецов
Видеозаписи:
MP4 2,228.7 Mb
MP4 1,011.9 Mb

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

С. Л. Кузнецов



Аннотация: Решёткой Клини называется решётка с дополнительными операциями умножения (задаёт структуру моноида) и итерации Клини, $a^{\star}$, определяемой как наименьшая неподвижная точка операции $x \to 1 \lor ax$. Если в такой решётке определены операции левого и правого деления, естественным образом согласованные с операцией умножения и частичным порядком, задаваемым решёточной структурой, получается решётка Клини с делением [Пратт 1991, Козен 1994]. Относительно интерпретации на решётках с делением (без итерации Клини) корректно и полно исчисление Ламбека с аддитивными конъюнкцией и дизъюнкцией. Добавление итерации Клини с соответствующими аксиомами даёт логику решёток Клини с делениями (в иностранной литературе также используется термин "action logic"). Для болеесильной системы, полной относительно более узкого класса $\star$-непрерывных алгебр Клини (где $a^\star$ определяется как $\sup \{ a^n | n = 0,1,2,3... \}$), известно [Бушковский 2007], что эта логика неразрешима, точнее - $П_1^0$-полна. Вопрос о сложности для логики всех решёток Клини с делением в работах Пратта, Козена и Бушковского оставлен как открытая проблема. Будет рассказано её решение: доказательство неразрешимости, а именно $\Sigma_1^0$-полноты.
 
  Обратная связь:
 Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2024