- Номер
- Журнал СФУ. Математика и физика. Prepublication
- Авторы
- Мишко, Николай А.
- Контактная информация
- Мишко, Николай А. : Сибирский федеральный университет (Красноярск, Российская Федерация)
- Ключевые слова
- formal system; big-step semantics; proof verification; формальная система; операционная семантика; верификация доказательств
- Аннотация
В работе представлена операционная семантика языка, достаточного мощного для выражения произвольных формальных систем с вычислимыми правилами вывода и метатеорем об этих системах, при этом достаточно простого для реализации и теоретического анализа, а также потенциально пригодного для самоверификации
- Страницы
- 335–346
- EDN
- KHDDDY
- Статья в архиве электронных ресурсов СФУ
- https://elib.sfu-kras.ru/handle/2311/158233
Журнал СФУ. Математика и физика / Общий метаязык для формальных доказательств
Полный текст (.pdf)