Журнал СФУ. Математика и физика / Общий метаязык для формальных доказательств

Полный текст (.pdf)
Номер
Журнал СФУ. Математика и физика. Prepublication
Авторы
Мишко, Николай А.
Контактная информация
Мишко, Николай А. : Сибирский федеральный университет (Красноярск, Российская Федерация)
Ключевые слова
formal system; big-step semantics; proof verification; формальная система; операционная семантика; верификация доказательств
Аннотация

В работе представлена операционная семантика языка, достаточного мощного для выражения произвольных формальных систем с вычислимыми правилами вывода и метатеорем об этих системах, при этом достаточно простого для реализации и теоретического анализа, а также потенциально пригодного для самоверификации

Страницы
335–346
EDN
KHDDDY
Статья в архиве электронных ресурсов СФУ
https://elib.sfu-kras.ru/handle/2311/158233