Hispanopedia Wiki
Articulo de referencia

Nuprl

Nuprl es un sistema de desarrollo de demostraciones que proporciona análisis y demostraciones asistidas por ordenador de enunciados matemáticos formales, así como herramientas p...

Hispanopedia WikiContenido en espanolLectura gratuita

Nuprl es un sistema de desarrollo de demostraciones que proporciona análisis y demostraciones asistidas por ordenador de enunciados matemáticos formales, así como herramientas para la verificación y optimización de software. Desarrollado originalmente en la década de 1980 por Robert Lee Constable y otros, el sistema es mantenido actualmente por el Proyecto PRL de la Universidad de Cornell . La versión compatible actualmente, Nuprl 5, también se conoce como FDL (Formal Digital Library). Nuprl funciona como un sistema automatizado de demostración de teoremas y también puede utilizarse para proporcionar asistencia en la elaboración de demostraciones .

Diseño

Nuprl utiliza un sistema de tipos basado en la teoría de tipos intuicionista de Martin-Löf para modelar enunciados matemáticos en una biblioteca digital . Las teorías matemáticas se pueden construir y analizar con una variedad de editores, incluyendo una interfaz gráfica de usuario , un editor basado en web y un modo Emacs . Una variedad de evaluadores y motores de inferencia pueden operar sobre los enunciados en la biblioteca. Los traductores también permiten manipular enunciados con programas Java y OCaml . [ 1 ] El sistema general se controla con una variante de ML .

La arquitectura de Nuprl 5 se describe como una " arquitectura abierta distribuida " [ 1 ] y Nuprl 5 está pensado principalmente para ser utilizado como un servicio web en lugar de como un software independiente.

Historia

Nuprl se lanzó por primera vez en 1984 y se describió en detalle en el libro Implementing Mathematics with the Nuprl Proof Development System , [ 2 ] publicado en 1986. Nuprl 2 fue la primera versión para Unix . Nuprl 3 proporcionó demostraciones computacionales para problemas matemáticos relacionados con la paradoja de Girard y el lema de Higman . Nuprl 4, la primera versión desarrollada para la World Wide Web , se utilizó para verificar protocolos de coherencia de caché y otros sistemas informáticos. [ 3 ]

La arquitectura del sistema actual, implementada en Nuprl 5, se propuso por primera vez en un artículo de conferencia del año 2000. Un manual de referencia para Nuprl 5 se publicó en 2002. [ 4 ] Nuprl ha sido objeto de numerosas publicaciones en el campo de la informática .

Sucesores

Los sistemas JonPRL y RedPRL también se basan en la teoría de tipos computacional. [ 5 ] RedPRL está explícitamente "inspirado en Nuprl". [ 6 ]

Referencias

  1. 1 2 "Nuprl 5 arquitectura abierta distribuida" . Proyecto PRL . Archivado del original el 15 de junio de 2018. Recuperado el 7 de marzo de 2015 .
  2. ↑ Constable, Robert; et al. (1986). Implementing Mathematics with The Nuprl Proof Development System . Englewood Cliffs, NJ: Prentice-Hall. ISBN  1468059106Consultado el 7 de marzo de 2015 .
  3. ↑ Allen, Stuart; Constable, Robert; Eaton, Richard; Kreitz, Christoph; Lorigo, Lori. "El entorno lógico abierto Nuprl (presentación de diapositivas de 2000)" (PDF) . Consultado el 7 de marzo de 2015 .
  4. ↑ Kreitz, Christoph (2002). El sistema de desarrollo de pruebas Nuprl, versión 5: manual de referencia y guía del usuario (PDF) .
  5. ↑ Harper, Robert; Angiuli, Carlo (10 de mayo de 2017). «Teoría de tipos computacional de dimensiones superiores» (PDF) . Actas del 44.º Simposio ACM SIGPLAN sobre Principios de Lenguajes de Programación . págs. 680–693 . doi : 10.1145/3009837.3009861 . ISBN  978-1-4503-4660-3.
  6. ↑ "La lógica del refinamiento del pueblo" . www.redprl.org . Consultado el 24 de octubre de 2017 .
  • Página web del proyecto PRL en la Universidad de Cornell. Los actuales responsables del mantenimiento de Nuprl cuentan con amplia documentación y publicaciones sobre Nuprl.
  • Antigua página web del proyecto PRL en Wayback Machine (archivada el 14 de noviembre de 2023) .
  • Introducción a nivel de usuario del sistema de desarrollo de pruebas Nuprl (documento de 2001 presentado en el Centro de Recursos Académicos de la Universidad de Pensilvania)
  • Página web de RedPRL