Видеотека
RUS  ENG    ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB  
Видеотека
Архив
Популярное видео

Поиск
RSS
Новые поступления






Workshop on Proof Theory, Modal Logic and Reflection Principles
18 октября 2017 г. 11:10–11:45, Москва, Математический институт им. В.А. Стеклова РАН
 


Instantial Neighborhood Logic — tableau, sequent calculus, and interpolation

J. Yu
Видеозаписи:
MP4 1,030.3 Mb
MP4 282.4 Mb

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

J. Yu


Видео не загружается в Ваш браузер:
  1. Проверьте с Вашим администратором, что из Вашей сети разрешены исходящие соединения на порт 8080
  2. Сообщите администратору портала о данной ошибке

Аннотация: Instantial Neighborhood Logic (INL) employs a two-sorted operator $\square$. In INL, formula $\square(\alpha_1,…,\alpha_j;\alpha_0)$ means, the current point has a neighborhood in which $\alpha_0$ universally holds, and none of $\alpha_1,…,\alpha_j$ universally fails. In my talk last year at Tbilisi State University, a tableau system for INL was presented. To continue, in this talk we convert that tableau system to a hyper-sequent calculus, and then to a (normal) sequent calculus G3inl. Based on a splitting version of G3inl, we will explain how Lyndon interpolation theorem of INL is constructively established.

Язык доклада: английский

ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru
 
Обратная связь:
 Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2021