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.[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

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.

Datos: Q6667462

Este artículo ha sido escrito por Wikipedia. El texto está disponible bajo la licencia Creative Commons - Atribución - CompartirIgual. Pueden aplicarse cláusulas adicionales a los archivos multimedia.

[1] Gordon, Michael J. C. (1996). «From LCF to HOL: a short history». Consultado el 2 de febrero de 2016.

[2] Milner, Robin (mayo de 1972). Logic for Computable Functions: description of a machine implementation.. Stanford University. Consultado el 2 de febrero de 2016.

[3] Milner, Robin (mayo de 1972). Logic for Computable Functions: description of a machine implementation.. Stanford University. Consultado el 2 de febrero de 2016.