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

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

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

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

Nuprl 5's architecture is described as "distributed open architecture"[1] and intended primarily to be used as a web service rather than as standalone software. Those interested in using the web service, or migrating theories from older versions of Nuprl, can contact the email address given on the Nuprl System web page.[2]

History[edit]

Nuprl was first released in 1984, and was first described in detail in the book Implementing Mathematics with the Nuprl Proof Development System,[3] published in 1986. Nuprl 2 was the first Unix version. Nuprl 3 provided machine proof for mathematical problems related to Girard's paradox and Higman's lemma. Nuprl 4, the first version developed for the World Wide Web, was used to verify cache coherency protocols and other computer systems.[4]

The current system architecture, implemented in Nuprl 5, was first proposed in a 2000 conference paper. A reference manual for Nuprl 5 was published in 2002.[5] Nuprl has been the subject of many computer science publications, some as recent as 2014.[6]

Successors[edit]

Both the JonPRL and RedPRL systems are also based on computational type theory.[7] RedPRL is explicitly "inspired by Nuprl".[8]

References[edit]

  1. ^ a b "Nuprl 5 distributed open architecture". PRL Project. Retrieved 7 March 2015.
  2. ^ "Nuprl System". PRL Project. Retrieved 7 March 2015.
  3. ^ Constable, Robert; et al. (1986). Implementing Mathematics with The Nuprl Proof Development System. Englewood Cliffs, NJ: Prentice-Hall. ISBN 1468059106. Retrieved 7 March 2015.
  4. ^ Allen, Stuart; Constable, Robert; Eaton, Richard; Kreitz, Christoph; Lorigo, Lori. "The Nuprl Open Logical Environment (2000 slide presentation)" (PDF). Retrieved 7 March 2015.
  5. ^ Kreitz, Christoph (2002). The Nuprl Proof Development System, Version 5: Reference Manual and User’s Guide (PDF).
  6. ^ "PRL Project - Knowledge Base". PRL Project. Retrieved 7 March 2015.
  7. ^ Harper, Robert; Angiuli, Carlo (May 10, 2017). "Computational higher-dimensional type theory" (PDF). 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).
  8. ^ "The People's Refinement Logic". www.redprl.org. Retrieved 2017-10-24.

External links[edit]

  • PRL Project web page. The current maintainers of Nuprl have extensive documentation and publications on Nuprl.
  • A User-Level Introduction to the Nuprl Proof Development System (2001 paper at the University of Pennsylvania Scholarly Commons)
  • RedPRL web page