Манифест QED - QED manifesto
В Манифест QED было предложение о компьютерной базе данных всех математический знания, строго формализованные и со всеми доказательствами проверяется автоматически. (Q.E.D. средства quod erat manifestrandum в латинский, что означает «что должно было быть продемонстрировано»).
Обзор
Идея проекта возникла в 1993 году, в основном под влиянием Роберт Бойер. Цели проекта, названные предварительно QED проект или же проект QED, были изложены в манифесте QED, документе, впервые опубликованном в 1994 году при участии нескольких исследователей.[1] Явного авторства сознательно избегали. Был создан специальный список рассылки и проведены две научные конференции по QED, первая в 1994 г. Аргоннские национальные лаборатории и второй в 1995 г. Варшава организованный Мицар группа.[2]
Похоже, что к 1996 году проект был распущен, так как он никогда не производил ничего, кроме обсуждений и планов. В статье 2007 года Фрик Видийк определяет две причины провала проекта.[3] В порядке важности:
- Мало кто работает над формализацией математики. Для полностью механизированной математики нет убедительного приложения.
- Формализованная математика еще не похожа на настоящую традиционную математику. Отчасти это связано со сложностью математической записи, а отчасти с ограничениями существующих средства доказательства теорем и помощники доказательства; в документе говорится, что основные претенденты, Мицар, HOL, и Coq имеют серьезные недостатки в своих способностях выражать математические науки.
Тем не менее, проекты в стиле QED регулярно предлагаются, и Мицар Библиотека успешно формализовала большую часть математики бакалавриата. По состоянию на 2007 г.[Обновить] это самая большая такая библиотека.[4] Еще один такой проект - Метамат база данных доказательств.
В 2014 году Двадцать лет Манифесту QED[5] семинар был организован в рамках Венское лето логики.
Смотрите также
- Формализм (математика)
- Управление математическими знаниями
- POPLmark, более скромный проект в теория языков программирования
Рекомендации
- ^ Манифест QED в Автоматическое удержание - CADE 12, Springer-Verlag, Lecture Notes in Artificial Intelligence, Vol. 814, стр. 238-251, 1994. HTML версия
- ^ Отчет QED Workshop II
- ^ Фрик Видейк, Новый взгляд на манифест QED, 2007
- ^ Файруз Камареддин, Мануэль Маарек, Кшиштоф Ретель и Дж. Б. Уэллс, Постепенная компьютеризация / формализация математических текстов в Mizar
- ^ Двадцать лет мастерской QED Manifesto
дальнейшее чтение
- Х. Барендрегт И Ф. Видейк, Проблема компьютерной математики, Транзакции A Королевского общества 363 No. 1835 г., 2351–2375, 2005 г.
- «Специальный выпуск о формальном доказательстве». Уведомления Американского математического общества. Декабрь 2008 г. (проблема с открытым доступом)
- Ричард А. Де Милло, Ричард Дж. Липтон, Алан Дж. Перлис, Социальные процессы и доказательства теорем и программ, Коммуникации ACM, Том 22, выпуск 5 (май 1979 г.), Страницы: 271 - 280
- Джон Харрисон, Формализованная математика, Технический отчет 36, Центр компьютерных наук Турку (TUCS)
внешняя ссылка
- Фрик Видейк, Формализация 100 теорем Страница, отслеживающая прогресс в формализации 100 общих теорем.
- Фрик Видейк, Семнадцать испытателей мира, доказательство иррациональность квадратного корня из двух в семнадцати различных помощниках доказательства.
- Формализованная математика журнал, в котором представлены доказательства Мицара.
- Архив формальных доказательств аналогичное (рецензируемое) хранилище доказательств в Isabelle / HOL.
- [1] Хранилище доказательств в Coq.
- UniMath "Библиотека Coq призвана формализовать значительную часть математики с помощью однозначный точка зрения"