Аннотация:
Доклад будет посвящен обзору логики свидетельств, которая была открыта в результате поиска нового прочтения BHK семантики (Artemov, 1995). Логика свидетельств позволяет представлять доказательства как эксплицитные объекты добавлением в язык формул вида «$s:F$», которые интерпретируются как «$s$ свидетельствует в пользу $F$». Впервые идея рассматривать доказательства как имеющие структуру абстрактные объекты с возможностью применения к ним операций была предложена К. Гёделем. Однако его работа долго оставалась неопубликованной, пока логика свидетельств в её современном виде не была переоткрыта С.Н. Артёмовым. В докладе будут рассмотрены различные системы логики свидетельств и их отношения с модальными логиками.
