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

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





Для просмотра файлов Вам могут потребоваться






Симпозиум по логике и вычислимости «Logic and Computation Day»
7 июня 2013 г. 12:15, г. Москва, МИАН
 


Circular proofs for provability logic

D. S. Shamkanov

Steklov Mathematical Institute of the Russian Academy of Sciences

Количество просмотров:
Эта страница:33

Аннотация: We present a circular proof system for the Gödel-Löb provability logic GL. In contrast to the ordinary proofs, a circular proof can be formed from an ordinary derivation tree by identifying each open assumption with an identical interior sequent. We prove that the circular proof-system is sound and complete with respect to the standard sequent-style formulation of GL, that it is contraction-free and cut-free, and that its logical rules are invertible. As an application, we give a syntactic proof of Lyndon interpolation for GL.

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

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