Из Википедии, свободной энциклопедии
Перейти к навигации Перейти к поиску

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

Дизайн [ править ]

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

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

История [ править ]

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

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

Преемники [ править ]

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

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

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

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

  • Веб-страница проекта PRL . Текущие сопровождающие Nuprl имеют обширную документацию и публикации по Nuprl.
  • Введение на пользовательском уровне в систему разработки доказательств Nuprl (статья 2001 г. в Университете Пенсильвании Scholarly Commons)
  • Веб-страница RedPRL