Система Mizar

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

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

Примечания

  1. ↑ Ламберов Лев Дмитриевич. ПРАКТИКА КОМПЬЮТЕРНЫХ ДОКАЗАТЕЛЬСТВ И ЧЕЛОВЕЧЕСКОЕ ПОНИМАНИЕ: ЭПИСТЕМОЛОГИЧЕСКАЯ ПРОБЛЕМАТИКА // Вестник Пермского университета. Философия. Психология. Социология. — 2021. — № 1.
  2. ↑ Матиясевич Юрий Владимирович. Математическое доказательство: вчера, сегодня, завтра // Компьютерные инструменты в образовании. — 2012. — № 6.
  3. ↑ Wiedijk Freek. Formalizing Arrow’s theorem (англ.) // Sadhana. — 2009. — February (vol. 34, no. 1). — P. 193—220. — ISSN 0256-2499. — doi:10.1007/s12046-009-0005-1.
Эта статья взята у (из) Wikipedia. Текст лицензируется по Creative Commons - Attribution - Sharealike. К медиа файлам могут применятся дополнительные условия.