LCF
De Wikipedia, la enciclopedia libre
LCF es un demostrador 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.
