Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску
Для звездной системы см Мицар (звезда) .
Мицар
Mizar system logo.gif
Скриншот
Mizar MathWiki screenshot.png
Скриншот Mizar MathWiki
ПарадигмаДекларативная
РазработаноАнджей Трыбулец
Впервые появился1973
Печатная дисциплинаСлабый , статичный
Расширения имени файла.miz .voc
Интернет сайтwww.mizar.org
Под влиянием
Автомат
Под влиянием
Режимы OMDoc , HOL Light и Coq mizar

Система Mizar состоит из формального языка для написания математических определений и доказательств, помощника по доказательству , который может механически проверять доказательства, написанные на этом языке, и библиотеки формализованной математики , которая может использоваться при доказательстве новых теорем. [1] Система поддерживается и развивается проектом Mizar Project, который ранее находился под руководством его основателя Анджея Трюбулеца .

В 2009 году Математическая библиотека Мицара была крупнейшим из когда-либо существовавших целостных систем строго формализованной математики. [2]

История [ править ]

Проект Mizar был начат примерно в 1973 году Анджеем Трюбулецом как попытка восстановить математический язык, чтобы его можно было проверить на компьютере. [3] Его текущая цель, помимо постоянного развития системы Мицар, - совместное создание большой библиотеки формально проверенных доказательств, охватывающих большую часть ядра современной математики. Это соответствует влиятельному манифесту QED . [4]

В настоящее время проект разрабатывается и поддерживается исследовательскими группами Белостокского университета , Польша, Университета Альберты , Канада, и Университета Синшу , Япония. В то время как средство проверки доказательств Mizar остается собственностью [5], математическая библиотека Mizar - значительный объем формализованной математики, которую она проверила - является лицензированной с открытым исходным кодом. [6]

Статьи, относящиеся к системе Mizar, регулярно появляются в рецензируемых журналах академического сообщества математической формализации. К ним относятся исследования по логике, грамматике и риторике , интеллектуальной компьютерной математике , интерактивному доказательству теорем , журналу автоматизированных рассуждений и журналу формализованных рассуждений .

Язык Mizar [ править ]

Отличительной особенностью языка Mizar является его читабельность. Как это принято в математическом тексте, он основан на классической логике и декларативном стиле . [7] Статьи Mizar написаны в обычном ASCII , но язык был разработан так, чтобы быть достаточно близким к математическому жаргоном, чтобы большинство математиков могли читать и понимать статьи Mizar без специальной подготовки. [1] Тем не менее, язык обеспечивает повышенный уровень формальности, необходимый для автоматизированной проверки .

Чтобы доказательство было принято, все шаги должны быть обоснованы либо элементарными логическими аргументами, либо цитированием ранее проверенных доказательств. [8] Это приводит к более высокому уровню строгости и детализации, чем это принято в математических учебниках и публикациях. Таким образом, типичная статья Mizar примерно в четыре раза длиннее аналогичной статьи, написанной обычным стилем. [9]

Формализация относительно трудоемка, но не безнадежно трудна. После того, как кто-то познакомится с системой, потребуется около недели полной занятости, чтобы формально проверить страницу учебника. Это говорит о том, что его преимущества теперь доступны в таких прикладных областях, как теория вероятностей и экономика . [2]

Математическая библиотека Mizar [ править ]

Математическая библиотека Mizar (MML) включает все теоремы, на которые авторы могут ссылаться в недавно написанных статьях. После утверждения проверкой корректуры они проходят дальнейшую оценку в процессе экспертной оценки на предмет соответствующего вклада и стиля. В случае принятия они публикуются в соответствующем журнале «Формализованная математика» [10] и добавляются в MML.

Ширина [ править ]

По состоянию на июль 2012 года MML включал 1150 статей, написанных 241 автором. [11] В совокупности они содержат более 10 000 формальных определений математических объектов и около 52 000 теорем, доказанных на этих объектах. Более 180 названных математических фактов получили такую ​​пользу от формальной кодификации. [12] Некоторые примеры теоремы Хана-Банаха , лемма Кенига , Брауэра о неподвижной точке теорема , теорема Гёделя о полноте и теорема жордановой кривой .

Такая широта охвата привела некоторых [13] к предложению Мицара в качестве одного из ведущих приближений к утопии QED о кодировании всей основной математики в проверяемой компьютером форме.

Доступность [ править ]

Все статьи MML доступны в формате PDF в виде статей Journal of Formalized Mathematics . [10] Полный текст MML распространяется с программой проверки Mizar и может быть бесплатно загружен с веб-сайта Mizar. В текущем недавнем проекте [14] библиотека также была сделана доступной в экспериментальной форме вики [15], которая допускает редактирование только тогда, когда они одобрены программой проверки Mizar. [16]

