线性算术决策过程的集成与证明验证

理论计算机科学电子笔记151（2006）3-20www.elsevier.com/locate/entcs线性算术与归纳定理证明托比亚斯·施密特-萨摩亚1FB Informatik，技术 德国凯撒大帝大学摘要为了扩大线性算术的决策过程的范围，必须将它们集成到定理证明器中。成功的方法，例如在NQTHM或ACL2建议一个紧密的集成计划，增加了决策过程与引理有关的用户定义的运营商。 我们提出了一个更紧密的集成提供反馈的状态的决策过程中所涉及的公式有三个原因：第一，提供详细的证明对象的证明检查和存档。第二，分析和改进决策程序与定理证明者第三，调查是否通信的状态失败的证明尝试的人类用户与可理解的标准GUI机制的定理证明可以提高辅助引理的推测。关键词：决策过程，以人为本的定理证明，集成方案，引理推测，线性算术，证明对象1引言与基于启发式搜索策略的定理证明器相比，决策过程在决定其专用域上的公式方面非常有效。但这个领域通常相当小。许多公式正好脱离了决策程序的理论因此，为了克服这些局限性，许多研究人员研究了两种不同的方法至少三十年：第一，在析取域上组合不同的决策程序;第二，将决策程序纳入1Email：schmidt@informatik. 乌尼克湖De1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.11.0204T. Schmidt-Samoa/Electronic Notes in Theoretical Computer Science 151（2006）3启发式定理证明使用扩增。关于第一种方法的研究由Nelson Oppen [17]和Shostak [19]的基础工作发起。在本文中，我们关注的是第二种方法。BoyerMoore [7]将基于Hodes [9]的有理数判定过程（归功于[14]中的Fourier）集成到他们的归纳定理证明器NQTHM[6]中。线性算术是指谓词符号上的泛量化一阶理论，≤、=、/=、≥、>表示数上的序关系，函数符号0、s和+表示常数零、一元后继函数和二进制加法。[2]根据基础领域，这些理论在[10]中被称为Presburger有理算术（PRA），Presburger整数算术（PIA）和Presburger自然算术 我们感兴趣的是一个半决策过程的扩展理论的PNA包含addi- tional谓词或功能符号。这些符号是无法解释的，决策过程，但可能受到定理证明器的约束Hodes程序可作为PRA的判定程序，也可作为PIA和PNA的半判定程序。它检查一组不等式的不满足性。关键思想是“交叉乘和加”[ 7 ]两个不等式来消除一个我们称之为变量消除步骤。变量消去步骤可以限制在不等式中最重的变量。一个固定的良好的秩序。在以前的工作中，不等式存储在决策过程的内部状态中，在[7]中称为线性算术数据库，在[2，3]中称为约束存储如果导出了一个不可满足的（基础）不等式，则原始不等式对有理数、整数和自然数都是不可满足的否则，如果集合在变量消去步骤下是闭的，则原始不等式对有理数是满足的，但对整数或自然数可能是不满足的。如果我们试图在一个适当扩展的理论中证明定理，我们必须使用定理证明者提供的关于扩展的附加事实。这些事实通常以（条件）引理的形式给出如果引理的条件能够被证明是有效的，则引理的结论这些证明可以由判定过程或定理证明器来完成。因此，我们得到了相互依赖性。根据[13]，将线性算术集成到ACL 2中会导致简化器和算术包之间存在四种依赖关系。因此，将线性运算作为一个单独的模块进行集成是否明智值得怀疑。根据[15]，如果引理的结论是方程s=t，则我们称其为重写规则;如果结论是不等式，则我们称其为线性规则[2]为了方便使用，我们还将考虑所有数字的常数符号，−表示减法，·表示与常数相乘（n·x表示包含n乘以x的和）。T. Schmidt-Samoa/Electronic Notes in Theoretical Computer Science 151（2006）35u≤v。重写规则的应用将s的实例替换为t的相同实例。与此相反，线性规则的应用将u≤v的实例添加到决策过程的状态中，以便它可以从新不等式中受益。这种增强机制在[7]中引入如果所需的引理不存在，情况会变得更糟为了自动规范重写规则，已经提出了成功的方法例如[16，8]。但是对于线性规则的自动推测，还没有提出通用的方法。只有非线性算法的方法[12，1]。由于线性规则包含一个估计，因此要推测出既有效又有用的引理比重写规则更困难。在我们看来，引理推测是一项非常有创造性的任务，在大多数情况下必须由人类来完成。但必须尽可能支持这项任务。因此，我们需要一个适当的互动计划，提供人类用户所需的所有信息以前的方法缺乏信息有两个原因：首先，它们没有明确地向用户呈现决策过程相反，信息隐藏在决策过程的内部状态此外，决策过程只删除最重的条款。在本文中，我们提出了一种新的方法，将PNA的决策过程紧密结合到我们的归纳定理证明器QUODLIBET[4]中。我们严格区分了决策过程的逻辑部分和控制部分：决策过程的每一个基本步骤都由一个新的推理规则表示，该推理规则在其应用所产生的子句中明确地提供了决策过程的状态变量消除步骤例如：引入了一个新的文字，它结合了两个不等式，消除了所考虑的变量。局部属性的推理规则保证我们的方法的可靠性它们可以自动应用于以适应的命令式编程语言QML编写的策略。我们的方法提供了以下优点：碎片的决策过程到基本步骤实现的推理规则，为我们提供了详细的证明对象，可以很容易地检查与外部证明检查。它还可以统一和灵活地集成到我们的简化过程中。这使我们能够评估不同的集成方案，这些方案的定义比以前的方法更细它还为我们提供了实施不同策略的机会：集成到简化过程简化使用文献中已知的算法来自动化决策过程并指导增强机制。此外，我们还实现了一个特殊用途的策略leq-var-elim，它执行所有可能的变量消除步骤（但没有其他步骤）。只有当简化过程6T. Schmidt-Samoa/Electronic Notes in Theoretical Computer Science 151（2006）3失败了，我们需要更多的信息来推测辅助线性引理。尽管这种策略可能导致不平等的指数级增长，但在实践中这似乎并不是一个严重的问题首先，我们消除了冗余的不等式。第二，有经验的使用者往往很快就能找到所需的不等式，并专注于较简单的不等式。本文的其余部分组织如下：在第2节中对QUOD LIBET进行了简短的概述之后，我们在第3节中用一个简单的例子说明了增强机制以及我们的新集成方案。我们在第4节中描述了我们的方法，并在第5节中对其进行了评估，重点是其推测新的线性引理的能力。在第6节中的相关工作的调查之后，我们在第7节中总结进一步的工作。第二章归纳定理证明器QuodLibetQuod L ibet [4]是一个基于等式的归纳定理证明器，用于子句一阶逻辑，具有隐式普遍量化变量。它允许自由构造函数上的运算符的部分定义，使用（可能是非终止的）条件方程以及构造函数、析构函数和相互递归。归纳有效性被定义为所谓的数据模型类中的有效性，这些模型不使任何不同的构造函数基础项相等。更准确地说，一个规范spec=（E，E）由一个签名和正/负条件方程E给出。一个签名<$=（S，C，F）由一组排序S、一组自由构造函数C<$F和一组函数符号F组成。给定一组变量V，项的集合Term（F，V）像往常一样定义。 设top（t）是项t的顶层算子。 原子是使用一个预定义的谓词符号来构造的，分别表示相等性（symbol =）、有界性（def）和顺序关系（或≤）。<我们使用一个微积分来证明条款所称的目标在QUOD LIBET。条款{11，.，ln}由析取组合的文字l i组成。3.推理规则将目标简化为一系列新的子目标（可能是空的）。一个证明是由一个证明状态树组成的目标和推理节点。证明状态树的根目标节点由要证明的子句组成。推理节点表示应用于其父节点的推理规则也就是目标节点它的n个子节点（n≥0）也是目标节点，代表推理规则创建的新子目标。证明状态树是关闭的，如果所有的叶子都是推理节点。在这种情况下，根目标节点的子句是归纳有效的，只要这对所应用的引理成立。3更确切地说，子句是一个文字列表。文字的顺序与自动校样控制有关。我们写r来附加子句和r的文字T. Schmidt-Samoa/Electronic Notes in Theoretical Computer Science 151（2006）373一个简单的例子首先，我们用一个简单的例子来说明Hodes例3.1（来自[7]）我们想证明公式（1）自然人。 因此，我们检查它的否定是否令人满意。(1)最大值，最小值（L≤Min≤00而进一步复杂化，引入另一个未解释的函数符号。然后，引理（10）的条件不直接存在于公式（9），但必须通过递归调用定理证明器和决策过程的简化器来缓解在下面的例子中，我们要指出我们的积分方案如何支持扩充机制所需的辅助引理的推测，如果这些引理不存在的话。例3.3我们考虑例3.2中的公式（9）（以子句形式），并想导出引理（10）。 图1以证明状态树的形式说明了我们的推导，根目标节点显示在顶部。我们首先尝试通过调用策略简化来自动证明该子句。这种自动证明尝试首先使用推理规则la-范数对所有文字进行规范化。推理规则使用的文字（或术语）如图1所示。由于tactical simplify使用了简化算法来消除最重的项，所以证明尝试在三个规范化步骤之后失败。调用专用策略leq-var-elim，执行推理规则≤-var-elim的所有变量消除步骤。这将导致最后一个目标节点，其中包含所需的辅助引理作为子公式，在图1中用框架标记。因此，我们得到了一个辅助引理的假设。Q拉范数≤-var-elim≤-var-elim≤-var-elimT. Schmidt-Samoa/Electronic Notes in Theoretical Computer Science 151（2006）394线性算术在本节中，我们将PNA的集成方案简化为归纳定理证明器QUOD LIBET。由于篇幅有限，我们不得不省略许多技术细节。这些可以在[18]中找到相反，我们试图直观地解释我们方法的基础为了保证PNA的一致集成，我们假设一个基本规范规范0，它由一个具有构造函数0和s以及定义的函数符号+，-和 * 的排序Nat组成。构造函数基项si（0）将写作i。定义的函数符号由公理指定：(14){+（x，0）=x}(15){+（x，s（y））=s（+（x，y））}(16){-（x，0）=x}(17){-（0，s（y））=0}(18){-（s（x），s（y））=-（x，y）}(19){*（x，0）=0}(20){*（x，s（y））=+（*（x，y），x）}QUODLIBET因此，语义是明确的。 我们推论PNA的规则基于基本规范的归纳有效引理spec0. 请注意，naturals为spec0提供了一个数据模型。4.1PNA的推理规则PNA的决策过程可以分为以下几个步骤：规范化，变量消除和检查的基础实例。为了整合到QUODLIBET中，我们将第1节中概述的过程转换为使用否定的归纳有效性的半判定过程决策过程的状态直接在目标子句中以推理规则添加的新文字的形式表示 注意，我们只需要为决策过程添加推理规则。扩充机制可以通过已经存在于Quod L ibet中的引理应用机制来实现。4.1.1推理规则la-范数为了支持变量消去步骤，我们必须确定不等式中每个项出现的次数因此，我们定义多项式和归一化不等式。我们假设项是一个固定的、完全的、有充分根据的项序。第四章. 1例（多项式时间序列/Fact或序列/多重复序列/Constant序列）p是多项式，如果p≠c+ni=1 c i t i并且对于所有i，j∈ {1，.，n}：c，ci∈ N，c i/= 0，t i∈Term（F，V），top（t i）/=+andt i

下载后可阅读完整内容，剩余1页未读，立即下载