RUS  ENG
Полная версия
ЖУРНАЛЫ // Сибирский журнал чистой и прикладной математики // Архив

Вестн. НГУ. Сер. матем., мех., информ., 2012, том 12, выпуск 2, страницы 13–25 (Mi vngu115)

Язык smm – упрощенный metamath

Д. Ю. Власовab

a Новосибирский государственный университет, ул. Пирогова, 2, Новосибирск, 630090, Россия
b Институт математики им. С. Л. Соболева СО РАН, пр. Акад. Коптюга, 4, Новосибирск, 630090, Россия

Аннотация: Описывается синтаксис и семантика языка smm – компьютерного языка формальной математики, предназначенного для представления современной математики на формальном уровне и надежной проверки, который является упрощенной версией языка формальной математики metamath.

Ключевые слова: формальная математика, представление математического знания, автоматическая проверка доказательств.

УДК: 510.23+811.93

Поступила в редакцию: 26.03.2010



© МИАН, 2024