Logic for Computable Functions (original) (raw)
Logic for Computable Functions (LCF) is an interactive automated theorem prover developed at Stanford and Edinburgh by Robin Milner and collaborators in early 1970s, based on the theoretical foundation of logic of computable functions previously proposed by Dana Scott. Work on the LCF system introduced the general-purpose programming language ML to allow users to write theorem-proving tactics, supporting algebraic data types, parametric polymorphism, abstract data types, and exceptions.
| Property | Value |
|---|---|
| dbo:abstract | 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 e Isabelle. Entre los lenguajes de programación descendientes de ML están Standard ML y . (es) Logic for Computable Functions (LCF) is an interactive automated theorem prover developed at Stanford and Edinburgh by Robin Milner and collaborators in early 1970s, based on the theoretical foundation of logic of computable functions previously proposed by Dana Scott. Work on the LCF system introduced the general-purpose programming language ML to allow users to write theorem-proving tactics, supporting algebraic data types, parametric polymorphism, abstract data types, and exceptions. (en) Logic for Computable Functions (рус. Логика для вычислимых функций), (LCF) — инструмент для интерактивного автоматического доказательства теорем, разработанный Робином Милнером и его сотрудниками в Стэнфорде и Эдинбурге в начале 1970-х годов на базе одноимённой дедуктивной системы, предложенной Даной Скоттом. В ходе работы над системой LCF был разработан универсальный язык программирования ML. Его применение в системе позволило пользователям писать тактики доказательства теорем, поддерживающие алгебраические типы данных, параметрический полиморфизм, абстрактные типы данных и исключения. (ru) |
| dbo:wikiPageExternalLink | http://www.dtic.mil/dtic/tr/fulltext/u2/785072.pdf http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.html |
| dbo:wikiPageID | 161900 (xsd:integer) |
| dbo:wikiPageLength | 5586 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1107472529 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Robin_Milner dbr:University_of_Edinburgh dbr:ML_(programming_language) dbr:Stanford_University dbr:Parametric_polymorphism dbr:Trusted_computing_base dbr:HOL_Light dbr:Logic_of_Computable_Functions dbr:Abstract_data_type dbr:Algebraic_data_type dbr:Dana_Scott dbr:Exception_handling dbr:Abstract_data_types dbr:HOL_(proof_assistant) dbc:Logic_in_computer_science dbc:Proof_assistants dbr:Automated_theorem_prover dbr:Programming_language dbr:Isabelle_proof_assistant dbr:Inference_rule |
| dbp:wikiPageUsesTemplate | dbt:Cite_book dbt:Refbegin dbt:Refend dbt:Reflist dbt:See_also dbt:Short_description dbt:Mathlogic-stub dbt:Cite_manual |
| dcterms:subject | dbc:Logic_in_computer_science dbc:Proof_assistants |
| gold:hypernym | dbr:Prover |
| rdf:type | owl:Thing dbo:Software yago:Assistant109815790 yago:CausalAgent100007347 yago:LivingThing100004258 yago:Object100002684 yago:Organism100004475 yago:Person100007846 yago:PhysicalEntity100001930 yago:Worker109632518 yago:YagoLegalActor yago:YagoLegalActorGeo yago:Whole100003553 yago:WikicatProofAssistants |
| rdfs:comment | Logic for Computable Functions (LCF) is an interactive automated theorem prover developed at Stanford and Edinburgh by Robin Milner and collaborators in early 1970s, based on the theoretical foundation of logic of computable functions previously proposed by Dana Scott. Work on the LCF system introduced the general-purpose programming language ML to allow users to write theorem-proving tactics, supporting algebraic data types, parametric polymorphism, abstract data types, and exceptions. (en) Logic for Computable Functions (рус. Логика для вычислимых функций), (LCF) — инструмент для интерактивного автоматического доказательства теорем, разработанный Робином Милнером и его сотрудниками в Стэнфорде и Эдинбурге в начале 1970-х годов на базе одноимённой дедуктивной системы, предложенной Даной Скоттом. В ходе работы над системой LCF был разработан универсальный язык программирования ML. Его применение в системе позволило пользователям писать тактики доказательства теорем, поддерживающие алгебраические типы данных, параметрический полиморфизм, абстрактные типы данных и исключения. (ru) 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. (es) |
| rdfs:label | LCF (es) Logic for Computable Functions (en) Logic for Computable Functions (ru) |
| rdfs:seeAlso | dbr:Logic_of_Computable_Functions |
| owl:sameAs | freebase:Logic for Computable Functions yago-res:Logic for Computable Functions wikidata:Logic for Computable Functions dbpedia-es:Logic for Computable Functions dbpedia-ru:Logic for Computable Functions dbpedia-tr:Logic for Computable Functions https://global.dbpedia.org/id/4rDu4 |
| prov:wasDerivedFrom | wikipedia-en:Logic_for_Computable_Functions?oldid=1107472529&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Logic_for_Computable_Functions |
| is dbo:wikiPageDisambiguates of | dbr:LCF |
| is dbo:wikiPageRedirects of | dbr:LCF_theorem_prover dbr:LCF_(theorem_prover) |
| is dbo:wikiPageWikiLink of | dbr:Robin_Milner dbr:School_of_Informatics,_University_of_Edinburgh dbr:List_of_University_of_Edinburgh_people dbr:LCF_theorem_prover dbr:ML_(programming_language) dbr:Standard_ML dbr:Type_theory dbr:Logic_of_Computable_Functions dbr:Milner_Award dbr:OCaml dbr:LCF dbr:LCF_(theorem_prover) |
| is foaf:primaryTopic of | wikipedia-en:Logic_for_Computable_Functions |