In type theory, the LF logical framework provides a means to define (or present) logics. It 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.

PropertyValue
dbpprop:abstract
  • In type theory, the LF logical framework provides a means to define (or present) logics. It 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’. In the case of the LF logical framework, the language is the <math>\lambda\Pi</math>-calculus. This is a system of first-order dependent function types which are related by the propositions as types principle to first-order minimal logic. The key features of the <math>\lambda\Pi</math>-calculus are that it consists of entities of three levels: objects, types and families of types. It is predicative, all well-typed terms are strongly normalizing and Church-Rosser and the property of being well-typed is decidable. However, type inference is undecidable. A logic is represented in the LF logical framework by the judgements-as-types representation mechanism. This is inspired by from Per Martin-Löf's development of Kant's notion of judgement. The two higher-order judgements, the hypothetical <math>J\vdash K</math> and the general, <math>\Lambda x\in J. K(x)</math>, correspond to the ordinary and dependent function space, respectively. The methodology of judgements-as-types is that judgements are represented as the types of their proofs. A logical system <math>{\mathcal L}</math> is represented by its signature which assigns kinds and types to a finite set of constants that represents its syntax, its judgements and its rule schemes. An object-logic's rules and proofs are seen as primitive proofs of hypothetico-general judgements <math>\Lambda x\in C. J(x)\vdash K</math>. An implementation of the LF logical framework is provided by the Twelf system at Carnegie Mellon University. Twelf includes a logic programming engine meta-theoretic reasoning about logic programs (termination, coverage, etc. ) an inductive meta-logical theorem prover
  • 在类型论中，LF 逻辑框架提供了定义(或表示)逻辑的一种方式。它基于了通过有依赖类型的lambda 演算方式的对语法、规则和证明的一般性处理。语法按类似于但更一般性的 Per Martin-Löf 文章中的系统的风格来处理。 要描述一个逻辑框架，你必须提供如下: 1. 对要表示的那一类对象-逻辑的特征描述； 2. 适当的元-语言； 3. 对表示对象-逻辑的机制的特征描述。 总结为: “框架 = 语言 + 表示”。 在 LF 逻辑框架的情况下，这个语言是 <math>\lambda\Pi</math>-演算。这是与对一阶极小逻辑的命题为类型原理有关的一阶依赖函数类型的一个系统。<math>\lambda\Pi</math>-演算的关键特征是它由三层的实体组成: 对象、类型和类型家族。它是直谓性的，所有良好类型的项都是强规范化的和有 Church-Rosser定理性质的，是强类型的性质是可判定性的。但是类型推论是不可判定性的。 逻辑在 LF 逻辑框架中通过判断为类型编码来表示。这来源于 Per Martin-Löf 对康德的判断的概念的发展。两个高阶判断，假言的 <math>J\vdash K</math> 和一般的 <math>\Lambda x\in J. K(x)</math>，分别对应于普通的和依赖的函数空间。判断为类型的方法论是把判断表示为它们的证明的类型。逻辑系统 <math>{\mathcal L}</math> 由把种类(kind)和类型指派到表示它的语法、它的判断和它的规则模式(scheme)的有限集合的它的标署(signature)来表示。对象-逻辑的规则和证明被看做假言-一般判断 <math>\Lambda x\in C. J(x)\vdash K</math> 的原始证明。 LF 逻辑框架在卡内基梅隆大学的 Twelf 系统中实现了。Twelf 包括 逻辑编程引擎 关于逻辑编程(终止，覆盖等)的元理论推理 归纳法元逻辑定理证明器
dbpprop:hasPhotoCollection
rdfs:comment
  • In type theory, the LF logical framework provides a means to define (or present) logics. It 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.
  • 在类型论中，LF 逻辑框架提供了定义(或表示)逻辑的一种方式。它基于了通过有依赖类型的lambda 演算方式的对语法、规则和证明的一般性处理。语法按类似于但更一般性的 Per Martin-Löf 文章中的系统的风格来处理。 要描述一个逻辑框架，你必须提供如下: 1. 对要表示的那一类对象-逻辑的特征描述； 2. 适当的元-语言； 3.
rdfs:label
  • LF (logical framework)
  • 逻辑框架
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of