| dbo: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. (en)
- 在类型论中，LF 逻辑框架提供了定义(或表示)逻辑的一种方式。它基于了通过有依赖类型的lambda 演算方式的对语法、规则和证明的一般性处理。语法按类似于但更一般性的 Per Martin-Löf 文章中的系统的风格来处理。 要描述一个逻辑框架，你必须提供如下: 1. 对要表示的那一类对象-逻辑的特征描述； 2. 适当的元-语言； 3. 对表示对象-逻辑的机制的特征描述。 总结为: “框架 = 语言 + 表示”。 在 LF 逻辑框架的情况下，这个语言是 -演算。这是与对一阶极小逻辑的命题为类型原理有关的一阶依赖函数类型的一个系统。-演算的关键特征是它由三层的实体组成: 对象、类型和类型家族。它是直谓性的，所有良好类型的项都是强规范化的和有 性质的，是强类型的性质是可判定性的。但是类型推论是不可判定性的。 逻辑在 LF 逻辑框架中通过判断为类型编码来表示。这来源于 Per Martin-Löf 对康德的判断的概念的发展。两个高阶判断，假言的 和一般的 ，分别对应于普通的和依赖的函数空间。判断为类型的方法论是把判断表示为它们的证明的类型。逻辑系统 由把种类(kind)和类型指派到表示它的语法、它的判断和它的规则模式(scheme)的有限集合的它的标署(signature)来表示。对象-逻辑的规则和证明被看做假言-一般判断 的原始证明。 LF 逻辑框架在卡内基梅隆大学的 系统中实现了。Twelf 包括
* 逻辑编程引擎
* 关于逻辑编程(终止，覆盖等)的元理论推理
* 归纳法定理证明器 (zh)
|
| dbo:wikiPageExternalLink
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 7413 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| dbp:wikiPageUsesTemplate
| |
| dcterms:subject
| |
| rdf:type
| |
| rdfs: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. 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. (en)
- 在类型论中，LF 逻辑框架提供了定义(或表示)逻辑的一种方式。它基于了通过有依赖类型的lambda 演算方式的对语法、规则和证明的一般性处理。语法按类似于但更一般性的 Per Martin-Löf 文章中的系统的风格来处理。 要描述一个逻辑框架，你必须提供如下: 1. 对要表示的那一类对象-逻辑的特征描述； 2. 适当的元-语言； 3. 对表示对象-逻辑的机制的特征描述。 总结为: “框架 = 语言 + 表示”。 在 LF 逻辑框架的情况下，这个语言是 -演算。这是与对一阶极小逻辑的命题为类型原理有关的一阶依赖函数类型的一个系统。-演算的关键特征是它由三层的实体组成: 对象、类型和类型家族。它是直谓性的，所有良好类型的项都是强规范化的和有 性质的，是强类型的性质是可判定性的。但是类型推论是不可判定性的。 逻辑在 LF 逻辑框架中通过判断为类型编码来表示。这来源于 Per Martin-Löf 对康德的判断的概念的发展。两个高阶判断，假言的 和一般的 ，分别对应于普通的和依赖的函数空间。判断为类型的方法论是把判断表示为它们的证明的类型。逻辑系统 由把种类(kind)和类型指派到表示它的语法、它的判断和它的规则模式(scheme)的有限集合的它的标署(signature)来表示。对象-逻辑的规则和证明被看做假言-一般判断 的原始证明。 (zh)
|
| rdfs:label
|
- Logical framework (en)
- 逻辑框架 (zh)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:isPrimaryTopicOf
| |
| is dbo:wikiPageDisambiguates
of | |
| is dbo:wikiPageRedirects
of | |
| is dbo:wikiPageWikiLink
of | |
| is foaf:primaryTopic
of | |
