逻辑框架

在逻辑学中，逻辑框架提供了一种方法来定义（或呈现）一个逻辑作为高阶类型理论中的签名，其方式是原始逻辑中公式的可证明性减少为框架类型理论中的类型栖息问题。这种方法已经成功地用于（交互式）自动定理的证明。

第 一个逻辑框架是Automath；然而，这个想法的名字来自更广为人知的爱丁堡逻辑框架，LF。最近的几个证明工具，如Isabelle，都是基于这个思想。与直接嵌入不同，逻辑框架的方法允许许多逻辑学被嵌入到同一个类型系统中。

逻辑框架是基于对语法、规则和证明的一般处理，其手段是依赖类型的λ微积分。语法的处理方式类似于PerMartin-Löf的arities系统，但比它更普遍。

为了描述一个逻辑框架，我们必须提供以下内容。对要表示的对象逻辑类别的描述；适当的元语言；对表示对象逻辑的机制的描述。这被总结为：框架=语言+表示法。

在LF逻辑框架的情况下，元语言是λΠ-calculus。这是一个由一阶从属函数类型组成的系统，通过命题类型原则与一阶最小逻辑相关。

λΠ-微积分的主要特征是，它由三个层次的实体组成：对象、类型和种类（或类型类，或类型族）。

它是预言性的，所有类型良好的术语都是强规范化和Church-Rosser的，类型良好的属性是可解的。然而，类型推理是不可判定的。

一个逻辑在LF逻辑框架中是由判断即类型的表示机制来表示的。这是受PerMartin-Löf在1983年锡耶纳讲座中对康德的判断概念的发展所启发。

两个高阶判断，即假设性的{displaystyleλxinJ.K(x)}，对应于普通函数和依赖函数。分别对应于普通函数空间和依赖函数空间。判断即类型的方法是，判断被表示为其证明的类型。

一个逻辑系统L{displaystyle{mathcal{L}}的逻辑系统由其签名来表示。｝是由它的签名来表示的，它把种类和类型分配给一个有限的常数集，代表它的语法、它的判断和它的规则方案。

一个对象逻辑的规则和证明被看作是假设性一般判断的原始证明卡内基梅隆大学的Twelf系统提供了一个LF逻辑框架的实现。

关于逻辑程序的元理论推理（终止、覆盖等）一个归纳的元逻辑定理验证器。