Нупрл
Nuprl — это система разработки доказательств, обеспечивающая компьютерный анализ и доказательства формальных математических утверждений, а также инструменты для проверки и оптимизации программного обеспечения. Первоначально разработанная в 1980-х годах Робертом Ли Констеблем и другими, система в настоящее время поддерживается проектом PRL в Корнелльском университете . Поддерживаемая в настоящее время версия Nuprl 5 также известна как FDL (формальная цифровая библиотека). Nuprl функционирует как автоматизированная система доказательства теорем , а также может использоваться для оказания помощи в доказательстве .
Дизайн [ править ]
Nuprl использует систему типов , основанную на Мартина-Лёфа интуиционистской теории типов , для моделирования математических утверждений в цифровой библиотеке . Математические теории можно создавать и анализировать с помощью различных редакторов, включая графический интерфейс пользователя , веб-редактор и режим Emacs . С утверждениями в библиотеке могут работать различные оценщики и механизмы вывода. Переводчики также позволяют манипулировать операторами с помощью программ Java и OCaml . [1] Вся система управляется с помощью варианта ML .
Архитектура Nuprl 5 описывается как «распределенная открытая архитектура ». [1] и предназначен в первую очередь для использования в качестве веб-сервиса, а не как отдельное программное обеспечение. Те, кто заинтересован в использовании веб-сервиса или переносе теорий из более старых версий Nuprl, могут связаться по адресу электронной почты, указанному на веб-странице системы Nuprl. [2]
История [ править ]
Nuprl впервые был выпущен в 1984 году и впервые был подробно описан в книге Implementing Mathematics with the Nuprl Proof Development System , [3] опубликован в 1986 году. Nuprl 2 была первой версией Unix . Nuprl 3 предоставил машинное доказательство математических задач, связанных с парадоксом Жирара и леммой Хигмана . Nuprl 4, первая версия, разработанная для Всемирной паутины , использовалась для проверки протоколов согласованности кэша и других компьютерных систем. [4]
Текущая архитектура системы, реализованная в Nuprl 5, была впервые предложена в документе конференции 2000 года . Справочное руководство для Nuprl 5 было опубликовано в 2002 году. [5] Nuprl был предметом многих публикаций по информатике .
Преемники [ править ]
Системы JonPRL и RedPRL также основаны на теории вычислительных типов. [6] RedPRL явно «вдохновлен Nuprl». [7]
Ссылки [ править ]
- ↑ Перейти обратно: Перейти обратно: а б «Распределенная открытая архитектура Nuprl 5» . Проект ПРЛ . Проверено 7 марта 2015 г.
- ^ «Система Нупрл» . Проект ПРЛ . Проверено 7 марта 2015 г.
- ^ Констебль, Роберт; и др. (1986). Реализация математики с помощью системы разработки доказательств Nuprl . Энглвуд Клиффс, Нью-Джерси: Прентис-Холл. ISBN 1468059106 . Проверено 7 марта 2015 г.
- ^ Аллен, Стюарт; Констебль, Роберт; Итон, Ричард; Крейц, Кристоф; Лориго, Лори. «Открытая логическая среда Nuprl (слайд-презентация 2000 г.)» (PDF) . Проверено 7 марта 2015 г.
- ^ Крейц, Кристоф (2002). Система разработки доказательств Nuprl, версия 5: Справочное руководство и руководство пользователя (PDF) .
- ^ Харпер, Роберт; Ангиули, Карло (10 мая 2017 г.). «Вычислительная теория многомерных типов» (PDF) . 43-й симпозиум ACM SIGPLAN-SIGACT по принципам языков программирования (POPL) .
- ^ «Логика народного усовершенствования» . www.redprl.org . Проверено 24 октября 2017 г.
Внешние ссылки [ править ]
- Веб-страница проекта PRL в Корнельском университете. Текущие сопровождающие Nuprl имеют обширную документацию и публикации по Nuprl.
- Бывшая веб-страница проекта PRL на Wayback Machine (архивировано 14 ноября 2023 г.).
- Введение на уровне пользователя в систему разработки доказательств Nuprl (доклад 2001 г. в Scholarly Commons Пенсильванского университета)
- Веб-страница RedPRL
| Базы данных органов управления : Национальные |
|---|