На веб-сайте MML Query [11] реализована мощная поисковая машина по содержимому MML. Помимо других возможностей, он может извлекать все доказанные теоремы MML о любом конкретном типе или операторе. [17] [18]

Логическая структура [ править ]

MML построен на аксиомах теории множеств Тарского – Гротендика . Несмотря на то, что семантически все объекты являются наборами , язык позволяет определять и использовать синтаксически слабые типы . Например, набор может быть объявлен как имеющий тип Nat, только если его внутренняя структура соответствует определенному списку требований. В свою очередь, этот список служит определением натуральных чисел, а набор всех наборов, которые соответствуют этому списку, обозначается как NAT . [19] Эта реализация типов стремится отразить то, как большинство математиков формально думают о символах [20], и таким образом упростить кодификацию.

Mizar Proof Checker [ править ]

Распространения Mizar Proof Checker для всех основных операционных систем бесплатно доступны для загрузки на веб-сайте Mizar Project. Программа проверки правописания бесплатна для всех некоммерческих целей. Он написан на Free Pascal, а исходный код доступен всем членам Ассоциации пользователей Mizar. [21]

См. Также [ править ]

  • Изар (Изабель)
  • Метамат

Ссылки [ править ]

  1. ^ a b Наумович, Адам; Артур Корнилович (2009). «Краткий обзор Мицара». Доказательство теорем в логиках высокого порядка . Конспект лекций по информатике. 5674 : 67–72. DOI : 10.1007 / 978-3-642-03359-9_5 . ISBN 978-3-642-03358-2.
  2. ^ a b Wiedijk, Freek (2009). «Формализация теоремы Эрроу» . Садхана . 34 (1): 193–220. DOI : 10.1007 / s12046-009-0005-1 . ЛВП : 2066/75428 .
  3. ^ Матушевский, Роман; Петр Рудницкий (2005). «Мицар: первые 30 лет» (PDF) . Механизированная математика и ее приложения . 4 .
  4. ^ Wiedijk, Фрик. «Мицар» . Проверено 24 июля 2018 года .
  5. ^ Список рассылки обсуждение архивации 2011-10-09 в Wayback Machine со ссылкой на близкого делокализация Мицар.
  6. ^ Объявление списка рассылки, относящееся к открытому исходному коду MML.
  7. ^ Geuvers, H. (2009). «Доказательства помощников: история, идеи и будущее» . Садхана . 34 (1): 3–25. DOI : 10.1007 / s12046-009-0001-5 .
  8. ^ Wiedijk, Фрик (2008). «Формальное доказательство - Начало работы» (PDF) . Уведомления AMS . 55 (11): 1408–1414.
  9. ^ Wiedijk, Фрик. «Фактор де Брейна » » . Проверено 24 июля 2018 года .
  10. ^ a b Журнал формализованной математики
  11. ^ a b Поисковая машина MML Query
  12. ^ «Список названных теорем в MML» . Проверено 22 июля 2012 года .
  13. ^ Wiedijk, Фрик (2007). «Новый взгляд на манифест QED» . От понимания к доказательству: Festschrift в честь Анджея Трибулеца . Исследования по логике, грамматике и риторике . 10 (23).
  14. ^ Домашняя страница проекта MathWiki
  15. ^ MML в форме вики
  16. ^ Алама, Джесси; Каспер Бринк; Лайонел Мамане; Йозеф Урбан (2011). «Большие формальные вики: проблемы и решения». Интеллектуальная компьютерная математика . Конспект лекций по информатике. 6824 : 133–148. arXiv : 1107,3212 . DOI : 10.1007 / 978-3-642-22673-1_10 . ISBN 978-3-642-22672-4.
  17. ^ Пример запроса MML , дающий все теоремы, доказанные дляоператора экспоненты , по количеству их цитирований в последующих теоремах.
  18. ^ Другой пример запроса MML , дающий все теоремы, доказанные для сигма-полей .
  19. ^ Грабовски, Адам; Артур Корнилович; Адам Наумович (2010). «Мицар в двух словах» . Журнал формализованных рассуждений . 3 (2): 152–245.
  20. ^ Тейлор, Пол (1999). Практические основы математики . Издательство Кембриджского университета . ISBN 9780521631075. Архивировано из оригинала на 2015-06-23 . Проверено 24 июля 2012 .
  21. ^ Сайт Ассоциации пользователей Mizar

Внешние ссылки [ править ]

  • Официальный веб-сайт