理论计算机科学电子笔记125（2005）53-68www.elsevier.com/locate/entcs经验证的证明-生产决策程序Robert Klapper和Aaron Stump部计算机科学与工程，华盛顿大学在圣路易斯。圣路易斯关闭KY，USA.网址：http://cl.cse.wustl.edu/摘要将决策过程（DP）与其他系统集成的一种广泛使用的技术是让DP发出他们报告有效的公式的证明。出现的一个问题是调试证明生成代码;在标准编程语言中编写代码生成不正确的证明。本文演示了如何证明生产DP可能会在一个编程语言，称为Rogue-Sigma-Pi（RSP），其类型系统，确保证明被正确地操纵。RSP结合了Rogue重写语言和Edinburgh逻辑框架（LF）。类型正确的RSP程序是部分正确的：本质上，任何由类型正确的RSP程序产生的假定LF证明对象都保证在LF中进行类型检查。 本文描述了一个简单的证明生产组合的命题满足性检查和同余闭包实现RSP。保留字：决策过程，证明产生，逻辑框架，同余闭包1介绍决策过程（DP）对于验证和携带证明的代码等应用仍然很有意义[10，11]。它们对于与证明助手的集成也很有价值。将DP和类似工具与其他系统集成的一种广泛使用的技术是让DP发出他们报告有效的公式的证明[7，12]。虽然这在概念上很简单，但证明生产DP所需的额外工程却很重要。一个问题是简单地调试证明生成代码;在标准编程语言中编写代码生成畸形证明或错误定理的证明是非常容易的。本文演示了如何证明生产DP可能会在一个命令式符号编程语言，称为流氓实现，1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.06.06754R. Klapper，A.Stump/Electronic Notes in Theoretical Computer Science 125（2005）53Sigma-Pi（RSP），其类型系统捕获（在编译时）所有这些在证明操作代码中的错误。从逻辑框架中采用的基本思想是，类型系统不仅跟踪某个表达式表示一个证明（具有Pf类型），而且跟踪它表示一个特定定理的证明（具有类型，比如说Pf（PQ））。当一个证明是从子证明中使用一个推论建立的规则，则类型系统可以强制子证明证明推理规则所期望的形式的定理。一个简单的证明生产DP，称为RVC（“流氓有效性验证”），已在RSP中实现，并演示了该方法。RVC结合了一个证明生成命题SAT求解器和一个证明生成同余闭包（CC）算法，以检查具有未解释函数的等式理论中的无量化器公式的有效性。本文的第一部分在抽象层面上介绍了RVC（第2节）。 我们考虑由RVC决定的逻辑，使用的SAT和CC算法，用于组合它们的组合方案，以及证明生产所需的扩展。 本文的第二部分讨论了RVC是如何在RSP中实际实现的（第3节）。我们看到证明生成算法是如何用RSP编写的，以便类型检查在证明操作代码中捕获正确性错误。2RVC的概念本节在算法和逻辑层面介绍RVC。总而言之，RVC决定了等式理论中的无量化器公式和不可解释函数的有效性。它结合了一个非常简单的完整的非子句SAT求解器和在线版本的Downey-Sethi-Tarjan CC算法[8]。SAT和CC的组合是按照[3]中描述的急切方法完成的，其中 CC立即通知SAT断言的文字（这里是方程或等式），然后如果断言的文字集被确定为不一致，则SAT立即被CC通知。证明是使用我们所谓的工具化方法来产生的，在这种方法中，算法只是被工具化，以构建它们在执行时推导出所使用的证明系统是一个希尔伯特式的系统，具有标准的等式公理。2.1语言RVC根据图1中归纳定义的输入语言F来决定公式的有效性。集合T也被定义为从一个签名n建立的一阶项的集合。 我们假设每个函数符号f∈ n有一个固定的元n≥ 0，我们有时用f n表示。为了证明的目的，RVC依赖于核心隐含语言I，归纳定义为R. Klapper，A.Stump/Electronic Notes in Theoretical Computer Science 125（2005）5355F：=T1=T2|€ F|F1和F2|F1<$F2T：= f n（T1，.，Tn）Fig. 1. RVC的输入语言我 ：=T 1 = T 2假I 1 I 2||I1我∧：=I2：=我错了<$（I1<$I2）I1 ∨ I2：=I1I1 ≈ I2：=（I1 I2）（ I2 I1）图二. RVC核心语言图2.图中还显示了F使用的布尔连接词的标准缩写，以及命题等价的标准缩写（这里表示为“”，优先级最低字面量要么是项之间的等式，要么是项的否定。为了证明一个公式P∈ F，我们在本节中考虑它必须证明P从I导出的公式。 为了证明P，它能证明P是假的。这一点将在我们考虑《可吸入悬浮粒子计划》的实施情况（第3节）。2.2证明和有效公式RVC逻辑的有效公式[17，第2章]）。规则是示意性的，使用元变量P和Q作为公式（来自I）和X，Y，Z，等条件。在一些地方，我们使用了图2中的缩写。H=中的证明，我们称之为H=-证明，对于人类来说并不自然，但它们很容易检查。原因是，它们本身并不包含当地的假设。在自然演绎证明系统中，一些证明规则依赖于能够引入新的假设，这些假设只能合法地用于特定的子证明。例如，蕴涵引论的规则说，要证明一个蕴涵P<$Q，必须在P成立的局部假设下证明Q。校对使用局部假设比检查没有它们的证明更复杂，因为证明检查器必须检查局部假设没有在其范围之外使用。相比之下，H=的证明检查器只是从由其直接子证明证明的定理中计算由证明证明的定理，而不需要强制执行任何类型的范围。证明的简单性56R. Klapper，A.Stump/Electronic Notes in Theoretical Computer Science 125（2005）53（K）P（QP）（S）（P（QR））（（PQ）（PR））（DN）<$PPPQP（MP）Q（方程式10）X=X（等式）X=YY=X（Eqtranss）X=YY=ZX=Z（Eqcong）X1=Y1... Xn=Ynf n（X1，.，Xn）= fn（Y1，...，Y n）图三. 证明系统H =检查是一个理想的功能，特别是在像携带证明的代码这样的应用中，其中最小化可信计算基础是一个重要目标[2]。 因此，我们采用H=作为RVC的证明系统，而不是一个自然演绎系统2.3命题有效性检查测试非子句公式的有效性是以一种基于案例分解和简化的标准和非常原子公式（这里是方程）被选择用于情况分裂，我们递归地检查通过分别用TRUE和TRUE替换所选原子公式获得的公式简化的有效性。原子公式以简单的自上而下、从左到右的方式被选择用于大小写拆分。对原子公式赋值所产生的公式的简化由函数repsim（“替换和简化”）执行。该函数递归地简化了直接自下而上的替换后的公式。在递归简化中的每一点，使用辅助函数sim来简化以TRUE或TRUE作为直接子表达式的项。这个简单的方案可以优化，如[4]所示2.4同余闭包RVC实现了Downey-Sethi-Tarjan CC算法的在线版本[8]，我们在续集中将其称为CC。方程式和方程式是-R. Klapper，A.Stump/Electronic Notes in Theoretical Computer Science 125（2005）5357来自T的Tween项可以被断言到该算法。如果断言其中一个导致一组不一致的公式，CC立即报告不一致。CC依赖于用于维护表达式的等价类的公知的并集查找数据结构的实现[6，第22章]）。每个等价类都有一个代表，由find函数返回。union函数接受t1和t2项并合并它们的等价类，使t2如果一个项没有被赋予union或find，它就不被认为属于等价类。我们将联合查找实现称为UF。CC还依赖于以下辅助概念：签名f（t1，.，t n）是f（tJ，.，tJ），其中tJ是CC。对于所有i，代表t i。1n iCC-代表f（t1，.，t，n）是其UF表示（用find获得），如果它在等价类中;或者是其签名表示的UF表示。签名代表t的签名代表是签名为t的等价类中的选定项。如果等价类中没有项具有签名t，则t被视为其自身的签名代表。父列表项t的父列表是在t禁止列表一个项t的禁止列表是一个双等式列表（下面称为禁止），每个双等式在t的等价类中的项u和已经被断言不等于u的某个其他项之间为了断言等式t1=t2，我们将t1的CC- rep合并 为了将x合并到y中，我们对x和y进行合并（使yx的父元素也被添加到全局待定列表的末尾（下面解释）。我们还检查x的禁止（下面解释）。然后x的父列表和禁止列表被设置为空列表。在断言一个等式之后，未决列表被如下处理。第一项t从列表的前面删除，我们断言等式t=tJ，其中tJ是代表t的签名。我们还检查了t的禁止。为了检查项的禁止，我们简单地验证对于每个禁止t/=tJ，t的CC-rep与tJ的CC-rep不相同。如果是的话，已被发现，并报告给呼叫者。 宣布离婚，我们按照刚才的描述检查它，然后将其添加到每一方的禁止列表中58R. Klapper，A.Stump/Electronic Notes in Theoretical Computer Science 125（2005）53关于disequation我们对DST CC算法的主要补充是使用禁止列表来跟踪不平等（在[8]中没有直接处理选择这些是为了支持对CC的字面量的增量断言。特别是，我们把递增地进入CC的新项放入它们从一开始就存在的情况下被断言为相等的形式。2.5结合SAT和CC同余闭包与命题有效性检查器的集成遵循所谓的渴望方法，其中对原子公式的赋值在进行时被断言到决策过程[3]。CC负责立即通知SAT，如果断言的文字的当前集合L1、L2、...，Ln被确定为不一致。如果检测到这种不一致，则关闭有效性检查搜索的当前分支2.6生产证明我们在RVC中进行打样生产的方法基于以下原则和目标。我们在3.4节中看到了我们的实现如何解决这些问题。假设（引理）：我们假设我们有能力从我们的逻辑的原始规则中导出命名引理（图3）。在本文中，引理是H=的一个定理或一个推导的推理规则在前一种情况下，引理由H=证明。 在后者中，它证明的H=证明，另外可以使用假设的推理规则作为假设。假设（策略）：我们假设我们有能力编写可以操纵H=-证明的通用程序（策略我们只在下面的一种情况下使用这个假设，即演绎定理，其证明是只是一个证明转换程序（2.8节）。我们并不认为我们有办法验证战术是否具有终止或案例覆盖等属性。因此，我们并不认为战术总是成功的。目标（常数时间证明）：我们试图确保只有常数时间计算才能构建证明。这是证明生产的工具化方法的重要部分，我们只是试图在我们生产的证明中反映DP执行的演绎R. Klapper，A.Stump/Electronic Notes in Theoretical Computer Science 125（2005）5359A（P<$PJ）A（Q<$QJ）A_∞（P<$Q<$PJ<$QJ）超同余与A（PQ）QRA型（P型R）HypEquivTransA（v）PA（vTRUE）P一个简单的案例Split见图4。 SAT使用的派生规则关于Repsim（vx）（AAJ）关于Repsim（vx）（BBJ）从sim（v）（ABAJBJ）（v<$x）（A<$B<$PJ）（AJ<$BJ）PJ图五. 与案件2.7从SAT函数repsim从公式P和变量v的真值x的赋值中产生一个简化的公式PJ。repsim通过分析输入公式P的结构递归地生成（v<$x）<$（P<$PJ）的证明。例如，假设P<$A<$B。通过递归调用repsim，我们得到了（v<$x）<$（A<$AJ）和（v<$x）<$（B<$BJ）形式的证明，其中AJ和BJ分别表示A和B 我们可以然后使用导出的证明规则HypCongruenceAnd（图4）来产生（v<$x）<$（A<$B<$AJ<$BJ）的证明。此外，通过使用函数sim，它从公式P和P≠PJ的证明中产生简化的公式PJ，我们可以证明AJ<$BJ<$PJ。通过应用派生证明规则HypEquivTrans（图4）我们可以证明（v<$x）<$（A<$B<$PJ），其中PJ是x 赋值给v 的简化公式。公式P 的有效性的证明是通过应用CaseSplit证明规则产生的（见图4）。2.8从CC生成打样我们扩展了CC的高级接口，以如下方式生成证明。如果CC发现某个子集{L1，...，Ln}是不一致的，它产生了一个证明，即L1不一致。中文（简体）60R. Klapper，A.Stump/Electronic Notes in Theoretical Computer Science 125（2005）53D1A1x=fD2A2f=rHypEqtranssA1<$A2<$x=r见图6。 在路径压缩假的。 我们用CC来维护它所推导出的所有中间事实的证明。我们想要保持对像t=tJ这样的事实的证明，其中tJ是t的签名表示。由于这些事实只有在假设由SAT到CC，我们实际上必须保持稍微丰富的信息。 对于由CC存储或计算的每个中间方程t = T，我们保持子集{L1，. ，Ln}的断言的文字从SAT证明方程。 我们也有证据证明L1是... L n我们考虑一个例子。UF数据结构在平衡树中维护等价类。每个词都有一个find指针，指向树的根。树的根用作树所表示的等价类的代表。对项x的查找操作遵循从x到x的树的根r的查找指针然后，它通过更新路径上的所有find指针来压缩从x到r的路径直接指向r。对于每个项x，我们希望保持一个证明，x = f，其中f是x的find指针指向的项。 如前所述，我们实际上必须保持一个证明，即A ≠x = f，其中A是这个事实成立的假设。 在压缩路径时，我们基本上希望使用（Trans）公理（图3）将x = f和f = r的证明（我们通过归纳假设已经建立）与一对（MP）的实例。然而，由于存在假设，我们必须实际构建图6中的证明。D1和D2是我们已经拥有的证明，HypEqtranss是一种推导规则，允许在假设下使用传递性连接等式的证明这里采用的从RVC中的CC生成证明的方法与CVC中遵循的方法不同[13，第5章]。在CVC中，每当SAT向CC这样的子DP断言一个文字时，这个文字必须伴随一个证明（这个文字成立）。这在具有局部假设的证明系统中是合理的，其中SAT求解器可以引入文字保持的局部假设u，并将u提供给CC作为文字的证明。在没有当地假设的情况下，这不能直接进行。真的然而，由于以下原因，在假设下的探测在H=基本元定理：定理1（演绎定理）如果B在如下条件下可能可导，R. Klapper，A.Stump/Electronic Notes in Theoretical Computer Science 125（2005）5361假设A成立，那么公式A→B在没有这个假设的情况下是可导出的。可以在SAT和CC之间的接口处引入局部假设，并利用演绎定理来去除它们。然而，演绎定理的证明是在假设A下，以B的证明的形式通过归纳法进行的。因此，演绎定理在本质上是通过一个程序来证明的，该程序将B的证明转换为BLP-A的证明A的证明B的证明如上所述（第2.6节），我们假设有能力编写这样的程序，但我们并不认为我们可以验证它们的属性。因此，我们实际上需要运行这个程序，确保我们有正确的H=证明。运行演绎定理的证明需要，一般来说，时间与证明的大小成正比，转化.因此，如果我们在运行时运行演绎定理，我们将违反我们的目标（第2.6节），即只花费恒定时间的额外e-检验来构建证明。事实上，必须转换的证明不是RVC实际产生的证明，而是所有引理完全展开的证明（因为演绎定理的证明是通过上面的情况进行的）。H的基本规则=）。根据这些证据的大小和我们的经验-根据演绎定理（见下面的3.4节），我们推测在实践中，在运行时转换证明以消除局部假设是不可行的：性能损失和产生的证明大小的增加将是不可接受的。2.9RVC中的引理使用工具化方法来证明产生式，RVC目前需要52个引理来证明它所做的所有推理。这些引理都是从H=的基本规则导出的。用演绎定理推导引理是最方便的。因为，如上所述，演绎定理的证明本质上是一种不可信的策略，我们坚持证明使用演绎定理的引理可以完全扩展成只由H=和其他引理的本原规则组成的证明（见3.4节）。3RVC在RSP在本节中，我们考虑在Rogue-Sigma-Pi（RSP）编程语言中实现RVC（在前一节中以算法方式介绍）。在RSP中实现RVC的主要结果是RSP的类型检查在编译时验证RVC的证明操作代码是合理的。从本质上讲，RVC制作的所有证明都保证62R. Klapper，A.Stump/Electronic Notes in Theoretical Computer Science 125（2005）53检查，RVC关于H=中可证明性的可靠性因此得到了静态验证。实现中的错误仍然可能导致RVC无法完成。此外，由于运行时错误，像模式匹配失败一样，证明可以用其中的特殊符号来生成。这些校样是无法核实的.因此，RSP提供的保证的确切声明如下：任何不包含错误的证明都保证被检查。RSP基于Rogue，Rogue本身就是重写计算器的一个版本[15，5]。Rogue被用来编写没有证明的决策过程[16]。RSP为Rogue添加了一个强大的类型系统，我们使用它来捕获证明操作中的可靠性错误。RSP本身的开发正在进行中（见[14]）。特别是，实现合理性所需的元理论属性尚未建立。作者们坚信这些财产是有效的，他们希望很快就能建立起来。在此之前，这项工作必须继续进行。然而，RVC本身在RSP中的实现是完整的，在RSP的500行以下。RSP目前有原型工具支持（在Rogue中实现），形式是类型检查器和Rogue的简单编译器。使用这些工具，RVC已经进行了类型检查和编译，并且已经使用它证明了适度大小的示例公式。我们将在本节的其余部分介绍RSP，并展示如何使用它来实现验证的RVC。由于篇幅原因，我们只讨论实现的选定部分。最直接相关的工作是Appel和Festival3.1RSP：基本特性出于本文的目的，RSP可以被认为是一种类似ML的语言，具有一些额外的功能。RSP与ML共享的基本特性是支持基于模式匹配的案例分析和（通用）递归。RSP有模式抽象，它本质上是重写规则L ->R。这些抽象被应用（使用显式的@运算符）作为术语的函数如果模式不匹配，则这种抽象的应用程序的评估结果为“不匹配”。模式抽象可以与确定性选择算子|进行案例分析。 比如说，（a -> b）|c -> d）@ a计算结果为b，而（a -> b）|c -> d）@ cR. Klapper，A.Stump/Electronic Notes in Theoretical Computer Science 125（2005）5363f：Int => Int.g：Int => Int.f2g：Int=> Int.f2g：= f（x）\ x：Int-> g（f2g（x））|x：Int -> x。见图7。 RSP递归函数计算结果为d，（a-> b）|c-> d）@ q评价为。为了在抽象中指示模式变量，RSP使用语法P\D -> M，其中P是模式，D是声明模式变量及其类型的类型上下文，M是抽象的主体比如说（fx x）\x：Int-> x+x是一种模式抽象，将任何形式的表达式（f x x）转换为x+x，其中x是Int（RSP中唯一的内置类型）。为了使它具有良好的类型，我们应该将f声明为对于某个类型A具有类型Int=>Int=> A.A不需要是Int，因为就像普通函数一样，模式抽象的域和范围类型不需要相同。RSP还允许声明简单的ML样式的数据库。为了表示RVC的核心隐含公式（图2），我们声明O为公式的数据类型，然后声明与每个连接词对应的构造函数（具有curried类型）：O：类型。中文（简体）IMP：O=>O=>ORSP通过编写递归方程来支持递归。例如，图7中的程序在表达式的顶部将所有的f为了简化类型检查，RSP目前要求首先声明递归函数的类型。这个例子的确切语法将在下一节中详细说明。3.2表达式属性RSP从Rogue继承的一个非常方便的特性是对表达式属性的支持。这些基本上只是类型化的哈希表，可以由RSP程序员声明例如，在一个没有证明的UF实现中，我们有一个类型为I=>I的属性findp，其中我们将I作为术语的类型我们可以读取64R. Klapper，A.Stump/Electronic Notes in Theoretical Computer Science 125（2005）53我们可以用语法t.findp：= t如果没有为表达式的某个属性设置值，则读取该属性的计算结果为“否”。在DP中，需要将信息与表达式相关联是非常常见的，而在RSP中，属性提供了一种方便直观的方式来实现这一点。上一节中提到的递归方程实际上需要用属性写来实现。因此，图7的示例实际上必须像这样实现，其中我们假设A是某种类型：a：A.f2g：A =>Int=> Int.a.f2g：= f（x）\x：Int-> g（a.f2g（x）） |x：Int -> x。3.3RSP：依赖类型我们现在来看看RSP的关键类型化特性，它支持验证证明操作。假设我们正在ML中实现一个证明生成DP。表示H=-证明的自然方式是作为一个数据类型。 也就是说，我们将有一个数据类型的证明，然后我们将声明对应于每个证明规则的构造函数：Pf：类型。K、S、DN、Eqrefl、Eqsymm、Eqtransm、Eqcong：Pf。MP：Pf => Pf => Pf。例如，一个关于蕴涵的可反性的证明可以写成（MP@（MP@S@K）@K）。但是没有什么可以阻止形成像（MP@Eqrefl@Eqrefl）这样的证明，它不证明任何定理。 我们试图静态地排除的正是这样的病态证明RSP中采用的解决方案是将数据类型Pf细化为数据类型族{Pf（P）|P：O}。 我们对一个双曲线形式的公式P有一个形式Pf（P）。我们之前的意图是Pf将是所有证明。这被证明是太粗糙了，在这个意义上，我们不能限制成员在该数据类型只是证明一个定理的证明。我们的新意图是，精化类型Pf（P）将是证明P的所有证明的数据类型。事实证明，这可以方便地执行。从概念上讲，我们现在为每个构造函数都有一个无限族。比如我们有SP，Q，R：Pf（（P<$ Q<$ R）<$（P<$ Q）<$（P<$ R））KP，Q：Pf（P<$Q<$ P）MPP，Q： Pf（P Q）=> Pf（Q）=> Pf（P）R. Klapper，A.Stump/Electronic Notes in Theoretical Computer Science 125（2005）5365证明了蕴涵的可反性（MPPP P，P P@（MPP（ PP）P@S P，PP， P@K P，P P）@K P， P）我们现在所需要的就是找到一种方法来定义这些无限多个变量。我们通过将每个族看作从下标公式到相应构造函数的函数来简单地实现这一点。 例如，我们将K视为一个函数，它接受P和Q，并返回构造函数KP，Q。然后，它可以添加类型声明，如：S：（P：O=> Q： O=> R： O=>Pf（（P<$ Q<$ R）<$（P<$Q）<$（P <$ R）K：（P：O =>Q：O=> Pf（P<$Q<$ P））MP：（P： O=> Q： O=> Pf（PQ）=> Pf（Q）=> Pf（P））这里使用的技术特性是依赖函数类型，其形式为x：A => B。 这是一个函数的类型，它接受类型A的输入x，并返回依赖于x的类型B的输出。 K接受公式 P和Q，并返回公式（P<$Q<$P）的证明。我们终于可以实际上以类似的方式声明我们的无限证明类型家族：Pf：O=> type。这种用精化数据集表示证明的方法是由Harper，Honsell和Plotkin提出的，并由他们的爱丁堡逻辑框架（LF）[9]实现，这是RSP的一个适当片段RSP还有一个类型构造（不包括在LF中）来支持像RVC这样的应用程序。对于产生证明的代码，子例程产生一个输出和一个证明是很自然的。例如，上述repsim函数接受变量v、布尔值x和公式P，并且给出了一个简化的公式PJ，以及（v<$x）<$（P<$PJ）的证明。RSP使用依赖对来支持这种行为，pairs中的第二个元素的类型取决于pairs中的第一个元素的值。依赖对类型写为x：A，B，依赖对形成为x\M，N，其中x是M在N中的别名。3.4RSP中的缩写和引理RSP支持第2.6节中描述的要求。它有一个引入定义的机制，演绎定理的证明可以是66R. Klapper，A.Stump/Electronic Notes in Theoretical Computer Science 125（2005）53rvc.repsim：（v： O => x： O => p： O =>（q：O，Pf（IMP@（EQUIV@v@x）@（EQUIV@p@q）AND@a@b\（a：O，b：O）->设（r1，（rvc.repsim@v@x@a），设（r2，（rvc.repsim@v@x@b），令（r3，（rvc.sim@（ AND@r1.1@r2.1）），（q\r3.1，HypEquivTrans @（EQUIV @ v @ x）@p@（ AND@r1.1@r2.1）@r3.1@（HypConventionce And @（EQUIV @ v @ x）@a@r1.1@b@r2.1（@r1.2@r2.2）@r3.2））见图8。 repsim的类型声明和示例情况很容易在RSP中编写为证明转换程序。事实上，RSP的类型系统保证了我们一直在考虑的这个实现然而，可以想象（尽管我们认为不是实际的）遗漏了一个角落案例，或者代码在某些情况下可能无法终止。因此，我们不相信我们的演绎定理的实现，而是坚持使用它证明的所有引理都被完全扩展为原始H=-推论。 的完全展开派生的总大小RVC需要的52个词元是370KB。使用演绎定理的33个推导的未扩展形式的总大小为24KB。其他19个推导需要12KB。3.5证明生成SAT我们简单地看一下SAT代码的公式简化部分的证明生成，由rvc.repsim实现。如上所述，该函数负责简化关于布尔值v到变量x的赋值的公式p。它的类型在图8的顶部给出。repsim被声明为返回由输入公式p的简化版本q组成的依赖对，以及证明EQUIV@ v @ ximplysEQUIV@p@q。图的结果示出了对于传递给repsim的公式p具有AND@ a @ b形式的情况的模式ab的牵引。repsim将通过首先递归地对参数a和b调用它- self来分别获得a'和b'，以及I MP @（E Q U I V @ v @ x）@（E Q U I V @ a @ a '）和IMP @（EQUIV @ v @ x）@（EQUIV @ b @ b'）的pr o o fs来生成所需的公式。接下来，通过调用函数sim将新公式q计算为AND@ a' @ b'的简化。sim将返回R. Klapper，A.Stump/Electronic Notes in Theoretical Computer Science 125（2005）5367对于公式q，s的含义是：EQUIV@（AND@aQ.最后，我们可以使用导出的证明规则HypCongruence-And和HypEquivTrans的应用程序来生成IMP @（EQUIV @ v @ x）@（EQUIV @ p @ q）的所需证明。变量r1和r2分别表示在a和b上递归调用repsim的结果。 变量r3是AND @ a投影r1.1和r1.2表示repsim返回的对的第一个（公式）和第二个（证明）元素。类似地，对于r3，其保持简化AND @ a3.6证明的恒定时间开销必须注意的是，RSP中RVC的实现未能实现在某个点上产生证明的恒定时间开销的目标（第2.6节）。 CC可以向SAT报告某个真子集{L1，.，Lk}，由SAT断言的文字集合S是不一致的。当它这样做的时候，产生证明的CC实际上给了SAT一个L1错误的证明... L k应当RSP的类型系统不足以检测到这一点，这并不奇怪{L1，.，L k}是S的子集。因此，RVC包括一段代码来产生一个“胶水证明”，S中公式的合取意味着L1... L k.4结论描述了用RSP语言实现的SAT和CC的组合，称为RVC由于RSP进一步的工作包括一个更复杂的SAT实现，以及将RSP编译为C++而不是Rogue以获得高性能。此外，应该可以用一个只传播验证码的残差来替换产生验证码的代码，这样就可以检测到由于运行时错误而导致验证码进入验证码的情况，而不需要实际产生完整的验证码。致谢：感谢匿名评论者对本文早期版本的有益评论，并感谢AndrewAppel 和 他 的 团 队 ， SergeyBerezin ， IlianoCervesato ， DavidDill ，VijayGanesh，C′esarSanchez，Matteo Slanina和Sriram Sankaranarayanan对本工作的有益反馈。68R. Klapper，A.Stump/Electronic Notes in Theoretical Computer Science 125（2005）53引用[1] A. Appel和A.很好依赖类型保证定理证明器的部分正确性Journal of Functional Programming，14（1）：3[2] A. Appel ， N. Michael ， A. Stump 和 R. 维 尔 加 值 得 信 赖 的 证 据 。 Journal of AutomatedReasoning，Special issue on Proof-Carrying Code，31（3-4），2003.[3] C. Barrett，D. Dill，和A.树桩通过增量翻译到SAT来检查一阶公式的可满足性。2002年第14届计算机辅助验证国际会议[4] C.巴雷特和J. 结合SAT方法与非子句决策启发式。在S. Ranise和C.Tinelli，编辑，Pragmatics of Decision Procedures in Automated Reasoning，2004。[5] H. Cirstea和C.基什内尔重写演算-第一部分。 逻辑杂志的兴趣小组在纯粹和应用逻辑，9：363-399，2001年5月。也可作为技术报告A01-R-203获得，LORIA，Nancy（法国）。[6] T.科门角，澳-地Leiserson，和R.里维斯特 算法导论 麻省理工学院出版社，1992年。[7] E.德普拉涅角Kirchner，H. Kirchner和Q.阮。方程和归纳定理的证明搜索和证明检查。InF.Baader，编辑，自动演绎会议- CADE-19，迈阿密，美国，2003年。[8] 唐尼河Sethi和R.塔扬 常见子表达式问题的变体Journal of the Association for Computing Machinery，27（4）：758[9] R. Harper ， F. Honsell 和 G. 普 洛 特 金 定 义 逻 辑 的 框 架 。 Journal of the Association forComputing Machinery，40（1）：143[10] M. Velev和R.布莱恩特在超标量和VLIW微处理器的形式验证中有效使用布尔可满足性过程。Journal of Symbolic Computation，35（2）：73[11] G. Necula 携 带 证 明 代 码 。第 24 届 ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages，第106-119页[12] G. Necula和P. Lee。在试金石定理证明器中的证明生成。 David McAllester，编辑，第17届自动演绎国际会议，2000年。[13] A. 树 桩 检 查 有 效 性 和 证 明 与 CVC 和 CVC 。 斯 坦 福 大 学 博 士 论 文 ， 可 查 阅 http ：//www.cse.wustl.edu/coststump/。[14] A. 树桩 输入LFMet a-Pr ogr amm i n g。 我在C。徐文，《逻辑框架与元语言》，2004年。[15] A.施通普河Besand，J. Brodman，J. Hseu，and B. 金纳斯利 从流氓到微流氓。重写逻辑与应用国际研讨会，2004年。[16] A. Stump，A. Deivanayagam，S. Kathol，D. Lingelbach和D. Schobel。流氓决策程序。InC.Tinelli和S.Ranise，编辑，第一届自动推理决策过程语用学国际研讨会，2003年。[17] A. Troelstra和H.施维滕贝格基本证明理论剑桥大学出版社，第2版，2000年。
