Нупрл - Википедия - Nuprl

Нупрл это система разработки доказательств, обеспечивающая компьютерный анализ и доказательства формальных математических утверждений, а также инструменты для проверки и оптимизации программного обеспечения. Первоначально разработанный в 1980-х годах Роберт Ли Констебль и другие, система теперь поддерживается проектом PRL по адресу Корнелл Университет. Поддерживаемая в настоящее время версия Nuprl 5 также известна как FDL (формальная цифровая библиотека). Nuprl функционирует как автоматическое доказательство теорем система, а также может использоваться для предоставления доказательная помощь.

Дизайн

Nuprl использует систему типов на основе Мартина-Лёфа интуиционистская теория типов моделировать математические утверждения в цифровая библиотека. Математические теории можно строить и анализировать с помощью различных редакторов, в том числе графический интерфейс пользователя, веб-редактор и Emacs режим. С операторами в библиотеке могут работать различные оценщики и механизмы вывода. Переводчики также позволяют манипулировать утверждениями с помощью Ява и OCaml программы.[1] Вся система управляется с помощью варианта ML.

Архитектура Nuprl 5 описывается как "распределенная открытая архитектура "[1] и предназначен в первую очередь для использования в качестве веб-сервис а не как отдельное программное обеспечение. Те, кто заинтересован в использовании веб-сервиса или переносе теорий из старых версий Nuprl, могут связаться с Адрес электронной почты приведено на веб-странице системы Nuprl.[2]

История

Nuprl был впервые выпущен в 1984 году и впервые был подробно описан в книге Внедрение математики с помощью системы разработки доказательств Nuprl,[3] опубликовано в 1986 году. Nuprl 2 была первой версией Unix. Nuprl 3 предоставил машинное доказательство для математических задач, связанных с Парадокс Жирара и Лемма хигмана. Nuprl 4, первая версия, разработанная для Всемирная паутина, использовался для проверки протоколов согласованности кэша и других компьютерных систем.[4]

Текущая системная архитектура, реализованная в Nuprl 5, была впервые предложена в 2000 г. доклад конференции. Справочное руководство для Nuprl 5 было опубликовано в 2002 году.[5] Nuprl был предметом многих Информатика публикации, некоторые из которых датируются 2014 годом.[6]

Преемники

Оба JonPRL и RedPRL системы также основаны на теории вычислительного типа.[7] RedPRL явно «вдохновлен Nuprl».[8]

Рекомендации

  1. ^ а б «Распределенная открытая архитектура Nuprl 5». Проект PRL. Получено 7 марта 2015.
  2. ^ «Система Нупрл». Проект PRL. Получено 7 марта 2015.
  3. ^ Констебль, Роберт; и другие. (1986). Реализация математики с помощью системы разработки доказательств Nuprl. Энглвуд Клиффс, Нью-Джерси: Прентис-Холл. ISBN  1468059106. Получено 7 марта 2015.
  4. ^ Аллен, Стюарт; Констебль, Роберт; Итон, Ричард; Крайц, Кристоф; Лориго, Лори. "Открытая логическая среда Nuprl (презентация 2000 г.)" (PDF). Получено 7 марта 2015.
  5. ^ Крайц, Кристоф (2002). Система разработки Nuprl Proof, версия 5: справочное руководство и руководство пользователя (PDF).
  6. ^ «Проект ПРЛ - База знаний». Проект PRL. Получено 7 марта 2015.
  7. ^ Харпер, Роберт; Ангиули, Карло (10 мая 2017 г.). «Вычислительная теория многомерных типов» (PDF). 43-й симпозиум ACM SIGPLAN-SIGACT по принципам языков программирования (POPL).
  8. ^ "Логика народного уточнения". www.redprl.org. Получено 2017-10-24.

внешняя ссылка