stringtranslate.com

Система Мицар

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

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

История

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

В настоящее время проект разрабатывается и поддерживается исследовательскими группами Белостокского университета (Польша), Университета Альберты (Канада) и Университета Синсю (Япония). Хотя программа проверки доказательств Mizar остается частной собственностью, [5] Математическая библиотека Mizar — значительная часть формализованной математики, которую она проверяла — имеет лицензию с открытым исходным кодом. [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 Query [11] реализует мощную поисковую систему по содержимому MML. Помимо прочего, он может извлекать все теоремы MML, доказанные для любого конкретного типа или оператора. [17] [18]

Логическая структура

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

Мицар Proof Checker

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

Смотрите также

Рекомендации

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

Внешние ссылки