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.
Property | Value |
---|---|
dbo:abstract |
|
dbo:wikiPageID |
|
dbo:wikiPageLength |
|
dbo:wikiPageRevisionID |
|
dct:subject | |
rdfs:comment |
|
rdfs:label |
|
owl:sameAs | |
prov:wasDerivedFrom | |
foaf:isPrimaryTopicOf | |
is owl:sameAs of | |
is foaf:primaryTopic of |