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