Система Mizar

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

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

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

Содержание

  • 1 История
  • 2 Язык Mizar
  • 3 Математическая библиотека Mizar
    • 3.1 Ширина
    • 3.2 Доступность
    • 3.3 Логическая структура
  • 4 Mizar Proof Checker
  • 5 См. Также
  • 6 Ссылки
  • 7 Внешние ссылки

История

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

В настоящее время проект разрабатывается и поддерживается исследовательскими группами в Белостокском университете, Польша, Университете Альберты, Канада, и Университет Синсю, Япония. В то время как средство проверки доказательств 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. В текущем недавнем проекте библиотека была также доступна в экспериментальной форме wiki, которая допускает редактирование только тогда, когда они одобрены программой проверки Mizar.

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

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

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

Mizar Proof Checker

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

См. Также

Ссылки

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

Последняя правка сделана 2021-05-30 03:55:16
Содержание доступно по лицензии CC BY-SA 3.0 (если не указано иное).
Обратная связь: support@alphapedia.ru
Соглашение
О проекте