Matches in DBpedia 2014 for { <http://dbpedia.org/resource/Logical_framework> ?p ?o. }
Showing items 1 to 33 of
33
with 100 items per page.
- Logical_framework abstract "In logic, a logical framework provides a means to define (or present) a logic as a signature in a higher-order type theory in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework type theory. This approach has been used successfully for (interactive) automated theorem proving. The first logical framework was Automath, however the name of the idea comes from the more widely known Edinburgh Logical Framework, LF. Several more recent proof tools like Isabelle are based on this idea. Unlike a direct embedding, the logical framework approach allows many logics to be embedded in the same type system.A logical framework is based on a general treatment of syntax, rules and proofs by means of a dependently typed lambda calculus. Syntax is treated in a style similar to, but more general than Per Martin-Löf's system of arities.To describe a logical framework, one must provide the following: A characterization of the class of object-logics to be represented; An appropriate meta-language; A characterization of the mechanism by which object-logics are represented.This is summarized by:‘Framework = Language + Representation’.".
- Logical_framework wikiPageExternalLink book.
- Logical_framework wikiPageExternalLink lfs-impl.html.
- Logical_framework wikiPageExternalLink mdorf01.pdf.
- Logical_framework wikiPageExternalLink meaning.html.
- Logical_framework wikiPageID "901613".
- Logical_framework wikiPageRevisionID "602614846".
- Logical_framework hasPhotoCollection Logical_framework.
- Logical_framework subject Category:Dependently_typed_programming.
- Logical_framework subject Category:Logic_in_computer_science.
- Logical_framework subject Category:Proof_assistants.
- Logical_framework subject Category:Type_theory.
- Logical_framework type Assistant109815790.
- Logical_framework type CausalAgent100007347.
- Logical_framework type LivingThing100004258.
- Logical_framework type Object100002684.
- Logical_framework type Organism100004475.
- Logical_framework type Person100007846.
- Logical_framework type PhysicalEntity100001930.
- Logical_framework type ProofAssistants.
- Logical_framework type Whole100003553.
- Logical_framework type Worker109632518.
- Logical_framework type YagoLegalActor.
- Logical_framework type YagoLegalActorGeo.
- Logical_framework comment "In logic, a logical framework provides a means to define (or present) a logic as a signature in a higher-order type theory in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework type theory. This approach has been used successfully for (interactive) automated theorem proving. The first logical framework was Automath, however the name of the idea comes from the more widely known Edinburgh Logical Framework, LF.".
- Logical_framework label "Logical framework".
- Logical_framework label "逻辑框架".
- Logical_framework sameAs m.03n7s_.
- Logical_framework sameAs Q6667502.
- Logical_framework sameAs Q6667502.
- Logical_framework sameAs Logical_framework.
- Logical_framework wasDerivedFrom Logical_framework?oldid=602614846.
- Logical_framework isPrimaryTopicOf Logical_framework.