Top Qs
Línea de tiempo
Chat
Contexto

LCF

De Wikipedia, la enciclopedia libre

Remove ads

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.

Remove ads

Referencias

Loading related searches...

Wikiwand - on

Seamless Wikipedia browsing. On steroids.

Remove ads