|
Вестник НГУ. Серия: Математика, механика, информатика, 2011, том 11, выпуск 2, страницы 27–50
(Mi vngu77)
|
|
|
|
Эта публикация цитируется в 1 научной статье (всего в 1 статье)
Язык формальной математики Russell
Д. Ю. Власовab a Институт математики им. С. Л. Соболева СО РАН, пр. Акад. Коптюга, 4, Новосибирск, 630090, Россия
b Новосибирский государственный университет, ул. Пирогова, 2, Новосибирск, 630090, Россия
Аннотация:
Russell — это компьютерный язык формальной математики, предназначенный для представления современной математики на формальном уровне, надежной проверки доказательств и автоматизации рутинных (технических) доказательств при доказательстве теорем. Russell является языком высокого уровня над языком smm, который, в свою очередь, является упрощенной версией языка формальной математики metamath. Ключевыми особенностями Russell являются: сохранение уровня универсальности и надежности языка metamath, возможность читать и реадктировать тексты формальных доказательств без привлечения специальных программ, чего лишен язык metamath. Язык Russell может считаться кандидатом на полную реализацию QED манифеста.
Ключевые слова:
формальная математика, автоматический вывод, представление математического знания, автоматическая проверка доказательств.
Поступила в редакцию: 26.03.2010
Образец цитирования:
Д. Ю. Власов, “Язык формальной математики Russell”, Вестн. НГУ. Сер. матем., мех., информ., 11:2 (2011), 27–50
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/vngu77 https://www.mathnet.ru/rus/vngu/v11/i2/p27
|
Статистика просмотров: |
Страница аннотации: | 290 | PDF полного текста: | 154 | Список литературы: | 53 | Первая страница: | 1 |
|