Система Mizar - Mizar system
Парадигма | Декларативная |
---|---|
Разработано | Анджей Трыбулец |
Впервые появился | 1973 |
Печатная дисциплина | Слабый , статичный |
Расширения имени файла | .miz .voc |
Веб-сайт | www.mizar.org |
Под влиянием | |
Автомат | |
Под влиянием | |
Режимы OMDoc , HOL Light и Coq mizar |
Система Mizar состоит из формального языка для написания математических определений и доказательств, помощника по доказательству , который может механически проверять доказательства, написанные на этом языке, и библиотеки формализованной математики , которая может использоваться при доказательстве новых теорем. Система поддерживается и развивается проектом Mizar Project, ранее возглавлявшимся его основателем Анджеем Трибулцем .
В 2009 году Математическая библиотека Мицара была крупнейшим из когда-либо существовавших целостных систем строго формализованной математики.
История
Проект Mizar был начат примерно в 1973 году Анджеем Трюбулецом как попытка восстановить математический язык, чтобы его можно было проверить с помощью компьютера. Его текущая цель, помимо постоянного развития системы Mizar, - совместное создание большой библиотеки формально проверенных доказательств, охватывающих большую часть ядра современной математики. Это соответствует влиятельному манифесту QED .
В настоящее время проект разрабатывается и поддерживается исследовательскими группами Белостокского университета , Польша, Университета Альберты , Канада, и Университета Синшу , Япония. В то время как средство проверки доказательств Mizar остается частной собственностью, математическая библиотека Mizar - значительный объем формализованной математики, которую она проверяла - имеет открытый исходный код по лицензии.
Статьи, относящиеся к системе Mizar, регулярно появляются в рецензируемых журналах академического сообщества математической формализации. К ним относятся исследования в области логики, грамматики и риторики , интеллектуальной компьютерной математики , интерактивного доказательства теорем , журнала автоматизированного мышления и журнала формализованного мышления .
Мицарский язык
Отличительной особенностью языка Mizar является его читабельность. Как это принято в математическом тексте, он основан на классической логике и декларативном стиле . Статьи Mizar написаны в обычном ASCII , но этот язык был разработан так, чтобы быть достаточно близким к математическому жаргоном, чтобы большинство математиков могли читать и понимать статьи Mizar без специальной подготовки. Тем не менее, язык обеспечивает повышенный уровень формальности, необходимый для автоматизированной проверки .
Чтобы доказательство было принято, все шаги должны быть обоснованы либо элементарными логическими аргументами, либо цитированием ранее проверенных доказательств. Это приводит к более высокому уровню строгости и детализации, чем это принято в учебниках и публикациях по математике. Таким образом, типичная статья Mizar примерно в четыре раза длиннее аналогичной статьи, написанной обычным стилем.
Формализация относительно трудоемка, но не безнадежно трудна. После того, как кто-то познакомится с системой, потребуется около недели полной занятости, чтобы формально проверить страницу учебника. Это говорит о том, что его преимущества теперь доступны в таких прикладных областях, как теория вероятностей и экономика .
Математическая библиотека Mizar
Математическая библиотека Mizar (MML) включает все теоремы, на которые авторы могут ссылаться в недавно написанных статьях. После утверждения проверкой корректуры они проходят дальнейшую оценку в процессе экспертной оценки на предмет соответствующего вклада и стиля. В случае принятия они публикуются в соответствующем журнале формализованной математики и добавляются в MML.
Ширина
По состоянию на июль 2012 года MML включал 1150 статей, написанных 241 автором. В совокупности они содержат более 10 000 формальных определений математических объектов и около 52 000 теорем, доказанных на этих объектах. Более 180 названных математических фактов получили такую пользу от формальной кодификации. Некоторые примеры теоремы Хана-Банаха , лемма Кенига , Брауэра о неподвижной точке теорема , теорема Гёделя о полноте и теорема жордановой кривой .
Такая широта охвата привела к тому, что некоторые предложили Мицара как одно из ведущих приближений к утопии QED, заключающейся в кодировании всей основной математики в проверяемой компьютером форме.
Доступность
Все статьи MML доступны в формате PDF как статьи Journal of Formalized Mathematics . Полный текст MML распространяется с программой проверки Mizar и может быть бесплатно загружен с веб-сайта Mizar. В текущем недавнем проекте библиотека также стала доступной в экспериментальной форме вики, которая допускает редактирование только тогда, когда они одобрены программой проверки Mizar.
На веб-сайте MML Query реализована мощная поисковая машина по содержимому MML. Помимо других возможностей, он может извлекать все доказанные теоремы MML о любом конкретном типе или операторе.
Логическая структура
MML построен на аксиомах теории множеств Тарского – Гротендика . Несмотря на то, что семантически все объекты являются наборами , язык позволяет определять и использовать синтаксически слабые типы . Например, набор может быть объявлен как имеющий тип Nat, только если его внутренняя структура соответствует определенному списку требований. В свою очередь, этот список служит определением натуральных чисел, а набор всех наборов, которые соответствуют этому списку, обозначается как NAT . Эта реализация типов стремится отразить то, как большинство математиков формально думает о символах, и таким образом упростить кодификацию.
Mizar Proof Checker
Распространения Mizar Proof Checker для всех основных операционных систем бесплатно доступны для загрузки на веб-сайте Mizar Project. Программа проверки правописания бесплатна для всех некоммерческих целей. Он написан на Free Pascal, а исходный код доступен всем членам Ассоциации пользователей Mizar.