Система Мицар
 | |
Скриншот | |
| Парадигма | Декларативный |
|---|---|
| Разработано | Анджей Трибулец |
| Впервые появился | 1973 |
| Дисциплина набора текста | Слабый , статичный |
| Расширения имен файлов | .miz .voc |
| Веб-сайт | www.mizar.org |
| Под влиянием | |
| Автомат | |
| Под влиянием | |
| OMDoc , HOL Light и Coq mizar Режимы | |
Система Мицар состоит из формального языка для написания математических определений и доказательств, помощника по доказательству , способного механически проверять доказательства, написанные на этом языке, и библиотеки формализованной математики , которую можно использовать при доказательстве новых теорем. [1] Система поддерживается и развивается проектом Mizar Project, ранее находившимся под руководством его основателя Анджея Трибулца .
В 2009 году Математическая библиотека Мицара была крупнейшим из существующих структур строго формализованной математики. [2]
История [ править ]
Проект «Мицар» был начат примерно в 1973 году Анджеем Трибулцем как попытка реконструировать математический язык , чтобы его можно было проверить с помощью компьютера. [3] Его текущая цель, помимо постоянного развития системы Мицар, — совместное создание большой библиотеки формально проверенных доказательств, охватывающей большую часть ядра современной математики. Это соответствует влиятельному манифесту QED . [4]
В настоящее время проект разрабатывается и поддерживается исследовательскими группами Белостокского университета (Польша), Университета Альберты (Канада) и Университета Синсю (Япония). Хотя программа проверки корректур Mizar остается проприетарной, [5] Математическая библиотека Мицара — значительная часть формализованной математики, которую она проверила, — имеет лицензию с открытым исходным кодом. [6]
Статьи, связанные с системой Мицар, регулярно появляются в рецензируемых журналах академического сообщества по математической формализации. К ним относятся исследования по логике, грамматике и риторике , интеллектуальной компьютерной математике , интерактивному доказательству теорем , журналу автоматизированных рассуждений и журналу формализованного рассуждения .
Плотницкий язык [ править ]
Отличительной особенностью языка Мицар является его читабельность. Как это обычно бывает в математических текстах, он опирается на классическую логику и декларативный стиль . [7] Статьи Mizar написаны в обычном ASCII , но этот язык был разработан так, чтобы быть достаточно близким к математическому языку, чтобы большинство математиков могли читать и понимать статьи Mizar без специальной подготовки. [1] Тем не менее, этот язык обеспечивает повышенный уровень формальности, необходимый для автоматической проверки доказательств .
Чтобы доказательство было признано, все шаги должны быть обоснованы либо элементарными логическими аргументами, либо ссылкой на ранее проверенные доказательства. [8] Это приводит к более высокому уровню строгости и детализации, чем это принято в математических учебниках и публикациях. Таким образом, типичная статья Mizar примерно в четыре раза длиннее аналогичной статьи, написанной обычным стилем. [9]
Формализация является относительно трудоемкой, но не такой уж невыполнимой задачей. После того, как человек разбирается в системе, ему потребуется около недели полной занятости для формальной проверки страницы учебника. Это говорит о том, что ее преимущества теперь доступны прикладным областям, таким как теория вероятностей и экономика . [2]
Математическая библиотека Мицара [ править ]
Математическая библиотека Мицара (MML) включает все теоремы, на которые авторы могут ссылаться в новых статьях. После утверждения проверяющим корректуры они дополнительно оцениваются в процессе рецензирования на предмет надлежащего вклада и стиля. В случае принятия они публикуются в соответствующем Журнале формализованной математики. [10] и добавлен в MML.
Ширина [ править ]
По состоянию на июль 2012 года в MML включено 1150 статей, написанных 241 автором. [11] В совокупности они содержат более 10 000 формальных определений математических объектов и около 52 000 теорем, доказанных на этих объектах. Более 180 названных математических фактов получили пользу от формальной кодификации. [12] Некоторые примеры: теорема Хана-Банаха , лемма Кенига , теорема Брауэра о неподвижной точке , теорема Гёделя о полноте и теорема Жордана о кривой .
Такая широта охвата привела к тому, что некоторые [13] предложить Мицар как одно из ведущих приближений к утопии КЭД, заключающейся в кодировании всей базовой математики в форме, поддающейся компьютерной проверке.
Наличие [ править ]
Все статьи MML доступны в формате PDF в виде статей журнала формализованной математики . [10] Полный текст MML распространяется вместе с проверкой Mizar и его можно бесплатно загрузить с сайта Mizar. В текущем недавнем проекте [14] библиотека также была доступна в экспериментальной вики- форме. [15] это допускает изменения только тогда, когда они одобрены программой проверки Mizar. [16]
Веб-сайт запросов MML [11] реализует мощную поисковую систему по содержимому MML. Помимо прочего, он может извлекать все теоремы MML, доказанные для любого конкретного типа или оператора. [17] [18]
Логическая структура [ править ]
MML построен на аксиомах теории множеств Тарского-Гротендика . Несмотря на то, что семантически все объекты являются множествами , язык позволяет определять и использовать синтаксически слабые типы . Например, набор может быть объявлен как набор типа Nat только в том случае, если его внутренняя структура соответствует определенному списку требований. В свою очередь, этот список служит определением натуральных чисел , а совокупность всех множеств, соответствующих этому списку, обозначается как NAT . [19] Такая реализация типов призвана отразить то, как большинство математиков формально думают о символах. [20] и таким образом упростить кодификацию.
Mizar Proof Checker [ править ]
Дистрибутивы Mizar Proof Checker для всех основных операционных систем доступны для бесплатного скачивания на веб-сайте Mizar Project. Использование средства проверки доказательств бесплатно для всех некоммерческих целей. Он написан на Free Pascal , а исходный код доступен на GitHub. [21]
См. также [ править ]
Ссылки [ править ]
- ^ Jump up to: Перейти обратно: а б Наумович, Адам; Корнилович, Артур (2009). «Краткий обзор Мицара». В Бергхофере, Стефан; Нипков, Тобиас; Городской, христианский; Венцель, Макариус (ред.). Доказательство теорем в логике высшего порядка, 22-я Международная конференция, TPHOLs 2009, Мюнхен, Германия, 17–20 августа 2009 г. Труды . Конспекты лекций по информатике. Том. 5674. Спрингер. стр. 67–72. дои : 10.1007/978-3-642-03359-9_5 .
- ^ Jump up to: Перейти обратно: а б Видейк, Фрик (2009). «Формализация теоремы Эрроу» . Садхана . 34 (1): 193–220. дои : 10.1007/s12046-009-0005-1 . hdl : 2066/75428 .
- ^ Матушевский, Роман; Петр Рудницкий (2005). «Мицар: первые 30 лет» (PDF) . Механизированная математика и ее приложения . 4 .
- ^ Видейк, Фрик. «Мицар» . Проверено 24 июля 2018 г.
- ↑ Обсуждение в списке рассылки. Архивировано 9 октября 2011 г. на Wayback Machine со ссылкой на закрытие источников Mizar.
- ^ Объявление в списке рассылки, касающееся открытого исходного кода MML.
- ^ Геверс, Х. (2009). «Помощники доказательства: история, идеи и будущее» . Садхана . 34 (1): 3–25. дои : 10.1007/s12046-009-0001-5 . hdl : 2066/75958 .
- ^ Видейк, Фрик (2008). «Формальное доказательство. Начало работы» (PDF) . Уведомления АМС . 55 (11): 1408–1414.
- ^ Видейк, Фрик. «Фактор де Брейна » . Проверено 24 июля 2018 г.
- ^ Jump up to: Перейти обратно: а б Журнал формализованной математики
- ^ Jump up to: Перейти обратно: а б Поисковая система MML Query
- ^ «Список названных теорем в MML» . Проверено 22 июля 2012 г.
- ^ Видейк, Фрик (2007). «Возвращение к Манифесту QED» (PDF) . От понимания к доказательству: Фестиваль в честь Анджея Трибулца . Исследования по логике, грамматике и риторике . 10 (23).
- ^ Домашняя страница проекта MathWiki
- ^ MML в вики-форме
- ^ Алама, Джесси; Бринк, Каспер; Мамане, Лайонел; Урбан, Йозеф (2011). «Большие формальные вики: проблемы и решения». В Давенпорте, Джеймс Х.; Фармер, Уильям М.; Урбан, Йозеф; Рабе, Флориан (ред.). Интеллектуальная компьютерная математика – 18-й симпозиум Calculemus 2011 и 10-я Международная конференция MKM 2011, Бертиноро, Италия, 18–23 июля 2011 г. Труды . Конспекты лекций по информатике. Том. 6824. Спрингер. стр. 133–148. arXiv : 1107.3209 . дои : 10.1007/978-3-642-22673-1_10 .
- ^ Пример запроса MML , выдающего все теоремы, доказанные об операторе экспоненты , по количеству раз, когда они цитируются в последующих теоремах.
- ^ Еще один пример запроса MML , дающий все теоремы, доказанные для сигма-полей .
- ^ Грабовский, Адам; Артур Корнилович; Адам Наумович (2010). «Мицар в двух словах» . Журнал формализованного рассуждения . 3 (2): 152–245.
- ^ Тейлор, Пол (1999). Практические основы математики . Издательство Кембриджского университета . ISBN 9780521631075 . Архивировано из оригинала 23 июня 2015 г. Проверено 24 июля 2012 г.
- ^ Исходный код Мицара