Jump to content

Это манифест

Манифест QED представлял собой предложение создать компьютерную базу данных всех математических знаний, строго формализованную и со всеми доказательствами, проверяемыми автоматически . ( QED означает quod Erat DemonStrandum на латыни , что означает «что должно было быть продемонстрировано».)

Обзор [ править ]

Идея проекта возникла в 1993 году, в основном благодаря инициативе Роберта Бойера . Цели проекта, предварительно названного проектом QED или проектом QED , были изложены в манифесте QED, документе, впервые опубликованном в 1994 году при участии нескольких исследователей. [1] Явное авторство намеренно избегалось. Был создан специальный список рассылки, и состоялись две научные конференции по КЭД: первая в 1994 году в Аргоннских национальных лабораториях , а вторая в 1995 году в Варшаве, организованная группой Мицар . [2]

Похоже, что к 1996 году проект распался, так и не принес ничего, кроме обсуждений и планов. В статье 2007 года Фрик Видейк называет две причины провала проекта. [3] В порядке важности:

  • Очень немногие люди работают над формализацией математики. Полностью механизированная математика не имеет убедительного применения.
  • Формализованная математика еще не похожа на настоящую, традиционную математику. Частично это связано со сложностью математической записи, а частично с ограничениями существующих средств доказательства теорем и помощников по доказательству ; В статье обнаруживается, что основные претенденты, Mizar , HOL и Coq , имеют серьезные недостатки в своих способностях выражать математические выражения.

Тем не менее, проекты в стиле QED предлагаются регулярно. Математическая библиотека Мицар формализует большую часть студенческой математики и в 2007 году считалась крупнейшей такой библиотекой. [4] Подобные проекты включают базу данных доказательств Metamath и библиотеку mathlib, написанную на Lean . [5]

В 2014 году Двадцать лет Манифесту QED [6] мастер-класс был организован в рамках Венского лета логики .

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

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

  1. ^ Манифест QED в области автоматического вывода - CADE 12 , Springer-Verlag, Конспекты лекций по искусственному интеллекту, Vol. 814, стр. 238–251, 1994. HTML-версия.
  2. ^ Отчет II семинара QED
  3. ^ Фрик Видейк, Новый взгляд на манифест QED , 2007 г.
  4. ^ Файруз Камареддин, Мануэль Маарек, Кшиштоф Ретель и Дж. Б. Уэллс, Постепенная компьютеризация/формализация математических текстов в мицар
  5. ^ библиотека mathlib https://leanprover-community.github.io/mathlib-overview.html
  6. ^ Двадцать лет семинара по Манифесту QED.

Дальнейшее чтение [ править ]

  • Х. Барендрегт и Ф. Видейк, Проблемы компьютерной математики , Труды A Королевского общества, 363 вып. 1835, 2351–2375, 2005 г.
  • «Специальный выпуск о формальных доказательствах» . Уведомления Американского математического общества . Декабрь 2008 г. (выпуск в открытом доступе)
  • Ричард А. Де Милло , Ричард Дж. Липтон , Алан Дж. Перлис , Социальные процессы и доказательства теорем и программ , Сообщения ACM , Том 22, Выпуск 5 (май 1979 г.), Страницы: 271–280
  • Джон Харрисон, Формализованная математика , Технический отчет 36, Центр компьютерных наук Турку (TUCS)
  • Иттай Вайс, Манифест QED после двух десятилетий  Версия 2.0 , Journal of Software vol. 11, нет. 8, стр. 803-815, 2016.

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

Arc.Ask3.Ru: конец переведенного документа.
Arc.Ask3.Ru
Номер скриншота №: c15cf89d6df5b19adc6992c4882f8623__1699807920
URL1:https://arc.ask3.ru/arc/aa/c1/23/c15cf89d6df5b19adc6992c4882f8623.html
Заголовок, (Title) документа по адресу, URL1:
QED manifesto - Wikipedia
Данный printscreen веб страницы (снимок веб страницы, скриншот веб страницы), визуально-программная копия документа расположенного по адресу URL1 и сохраненная в файл, имеет: квалифицированную, усовершенствованную (подтверждены: метки времени, валидность сертификата), открепленную ЭЦП (приложена к данному файлу), что может быть использовано для подтверждения содержания и факта существования документа в этот момент времени. Права на данный скриншот принадлежат администрации Ask3.ru, использование в качестве доказательства только с письменного разрешения правообладателя скриншота. Администрация Ask3.ru не несет ответственности за информацию размещенную на данном скриншоте. Права на прочие зарегистрированные элементы любого права, изображенные на снимках принадлежат их владельцам. Качество перевода предоставляется как есть. Любые претензии, иски не могут быть предъявлены. Если вы не согласны с любым пунктом перечисленным выше, вы не можете использовать данный сайт и информация размещенную на нем (сайте/странице), немедленно покиньте данный сайт. В случае нарушения любого пункта перечисленного выше, штраф 55! (Пятьдесят пять факториал, Денежную единицу (имеющую самостоятельную стоимость) можете выбрать самостоятельно, выплаичвается товарами в течение 7 дней с момента нарушения.)