LCF
LCF es un demostrador automático de teoremas interactivo desarrollado en la Universidad de Edimburgo y la Universidad de Stanford por Robin Milner y otros. LCF introdujo el lenguaje de programación ML, para permitir al usuario escribir tácticas de demostración. Los teoremas en LCF son proposiciones del tipo de dato abstracto teorema. El sistema de tipos de ML garantiza que solo proposiciones demostradas basadas en axiomas y reglas de inferencia tengan el tipo teorema. Entre los sucesores de LCF están los demostradores de teoremas HOL e Isabelle. Entre los lenguajes de programación descendientes de ML están Standard ML y OCaml.
LCF es un demostrador automático de teoremas interactivo desarrollado en la Universidad de Edimburgo y la Universidad de Stanford por Robin Milner y otros.[1]
LCF introdujo el lenguaje de programación ML, para permitir al usuario escribir tácticas de demostración. Los teoremas en LCF son proposiciones del tipo de dato abstracto teorema.[2] El sistema de tipos de ML garantiza que solo proposiciones demostradas basadas en axiomas y reglas de inferencia tengan el tipo teorema.
Entre los sucesores de LCF están los demostradores de teoremas HOL e Isabelle. Entre los lenguajes de programación descendientes de ML están Standard ML y OCaml.
Referencias
[editar]- ↑ Gordon, Michael J. C. (1996). «From LCF to HOL: a short history». Consultado el 2 de febrero de 2016.
- ↑ * Milner, Robin (mayo de 1972). Logic for Computable Functions: description of a machine implementation.. Stanford University. Consultado el 2 de febrero de 2016.
| Control de autoridades |
|
|---|
Datos: Q6667462