89理论计算机科学电子笔记42（2001）网址：http://www.elsevier.nl/locate/entcs/volume42.html15页在逻辑框架中嵌入显示演算：比较Isabelle和Bisabelf杰瑞米·E道森1号澳大利亚国立大学RajeevGor'e2澳大利亚国立大学信息科学与工程和澳大利亚国立大学摘要逻辑框架是计算机系统，允许用户使用基于数理逻辑和丘奇类型理论的专门设计的语言来形式化系统它们可以用来从逻辑规范中导出程序，从而保证结果程序的正确性它们也可以用来形式化关于逻辑系统的严格证明。 本文比较了在Isabelle和Isabelf逻辑框架中实现关系代数的显示演算δRA的几种方法。我们的目标是实现使我们能够在逻辑框架内形式化证明理论结果，例如δRA的切消定理和任何相关的证明长度增加我们将讨论由这一要求引起的问题。1介绍和动机逻辑框架是计算机系统，允许用户使用基于数理逻辑和丘奇类型理论的专门设计的语言来形式化数学。它们可以用来从逻辑规范中导出程序，从而保证结果程序的正确性。它们也可以用来形式化关于逻辑系统的严格证明1由澳大利亚研究委员会小额研究补助金支持。2由澳大利亚研究理事会伊丽莎白二世女王奖学金资助。2001年由ElsevierScien ceB出版。 诉 操作访问和C CB Y-NC-N D链接。DAWSON和G或E'90► ∨► ∨►►∨关系代数[12]是布尔代数的扩展;而布尔代数模型给定集合的子集，关系代数模型给定集合上的二元关系。关系代数具有诸如关系合成和关系逆的运算，以及诸如交（合取）和补（求反）的布尔运算。 关系代数是关系数据库的基础[6]，也是程序的规范和正确性证明的基础，特别是在Mili [15]的风格显示逻辑[1]是一个非经典逻辑的通用的可扩展框架它的优点包括一个通用的切消定理，只要显示计算的规则满足某些容易检查的条件，该定理就适用。它是一种非常普遍的逻辑形式主义，以统一的方式适用于许多（经典和非经典）逻辑[10]，[22]。显示框架的通用性意味着本质上相同的元级证明适用于许多不同的逻辑。严格的机械形式化的证明，然后广泛适用，值得追求。在本文中，我们讨论的实施δRA，关系代数的显示演算，作为一个案例研究，探索各种方法，这样一个机械形式化的显示演算一般。显示演算扩展了根岑的语言的顺序与额外的，复杂的，n元结构连接词，除了根岑的唯一的结构连接词，“逗号”。 虽然根岑假设逗号是联想的，交换的和固有的多价，显示演算没有这样的隐含假设。像这样的属性被明确地声明为结构规则。例如，δRA-序列是用二进制逗号、二进制分号和一元结构连接词来构建的因此，根岑的序列Γ假设Γ和是逗号分隔的公式列表，而δ RA序列X Y假设X和Y是由公式连同逗号、、和·构建的复杂树状结构。显示演算的定义特征是，在所有逻辑引入规则中，主公式总是作为右手或左手边的整体“显示”。 例如，规则（LK-），如左下方所示，是典型的根岑Γ R，P，Q（LK-R）XR，P，Q（δRA-R）Γ► ∆,P∨Q X►P∨Q直观地说，要在一个XJYJ上向下使用这个显示演算规则，除了（P，Q）之外的所有东西都必须被移动到左边的复杂结构X中，从而将结构（P，Q）显示为整个右手边。有一些规则可以使任何给定的结构得以显示。在规则应用程序之后，我们可以将移动的材料“取消显示”到其原始位置（反转所使用的显示步骤），这条规则的一个重要特点是将[9]见《易经》。DAWSON和G或E'91CPQ伊莎贝尔是一个自动化的证明助理[17]。它的元逻辑是一种直觉主义类型的高阶逻辑，足以支持高阶统一和项重写的内建推理步骤。Isabelle接受“from α 1，α 2，..”形式的推理规则，α n，推断β“，其中α i和β是伊莎贝尔元逻辑的表达式，或者是使用新语法的表达式，由用户定义，用于某些“对象逻辑”。Isabelle用户可以通过使用这些规则模板来编码C L的推理规则集，从而将用于某个逻辑L的特定演算CL编码为例如，如果CL是一个自然演绎演算，那么αi和β将是L的公式，而如果CL是一个自然演绎演算，那么αi和β将是L的序列。 这样的编码被称为在实践中，大多数用户将建立在一个全面的[20]是爱丁堡逻辑框架（LF）[11]的一个实现，它基于具有依赖类型的类型化λ演算。逻辑是用判断作为类型原则来表示的，其中形式为Γ，x：Q，y：P的每个判断都用其证明的类型来标识。 Besidf也接受“from α 1，α2，..”形式的推理规则，α n，推断β“。 但是现在，该规则被表示为类型为α1→α2→.的λ -演算项的声明。→αn→β。 同样，如果我们试图捕获的演算是自然演绎演算，那么αi和β将是公式（类型），但如果演算是一个自然演绎演算，那么αi和β将是序列（类型）。在早期的论文[4]中，我们描述了关系代数的显示演算δRA[9]的Isabelle实现，作为Isabelle的对象逻辑。在那篇论文中，我们描述了我们如何使用实现来证明结果，从证明理论的角度比较关系代数的替代形式化。然而，我们还没有证明这些结果本身在伊莎贝尔，在这个意义上，我们现在解释。假设逻辑L是一组我们认为在某种语义上有效的公式，和是L的两个演算（每个演算都由公理和推理规则组成）。还假设我们有P和Q的机械实现。然后，可以使用P的实现在P中导出Q的每个公理和规则。然后，我们可以走出力学系统，论证（通过归纳Q-导子的大小或结构）因此每个Q-可导的对象（典型的是公式或等式）也是P-可导的。在[4]中，我们使用IsabelleδRA实现来证明关系代数的某些其他演算的可靠性。这些结果在如前一段所述。另一种选择，当一个人这将需要在证明器中实现演算P和Q的不同风格，以便能够对形状进行推理以及P-导子和Q-导子的形式这通常需要DAWSON和G或E'92QPPQ在定理证明器中，对推导中使用的步骤的“树”进行建模，并且每个步骤都是微积分规则的实例，或者这在转需要建模的推理规则或语句的形式以及获得这种推理规则的特定替代实例的方法。术语“浅嵌入”和“深嵌入”经常被使用以区分这些实施方式[2]。因此，我们在[4]（见第2节）中的工作是浅嵌入的一个例子，而第4节中报告的工作是深嵌入。Mikhajlova和von Wright [14]在他们对经典一阶逻辑证明系统的比较这是我们所知的逻辑演算的深度嵌入的唯一另一个例子。其他的元数学结果也被机械化了在本文中，我们比较了各种逻辑框架中嵌入δRA的方法。我们探讨了在BMPF、Isabelle/CTT和Isabelle/HOL中实现“深度嵌入”的可能性。在随后的章节中，我们将描述最初的Isabelle/Pure实现和进一步的工作。2Isabelle/Pure实现Isabelle是一个基于计算机的交互式证明系统，在[17]中描述。它的功能包括高阶统一和项重写。 它是用标准ML编写的[16];用户可以通过输入更多的ML命令，并可以在ML中编程复杂的证明序列。如前所述，用户可用的基本Isabelle构造包括“从α 1，α 2，.，α n，推断β“。这些可以“向前”使用，以从α i获得β，或“向后”使用，以将给定目标β减少到子目标α 1，α 2，.，α n. Isabelle为向后证明和证明搜索（策略）提供了一些基本操作，以及将这些操作组合起来的策略Isabelle也支持前向证明。推理规则共同形成一个简单的元逻辑：一个直觉类型的高阶逻辑。 有三个逻辑运算符：==>（蕴涵，或演绎），==（相等，或可替换），和！！（普遍量化）。例如，[|A1; A2|]==> B，是“从α 1，α2，推断β“的Isabelle表示。这些运算符满足由其预期含义产生的某些性质例如，由于[|A1; A2|]==> B意味着β可以从α1和α2推导出来，那么就有可能从α2和α1推导出β，即，[|A2; A1|] ==> B.同样，由于A == B意味着A可以被B替换，反之亦然，==是自反的，对称的和传递的。这个元逻辑被称为伊莎贝尔的纯粹理论。在大多数情况下，用户会通过定义额外的常量来捕获语法，对象逻辑。例如，为了捕获集合论，我们将添加一个常数（比方说）来代表∈符号，而序列则需要常数的|-'和'，'。几个这样的对象逻辑与IsabelleDAWSON和G或E'93•∧∨► ∨►►分布[18]。一旦对象逻辑的这些语法元素就位，我们就可以将对象逻辑表达式构建到αi和β中。例如，在δRA中，第1节中的（δRA-δR）规则使用元逻辑运算符==>上面讨论的，可以输入为“X元|-P，Q ==>$X|-P v Q”其中，$将δRA-结构（如X）与δRA-公式（如P）区分开来。这个规则是“从α推断β“形式的一个实例在[4]中，δRA在Isabelle中直接在Pure理论之上实现，因此唯一可用的推理规则是δRA的规则。就伊莎贝尔元逻辑而言，我们可以把它的原子公式看作是对象逻辑的公式（对于δRA，是序列）。在这种情况下，这些是X Y形式的δRA-序列，使用对象逻辑“连接词”“，”，“”，“"等构建。.因此，像$X这样的表达式|- （P ==> Q）或A v（B ==> C）是不可能的。注意，上面讨论的α i和β通常只是δRA-序列，但也可以是“复杂的”Isabelle命题，例如$X |-P ==>$Y|-Q我们可以向Isabelle声明δRA演算的公理和推理规则。例如，pp是δ RA中的初始公理;因此它在Isabelle中被声明为规则，P|- P，没有前提。 类似地，δRA的每个规则都被声明为Isabelle规则，如示例中的（）上面的规则。这是一个浅嵌入，这反映在一个事实，即水平栏的搜索规则成为伊莎贝尔==>运算符。在深度嵌入中，如第4节所述，水平条也成为对象级常量。在这种浅嵌入中，仅在ML级别提供对δRA构造（即序列、结构、公式）和推导的形状的访问和操作 例如，在[4]中，我们描述了对δRA进行切割消除的程序。它的输入是一个δRA推导（表示为一个由切割规则实例组成的树），输出是一个不包含切割规则实例的推导。这需要检查推导的形状（表示为δRA规则实例的树）和表示数列的伊莎贝尔项的形状。虽然伊莎贝尔项的形状很容易（通过ML代码），但我们必须稍微改变伊莎贝尔代码，以便记录推导中使用的基本δRA规则，并构建可以操作的推导树。本文所描述的工作的目的是完全在定理证明器中执行割消证明（而不是用ML编写割消程序）。因此，我们需要在定理证明器，如§1中所讨论的。DAWSON和G或E'94→→→→→∈3依赖类型理论实现3.1介绍在依赖类型理论中，类型不仅可以在类型变量上参数化，还可以在项变量上参数化。这一点，再加上判断作为类型原则（其中判断与其证明的类型相同），使我们能够表达显示演算导出规则的推导Curry-Howard同构的一个更简单的例子是在简单类型的λ演算和直觉命题逻辑的自然演绎演算NDInt 设A和B是公式，π是A在NDInt中的导子。还假设A B可在NDInt中导出，并考虑A B的NDInt-导出，其中假设A并导出B。也就是说，它是B的一个推导，其中A被认为是真的;在使用A的地方，它会包含一些符号设ρ（ρ）为B的导数。因此，如果我们用π（A的导数）代替ρ（π）中的π，我们得到B的导数ρ（π），它不依赖于A作为假设。然后，使用π：A表示π：A ρ（π）：A→Bρ（π）：B删除注释π、ρ和如上所述，我们同样可以考虑ρ（。）作为A B的导数，或者作为一个函数，该函数以A的导数（如π）作为参数，并返回B的导数。 如果我们也认为A是“命题A的派生“类型 类型A的参数并返回类型B的结果。（方便的是，相同的符号依赖类型以两种不同的方式扩展了简单类型的λ演算。首先，考虑一个类型I的个体和一个参数化的类型A（i）;也就是说，对于每个个体iI，都有一个类型A（i）。则依赖类型A对应于I上的谓词A，类型A（i）对应于命题A（i）。其次，我们在项的层次上建立了一个对象逻辑，使得对象逻辑的表达式（公式或序列）成为依赖类型λ-演算的项。也就是说，我们可以使用所选对象逻辑的语法为术语安装语法，并声明类型构造函数P（. ），因此对于每个项t，P（t）将意味着这是我们模拟δRA的方法。当我们有一个P（t）类型的项时，把一个表达式（公式）t看作是可导的，有一定的后果。 例如，由于从X→Z，U→V→W和S→S→T类型的函数，我们可以构造函数DAWSON和G或E'95→ → → →→►类型X YZ、VUW和ST，我们有合理的证据弱化、交换和收缩。然而，请注意，在我们对δRA的表述中，这些是在元逻辑层面上，而不是在对象逻辑层面上基于依赖类型的两个理论是爱丁堡逻辑框架（LF）[11]和构造类型理论（CTT）[13]。3.2BMPF的实现[20]是爱丁堡逻辑框架（LF）[11]的一个实现。这是基于具有依赖类型的类型化λ演算。BASINF是用标准ML编写的，用户可以使用它的“ML接口”与系统交互，但只有有限的功能可用。图1是我们的BMPF源文件的摘录。1struct：type.2|-：struct -> struct -> type。3* ：struct -> struct.4%显示假设5sA：（* X|-Y）->（* Y|-X）。6 秒：（X|-* Y）->（Y|-* X）。7%派生结构规则8ssAS 1 = [D] sA（sS D）。图1.一、源代码示例第1行声明struct作为一个新类型来表示δRA结构。第2行声明|-作为二进制类型构造函数，接受两个struct类型的term参数并返回类型。按照上面的描述，我们应该声明一个新的类型来表示δRA序列，而P作为一个函数，接受一个类型为δRA的项参数并返回一个类型，因此：类型：类型。|-：struct -> struct -> struct.P：类型。图1中的实际代码通过删除类型构造函数P并（实际上）更改|-从一个术语构造函数到一个类型构造函数。因此，对于结构X和Y，构造X|- Y表示X Y的衍生物。(We这样做只是为了简化打印输出）。第3行将*声明为一元结构运算符。第4行和第7行是注释。在第5行和第6行中，项sA和sS被声明为表示δRA规则的派生的类型（参见[9]），如下所示DAWSON和G或E'96► ∗ ∗→∗ ∗►X∗Y ►X（sA）XYYX（sS）我们可以把这些声明看作是断言这些规则有派生（我们称之为sA和sS），或者把它们定义为现在，将sA和sS（代表“前件中的星”和“后件中的星”）视为函数，每个函数都取一个前件的导数，另一个函数的导数，它们可以对某个给定的函数V组成如下sS的求导U V−→sA的推导V推导∗∗U ►V第8行的ssSAl的定义就是这样做的;符号表示λD.sA（sS D）。Bjref计算ssSAl的类型，给出（S1S2）（S1S2）。注意X、Y、S1和S2是变量（S1和S2是由BMF选择的名称）。在类似于Prolog [5]的方式中，Prolog f允许人们进行查询，例如ssAS1： （X1|-** Y1）->（** X1|-Y1）。其搜索指定类型的项（即，搜索所述规则的推导），并用该术语实例化ssAS1。在这个例子中，因为basef允许替换查询中的X1和Y1以及sA和sS声明中的变量X和Y，所以搜索沿着错误方向的无限分支进行。另一方面，代码%定理ssASl_th：exists {DerivedRule：{S1：struct}{S2：struct}（S1|-** S2）->（** S1|-S2）}true.%prove 2 {}（ssASl_th DerivedRule）.成功地使用了Beself定理证明器来找到推导，返回/ssASl_th/：ssASl_th（[S1：结构][S2：结构]D：S1|-** S2] sA（sS D））。(Here变量S1和S2需要被显式地抽象Besidf的定理证明器没有被广泛记录，据说正在积极开发中，证明搜索组件预计将进行重大更改。证明搜索策略可以由用户控制，只有在有限的范围内，而我们已经发现，相当大的用户控制（使用从证明到证明的策略）通常是必要的，在我们的工作。我们发现，伊莎贝尔的某些方面，我们非常赞赏的是缺席的。Isabelle o拥有大量的用户DAWSON和G或E'97►mands”，以文档化的ML函数的形式，使用户能够编程证明过程，或检查术语或类型表达式的形状。例如，可以编写一个策略，它显式地检查当前的证明状态，然后决定应用几个策略中的哪一个。在Isabelle中有许多用于组合战术的富有表现力的“粘合剂”功能。文档中的不适当之处，或者在选择文档中的函数时，通常可以通过查看源代码来避免，这也可以对用户编程自己的策略有很大的帮助在这个阶段，Zerof似乎没有向用户提供类似的功能。因此，虽然定理证明器确实成功地找到了上面的推导，但我们不确定我们是否可以使用它来找到所有需要的推导，主要是因为缺乏用户对证明的控制3.3双曲正切函数中的截消定理在这一点上，我们应该参考在[19]中描述的使用BMF的割消定理的证明。这使用了一个相当巧妙的序列表示;传统Gentzen矩阵A B的免切证明被表示为类型neg A -> pos B -> @，而它的免切证明被表示为neg A ->pos B -> #，如[19]中所解释的。左下方显示的两个规则都表示为右侧显示的类型，A&A.AB(negA->#）->（阴性（A和B）->#）实际上，第二条规则可以直接用所示的类型表示，但第一条规则可以直接用（negΓ-> pos-> neg A->#）->（negΓ-> pos-> neg（A and B）->#）然而，第一个所示类型的项（函数）的存在平凡地意味着第二个所示类型的项（函数）的存在。进一步构造的类型表示证明到无剪切证明的转换阶段，并且终止检查器检查执行从证明到无剪切证明的整个转换的函数终止。但是，这个终止检查器只检查函数不会永远运行。它不检查它是否终止于一个自由割取的派生-关于割消定理的这项工作是基于一种巧妙的方法以一种适合于Cut f的方式来表示问题;即使如此，从它获得割消定理的证明依赖于基于几何的终止检查器，并且依赖于手动检查，即在“割”之上使用的规则的所有可能情况都已被覆盖。另一方面，换句话说。DAWSON和G或E'98因此，这个割消的证明介于我们之前的工作（我们只是在ML中编程了一个割消函数）和完全形式化的证明之间。3.4Isabelle/CTT的实施然后，我们转向伊莎贝尔的CTT理论，因为它是基于一个逻辑，这是非常相似的，在这方面，它包括依赖类型。我们实现了δRA类似于它的实现，例如，（省略形式的前提？X：str）“sA：*？X|- 你是说.. . Y-->*？Y|- 你是说.. . X”：thm“sA oo sS：？X|-你是谁？Y-->* *？X|- 你是 说 . . . Y”：thm其中oo表示函数组合。编写策略来确定术语的类型（即，确定由给定的规则组合获得的派生规则），通过求解诸如sA oo sS：？t（其中包含类型变量？t）。我们探索了搜索给定类型的术语（即给定术语的证明）的策略，通过解决下面的目标，其中包含术语变量？P.“？P：（X|-** Y）-->（** X|-Y）”。伊莎贝尔的CTT理论并不像其他一些理论那样广泛发展;我们发现有必要证明一些一般但基本的定理。3.5结论我们实验了BMF，因为它已经出现，我们将得到我们的手的证明“免费”，在这一过程中，推导出一个BMF或BMF规则，我们产生一个长期的体现推导进行。考虑到我们打算对割消定理做一个完全机械化的证明（在这个证明中我们广泛地操纵导子），我们认为，BMF的这个特性似乎是有用的。 我们对Isabelle/CTT的研究似乎表明，它可以做与Biferf相同的事情（通过一些扩展来产生适当的派生规则和策略）。然而，我们意识到，尽管我们可以产生一个表示推导的项，并表明构成推导的基本步骤，但我们不能在定理证明器的逻辑以所需的方式分析推导有鉴于此，使用依赖类型理论来实现似乎没有什么好处。我们已经提到了切消定理的一个证明，注意到它是基于一种巧妙的方法，以一种适合于切消定理的方式来表示问题，而且它不是一个完全形式化的证明。由于我们的目标是一个正式的证明，使用的技术，将同样适用于DAWSON和G或E'99其他证明理论的结果，我们觉得这个切割消除证明并不表明依赖类型理论将足够强大，我们的需要。4Isabelle/HOL的实现HOL是基于Church [3]的高阶逻辑和Gordon [8]的HOL系统的Isabelle理论因此，它包括对高阶函数和谓词的量化和抽象。HOL理论使用Isabelle自己的类型系统和函数应用和抽象（也就是说，对象级类型和函数被元级类型和函数识别）。Isabelle/HOL包含函数式编程语言中的构造（如数据类型和let），这极大地方便了在Isabelle/HOL中重新实现程序，然后对其进行推理。然而，限制（例如标准ML本身没有）阻止定义空的类型或不是集合的类型，或者不能终止的函数Isabelle/HOL完全适合δRA的深埋。导致我们得出这个结论的最重要的因素是数据类型声明和相关的原始递归函数定义的便利，这是非常有帮助的。例如，我们对δRA结构表达式（参见[9]）建模如下数据类型structr =逗号结构structr| SemiC结构| 星形结构| Blob结构| 我| E| 结构形式公式| SV字符串前六行对应于δRA的结构算子，下一行用于将最后一行在浅嵌入中没有类似的内容，我们只是使用了一个Isabelle变量，比如？S表示任何δRA-结构。 在深度嵌入中，SV因此，我们现在可以写SV？V，哪个Isabelle将与由单个结构变量组成的结构表达式匹配，或者？S匹配任何结构。我们还定义了函数（在Isabelle/HOL中），这些函数（例如）找到结构表达式中的所有变量，或者用给定的结构替换这样的变量。我们也为第2节中描述的工作编写了这样的函数，但使用的是标准ML，而不是Isabelle。为了描述推导的结构，我们有数据类型pftree =优先级规则（pftree列表）| Unf其中，Pr seq规则pts是Prseq的派生，DAWSON和G或E'100推导使用δRA规则，最后一步的前提是列表pts中推导的结论。 Unf（我们给出的结果表明，我们如何可以推理probability，在这个嵌入的例子。这里IsProvableR rules prems concl是指可以使用rulesrules从sequentsprems中推导出rulesconcl，IsProvable rules rule是指可以使用rules从其前提中推导出rule语句的结论。val IsProvableR_transs =“[|IsProvableR规则prems ' c o n c l ;所有p：prems '。IsProvableR规则前提条件|] ==>IsProvableR rules prems concl”val IsProvableR_deriv =“[|所有规则：规则。IsProvable rules规则;IsProvableR rules' prems concl| [详细]IsProvableR rules prems concl”虽然我们认为相应的结果，对于所涉及的序列和导子的特定实例，可以在BMF中比在Isabelle中更容易地证明，但我们无法看到如何在BMF或Isabelle/CTT中表达一般结果，而不是在这些系统中做深度嵌入，正如下一节所提到的。5进一步工作和相关工作关于δRA的割消定理的证明已经完成，并将在另一篇论文中报道。使用Isabelle/HOL的深度嵌入，我们能够指定和推理可导性和派生树。很明显，Isabelle/HOL逻辑很适合于编写规范，这些规范通过替换给定逻辑演算规则中的变量来描述执行证明的过程。我们将此归因于逻辑的丰富性，不仅包含和积类型，而且包含递归数据库（如在编程语言ML和Haskell中），并且Isabelle/HOL提供了描述每个此类类型的定理因此，它是这个项目的合适选择。正如其中一位裁判所指出的那样，我们最终将δRA嵌入Isabelle/HOL非常深，利用了Isabelle/HOL的递归数据库和其他特性。在尝试各种浅嵌入并发现它们不适合我们的证明理论需要的过程中，我们发现了这种深嵌入的必要性。一个有趣的问题是δRA 的同样深的嵌入是否在Isabelle/Pure，Is-abelle/CTT和Isabelle/CTT中是可行的。我们个人认为这是可能的，DAWSON和G或E'101但是这样的嵌入将是极其复杂和困难的，因为我们将不得不实际上重新实现诸如递归数据库之类的基本特征，而这些基本特征我们的目标是产生一个虽然我们已经做到了这一点（在某种意义上），我们的工作已经阐明了一些进一步的观点。贝尔纳普的显示演算的割消定理是通用的。它适用于所有规则满足一定条件的显示演算。我们对一个特殊的显示演算δRA（关系代数）进行了建模。相应地，我们证明了δRA的割消定理。虽然我们可以识别证明中使用的δRA在Isabelle/HOL中对任意显示演算进行建模将是一个更进一步（也更困难）的活动。6结论我们已经回顾了早期的工作，这些工作描述了将δRA 演算浅嵌入Isabelle/Pure逻辑，并指出了它在Isabelle本身中证明证明理论结果的缺点。基于依赖类型理论的工具将“免费”提供证明的表达能力，我们随后研究了BMF工具。虽然Isabelle/CTT工具仍在积极开发中，但我们注意到Isabelle/CTT中有类似的逻辑，这可以发挥Isabelle的优势，例如可以访问广泛的文档化ML函数进行编程证明策略。然而，我们也发现，虽然Isabelle/CTT和Isabelle/CTT有助于识别一个可导规则或导出规则的推导，但它们并不有助于推理推导的形状，或在其中发现的序列。因此，我们转向Isabelle/HOL，它似乎是深入嵌入演算（如δRA）的最佳工具，并推理我们需要的可导性，推导树和相关的证明理论概念。不用说，这是我们从一开始就从拉里·保尔森那里得到的建议确认我们感谢保罗·杰克逊、兰迪·波拉克和马克·斯台普斯就“浅嵌入”和“深嵌入”的概念进行了许多有益的讨论DAWSON和G或E'102引用[1] 贝尔纳普。显示逻辑。Journal of Philosophical Logic，11：375[2] RJ Boulton，A D Gordon，M J C Gordon，J R Harrison，J Herbert和Jvan Tassel。有在HOL中嵌入硬件描述语言的经验。Proc Intl. Conf. on TheoremProvers in Circuit Design ： Theory ， Practice and Experience ， IFIP Trans.Volume A-10：129-156. North-Holland/Elsevier，1992年。[3] 一座教堂。简单类型论的一个公式。Journal of Symbolic Logic，5：56[4] JD AWson和RGo R'E。一个使用显示逻辑的关系代数系统的机械化实现在JELIA98：人工智能中的逻辑，LNAI 1489：264-278。Springer，1998年。[5] P Deransart，A Ed-Dbali和L Cervoni。Prolog：标准。Springer-Verlag，1996.[6] R A Elmasri和S B Navaldam。数据库系统基础。本杰明/卡明斯，红木城，第2版，1994年。[7] J. H.加利尔计算机科学逻辑：自动定理证明的基础。John Wiley and Sons，1987年。[8] M J C Gordon和T F Melham。介绍HOL：高阶逻辑的定理证明环境。剑桥大学出版社，1993年。[9] 去吧。关系代数上的无割显示演算。CSL 96：计算机科学逻辑，LNCS 1258：198[10] 去吧。基于显示的子结构逻辑。逻辑学杂志的国际集团在纯粹和应用逻辑，6（3）：451-504，1998年[11] R Harper，F Honsell，and G Plotkin.定义逻辑的框架Journal of the ACM，40：143[12] 研发Maddux。关系代数、有限维圆柱代数及其相互关系导论。《代数逻辑》，Colloquia Mathematica Societatis Janos Bolyai，卷54：3611991年北荷兰[13] 马丁-洛夫。直觉主义Ty peTheor y. 1984年出版的《圣经》。[14] 米哈伊洛娃和J·冯·赖特。HOL中一阶证明系统的同构证明在高阶逻辑的定理证明，LNCS 1479：295314. Springer，1998年。[15] 一个米利。确定性程序设计的关系方法Acta Informatica，20：315[16] R米尔纳，M托夫特，R哈珀，和D麦奎因。标准ML的定义（修订版）。MITPress，1997.DAWSON和G或E'103[17] L·C·保尔森。伊莎贝尔参考手册。剑桥大学计算机实验室，1999年。[18] L·C·保尔森。伊莎贝尔计算机实验室。Univ. 剑桥，1999年。[19] F·芬宁。结构性削减消除。第十届国际计算机逻辑年会论文集。Sci. 第156-166页。IEEE Computer Society Press，1995.[20] FPfenning和CS chürmann。系统描述：Twelf-演绎系统的元逻辑In CADE-16 Proc. 16th Intl. Conf. on Automated Deduction ， LNAI 1632 ： 202-206.Springer，1999年。[21] 纳塔拉詹·香卡Metamathematics，Machines，and Goedel剑桥大学出版社，1994年。[22] 海因里希·万辛模态逻辑，逻辑趋势第三卷。Kluwer Academic Publishers，Dordrecht，1998年8月。
