Logic for Computable Functions
http://dbpedia.org/resource/Logic_for_Computable_Functions an entity of type: Thing
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.
rdf:langString
Logic for Computable Functions (рус. Логика для вычислимых функций), (LCF) — инструмент для интерактивного автоматического доказательства теорем, разработанный Робином Милнером и его сотрудниками в Стэнфорде и Эдинбурге в начале 1970-х годов на базе одноимённой дедуктивной системы, предложенной Даной Скоттом. В ходе работы над системой LCF был разработан универсальный язык программирования ML. Его применение в системе позволило пользователям писать тактики доказательства теорем, поддерживающие алгебраические типы данных, параметрический полиморфизм, абстрактные типы данных и исключения.
rdf:langString
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.
rdf:langString
rdf:langString
LCF
rdf:langString
Logic for Computable Functions
rdf:langString
Logic for Computable Functions
xsd:integer
161900
xsd:integer
1107472529
rdf:langString
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 .
rdf:langString
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.
rdf:langString
Logic for Computable Functions (рус. Логика для вычислимых функций), (LCF) — инструмент для интерактивного автоматического доказательства теорем, разработанный Робином Милнером и его сотрудниками в Стэнфорде и Эдинбурге в начале 1970-х годов на базе одноимённой дедуктивной системы, предложенной Даной Скоттом. В ходе работы над системой LCF был разработан универсальный язык программирования ML. Его применение в системе позволило пользователям писать тактики доказательства теорем, поддерживающие алгебраические типы данных, параметрический полиморфизм, абстрактные типы данных и исключения.
xsd:nonNegativeInteger
5586