交互式定理证明系统中的任务级别和断言应用

理论计算机科学电子笔记103（2004）161-181www.elsevier.com/locate/entcs带任务的M. Hubner1S. Autexie r2 C. Benzmüller2A. 美娥R21Max-Planck-InstitutfuürInforrmatikStuhlsatzenhausweg 8566123Saarbručken，Germany2萨尔大学计算机科学系，dFKISaarbrücken，66041Saarbruücken，Germany摘要数学的交互式定理证明系统要求用户界面允许尽可能自然然而，这种相互作用往往是有限的，大多数定理证明系统的基础传统演算。这对于断言的应用和证明状态的直观呈现在本文中，我们展示了如何一个更灵活的用户交互可以实现时，传统的演算的经典逻辑被取代的限制较少的推理引擎，最近开发的CORE[2]系统。我们描述了构建在CORE系统之上的任务级别，并将指向证明方法[5]与用于应用断言的灵活机制相结合，该机制避免了从断言的语法形式中分解和我们演示了如何证明步骤，是难以实现在其他系统中，如前向应用程序的断言，是很自然的底层CORE系统的支持，因此是直接实现在任务级别。关键词：交互式定理证明，任务，指向证明，断言应用1介绍交互式定理证明器（ITP）被用于各种领域，从形式化方法的证明助手到数学辅导的数学辅助系统。ITP在这些领域的成功应用需要支持面向人类的推理风格。因此，大多数ITP都基于自然演绎（ND）或微积分（SK）推理引擎1 电子邮件地址：huebner@mpi-sb.mpg.de2电子邮件：chris@ags.uni-s b.d e，{a ute xi er|a me ie r}@ df ki. De1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.021162M. Hübner等人理论计算机科学电子笔记103（2004）161其比为自动推理开发的演算更好地匹配人类推理风格（例如，决议原则）。然而，由于这些演算是为了证明理论的目的而发明的，因此基于这些演算的交互式证明框架仍然存在许多交互式定理证明中两个特别突出的问题是证明的表示和断言的应用当我们看一个样本微积分证明时，这些问题立即变得明显（图10）。①的人）。我们可以看到，原来的目标公式变成了PQ，Q R，PPP Q，Q R，P， QQPQ，Q R，PQP Q，Q R，P，RRPQ，Q R，PRPQ，QRPR（PQ）（QR）PR► （PQ）（QR）PRFig. 1. 微积分证明。在整个证明中分解，这使得证明呈现困难。出于同样的原因，很难以直观的方式支持断言（表达式左侧的公式）的应用。特别是，断言的应用取决于其语法结构。例如，应用PQ和<$PQ所需的步骤在微积分中是不同的，尽管PQ和<$PQ在逻辑上是等价的。当在ND演算中构造证明时，也会出现类似的问题。为了改善用户与依赖于SK或ND演算的系统的交互，进行了许多工作，以更用户友好的方式呈现证明，并尽可能地向用户隐藏演算Bornat [6]描述了一个系统，在该系统中，线性化版本的递归证明以框和线的形式呈现给用户。证明步骤可以在Box-Line级别表示，然后映射到SK规则应用程序的序列中。然而，在这种方法中，底层SK的缺点表现在证据呈现的水平上例如，为了使用户能够执行向前的步骤，必须通过应用切割规则3将每个这样的步骤费力地映射到SK演算中。Bertot等人[5]的指向证明方法也试图隐藏从用户的SK的不便。它们使用一组带注释的SK规则，使用户能够选择一个子公式。 系统然后 能够通过自动应用适当的[3]在Bornat的系统中，削减是由一种策略引入的。M. Hübner等人理论计算机科学电子笔记103（2004）161163SK规则。但是，在这种方法中，操作子公式仍然需要分解整个公式。可以看出，上述方法中的用户交互受到它们所基于的演算的在本文中，我们将展示如何更灵活的用户交互时，可以实现基本的ND或SK演算被替换为一个限制较少的推理引擎。我们使用最近开发的CORE[2]系统作为逻辑基础。CORE已经支持上下文重写证明风格的断言级别的灵活推理.在本文中，我们开发了一个通信层，所谓的任务层，在系统之上。这一层利用CORE在应用断言方面的优势，并为证明的结构化提供了额外的机制。任务层由一个引用子目标的数据结构和一组在此数据结构上定义的推理规则组成。此外，该层提供了一个证明数据结构，它代表了证明历史。任务级别用作各种证明构造组件（例如，交互式用户或自动证明过程）如Mega数学辅助系统[17]的证明规划器MULTI[14]）和CORE系统。这个通用接口使我们能够交错自动化和交互式的证明规划。例如，当前不活动的子问题可以由自动化证明规划器处理，而规划方法也可用于试图关闭活动子目标的交互式用户4这里我们关注任务层的用户交互方面我们表明任务层的用户交互与Box-Line方法或[15]的焦点窗口有关，但也为断言的应用提供了统一的机制，该机制从逻辑细节（如断言的语法形式）中抽象出来。本文件的结构如下。在第二章中，我们首先简要介绍了CORE系统，然后描述了任务层。二、秒4展示了任务层在实践中的使用方式。2核心系统CORE系统的主要特征是构造证明的上下文重写技术。这意味着系统能够确定目标公式G[F]内部的子公式F的逻辑上下文。然后，逻辑上下文产生了许多替换规则，[4]这在独立子目标的情况下很容易，即子目标不共享变量。 如何处理共享变量的子目标问题仍然是一个开放的研究问题。164M. Hübner等人理论计算机科学电子笔记103（2004）161→可以用来将公式F改写为某个公式FJ，从而产生新的目标G[FJ]。通过使用上下文重写技术，该系统支持一种自然的推理方式，其中公式分解被隐式处理，并且在断言级上可操作化Huang我们用下面的定理来说明这一点（也见图1）：(1)（PQ）（QR）（PR）在CORE中，我们可以在最右边的R的上下文中使用蕴涵Q<$R（在（1）中加下划线）来用Q代替R。 这是在从相应蕴涵生成的替换规则R Q >的帮助下实现的。将这个替换规则应用于R，从而得到(2)（PQ）（QR）（PQ）以类似的方式，可以通过应用替换规则Q→

将新获得的Q重写为P，该替换规则由Q的上下文中的蕴涵（P<$Q）来证明。因此，我们有(3)（PQ）（QR）（PP）核心简化为真实。这个小例子说明了CORE的关键特性：通过在子公式的上下文中从断言生成替换规则，可以在断言级别进行推理。此外，证明问题总是以其整体来表示和维护，而不是像自然演绎式演算那样分解为更小的部分。2.1技术说明CORE演算的关键技术是将公式视为树，并使用证明理论信息注释每个子树。证明理论信息是Smullyan [19]引入的极性和统一类型：直观地说，如果公式是目标，则公式的极性是正的，即。在某些序列式演算中，它出现在一个连续的连续项中，而在其他情况下，它是负的。结果，我们得到了有符号的公式。类型可以分配给有符号公式，α代表析取公式，β代表合取公式，γ代表泛量化公式，δ代表具有特征变量条件的存在量化公式。例如，用上标表示极性，用下标表示统一类型，（注： P（x）<$Q（x）<$Qy。 Q（y）<$R（y））<$<$z. P（z）R（z）M. Hübner等人理论计算机科学电子笔记103（2004）161165γ−⇒++αα⟨⟩α γα是规范注释如下：(((你好 （P（x）+<$Q（x）−）−β）−γ <$（<$y. （Q（y）+<$R（y）−）−β）−δ）α−（四）（（P（z）−<$R（z）+把这个公式看作一棵树，我们得到：+α∧−α你好+的你好−γ⇒−β很好−δ⇒β+αP（z）− R（z）+P（x）+ Q（x）−Q（y）+ R（y）−我们将此表示表示为索引公式树（IFT），并观察到它表示矩阵演算中的证明状态[21]。因此，我们可以重用这些演算中的规则来构造矩阵证明。特别是，它为我们提供了一个有效的表示变量依赖。为了启用断言级推理风格，我们首先从这样的（初始）IFT导出自由变量表示，我们用自由变量索引公式树（FVIFT）表示以获得：⇒−β∧−α⇒α⇒−βP（Z）— ⇒αR（Z）+P（X）+ Q（X）− Q（y）+ R（y）−因此，如果变量在IFT中的γ型位置上被约束，则我们用大写字母引入变量，而对于来自δ型位置的变量，则用小写字母引入变量。断言风格的推理是通过利用保留的极性和统一类型来实现的，如下所示：• 首先，统一类型允许静态地确定任何子公式的逻辑上下文对此的充分判据是包含两个子公式的最小子树是一致类型α，即它们是α-相关的。你比如说有符号子公式（P（Z）−<$R（Z）+）+和R（y）−是α相关的，顶级连接词+。• 对于逻辑上下文中的每个子公式，可以通过（1）固定规则的左侧以及（2）通过收集所有β相关子公式来确定子目标来导出使该公式的可能应用可操作的所有规则。 例如，将R（y）−固定为规则的左侧，β相关公式形成单例列表Q（y）+，我们将其表示为R（y）− −→ <$Q（y）+<$⇒166M. Hübner等人理论计算机科学电子笔记103（2004）161联系我们−→ ⟨⟩注意，我们同意将至少有一个β相关子树的事件表示为依赖事件。上述所谓的替换规则编码了这样一个事实，即我们可以用Q（y）+替换R（y）−的归结伙伴的出现。 这允许例如通过应用替换{y/Z}来将该规则应用于出现R（Z）+，以将整个FVIFT重写为+α⇒−β∧−α⇒−β+αP（y）Q（y）P（X）+ Q（X）− Q（y）+ R（y）−注意，我们使用原始的IFT，以便使用为此目的而开发的矩阵演算技术来检查替换的可接受性。形式上，替换规则的这种解析样式概念定义如下5：定义2.1（可接受的归结替换规则）设R0，R是某个F vift中的节点。 然后R0R1，... ，Rn是R的可容许归结替换规则，当且仅当(i)R0和R具有相反的极性并且通过节点cα相关，(ii) 和（R1，..，Rn）是与R0相关的低于c和β的子树. Q简而言之，CORE演算依赖于证明状态，该证明状态由表示量化器和替换依赖关系的IFT和FVIFT组成，F VIFT是一种由替换规则应用程序主动操纵的工作副本。阳离子。演算由12个规则组成，包括一个切割规则，将证明状态转换为一个派生的证明状态。一个证明状态被证明，如果FVIFT是一个命题平凡有效的公式，例如，真的。 该计算器是一个完整的计算器，可用于各种逻辑。到目前为止，CORE提供的框架是证明的完整状态总是表示为单个公式，这是设计目标之一。该系统可以将推理过程集中在任意子公式上，而无需实际执行分解的公式，即FVIFT。为此，我们增加了在任意子公式上引入窗口的可能性，这些子公式是显式表示的焦点。例如，在上面的示例中，没有窗口，完整的公式是可见的，即。推理过程的重点是整个[5]替换规则的一般概念包括对原始相等和等价的处理，从而产生所谓的重写替换规则。 但对于本文的目的是解决风格替换规则是足够的。欲了解更多细节，请感兴趣的读者参阅[2]。⇒M. Hübner等人理论计算机科学电子笔记103（2004）161167⇒⇒−β+αP（Z）−⇒−β⇒+ββαα式（P（X）+<$Q（X）−）−<$（Q（y）+<$R（y）−）−α<$（P（Z）−<$R（Z）+为了支持集中推理过程，我们对FVIFT的节点进行了注释。例如，在Windows−βP（X）+ Q（X）−∧−αQ（y）++αR（y）−窗口的内容是包含在以窗口所表示的节点为根的子树中的（有符号的）子公式例如，窗口是R（Z）+，并且是（P（X）+<$Q（X）−）−β。请注意，我们允许窗口出现在其他窗口下面。下面没有更多窗口的窗口称为活动窗口。聚焦的直觉是，活动窗口的内容是那些可以由规则应用程序操纵。为此，将纯CORE演算扩展到具有窗口的FVIFT，以获得类似于窗口推理的推理机制[16]。2.2使用CORE进行交互式定理证明在CORE中，用户当前使用窗口推断机制。这意味着当他在交互模式下调用CORE时，目标G与公理Ax1，.，Ax n，它为公式（Ax1，... Axn并为它创建一个FVIFT以及G上的初始窗口，呈现给用户。然后，可以通过应用CORE演算规则的窗口版本来更改此窗口的内容。通常，这将是替换规则的应用因此，CORE中的证明搜索是主要有两种选择：(i) 焦点选择：在活动窗口中选择用户希望将证明搜索集中(ii) 规则选择：选择替换规则。由于CORE在断言应用中的优势，它非常适合于交互式证明构造。然而，对焦点和规则选择的最佳支持仍然具有挑战性。一个挑战与规则选择有关，因为公式的上下文目前仅作为通常较长且非结构化的替换规则列表可用。更糟糕的是，即使是相当微不足道的问题，也已经有几十个替换规则。具体而言，可以从子树R（ZR（Z⇒168M. Hübner等人理论计算机科学电子笔记103（2004）161在树中的节点数是指数的。 虽然这是CORE在自动和半自动检验构造过程中必须控制这种可伸缩性。自动证明搜索的另一个困难是焦点的选择。因为证明的焦点可以任意改变，所以很难以系统的和目标导向的方式搜索证明。在下面的部分中，我们将描述支持用户构建证明的任务层。3任务- 组织证明搜索FVIFTs在Sec. 2同时表示证明状态的然而，虽然可以使用窗口推理机制突出显示各个子目标此外，在证明过程中，FVIFT可以显著增长，这使得证明状态的呈现变得困难。因此，将证明状态作为一组子目标（任务）呈现给用户，同时保持由证明状态被表示为单个公式的事实所产生的优点这就是我们的任务层所解决的问题。在这一层，我们使用窗口结构来引用并行在一个FVIFT中的子目标。这些子目标（任务）在任务层构建证明，其中提供了额外的规则来操作这些子目标。将任务级的推理步骤映射到CORE系统中的推理步骤，从而自动保证合理性。为了描述任务层，我们继续如下。首先，我们给出了任务数据结构的形式化定义。然后，我们提供了一组实现的任务操作规则。由这些规则实现的推理包括复合公式的简单分解、复合步骤（如断言的应用）和面向人的步骤（如引理引入）。3.1任务直观地说，一个任务表示一个子目标以及所有可以用来导出这个子目标的公式（断言）（所有与子目标α因此，任务被定义为所有在同一上下文中出现的窗口的列表。然而，在我们使这种直觉形式化之前，我们将依赖发生的概念转移到窗口。定义3.1（条件窗口）设w是子公式F上的窗口在FVIFTR.我们说窗口w在Ri中是有条件的，M. Hübner等人理论计算机科学电子笔记103（2004）161169►+∈联系我们F依赖于R。 否则我们称w在 R中是无条件的。定 义 3.2 （ 任 务 ） 设 R 为 当 前 证 明 状 态 的 FVIFT 。任 务 T 是 一 组 窗 口T=w1，. ..，w n.此外，我们还要求以下条件成立：如果RJ是R中包含T中所有窗口的最小子树：(i) 由W 1表示的子树，.，w n彼此α相关，(ii) T的所有支持窗口在RJ中是无条件的。我们区分目标和支持窗口，以明确表示任务中的注意力焦点。然而，从技术上讲，支持窗口和目标窗口之间没有区别。特别地，由于在CORE中明确地保存了关于每个公式的极性的信息，因此可以自由地交换任务的窗口。因此，任务操作（见第二节中的转移规则）。3.2）可以交换一个任务的目标窗口。 这是 一个显着的差异，以微积分，其中公式出现的左和右的不能自由交换，必须区别对待。特别地，任务a，apDaq不一定对应于微积分中的初始a，因为aJs可能具有相同的极性(i.e.p=q）。在任务中禁止条件支持窗口的决定也是由我们设想的交互式推理驱动的。支持获胜的内容将作为可用于在任务的目标窗口中导出公式如果支持窗口的内容与位于相应窗口之外的子树β相关，则这些树将自动成为从该窗口生成的任何替换规则的条件（与定义2.1相比）。也就是说，与β相关的子树将代表隐含的“知识”，这将以新的证明义务的形式引入。 我们假设， 不太适合于交互式证明构造，因为它将导致其起源对于用户来说不是直接明显的因为任务基本上是子目标的表示，我们接下来定义任务何时关闭。定义3.3（Closed task）如果存在一个w，则任务G是关闭的ΣG其中，w表示一个给定的子树;也就是说，w是True+或假−。从公理Ax1导出目标G的初始问题，. ，Ax n在系统中表示为符号公式（Ax1∈. AxnG）。相应的初始任务由G的目标窗口和每个公理的支持窗口组成：170M. Hübner等人理论计算机科学电子笔记103（2004）161定义3.4（初始任务）设G是一个公式，Ax1，.，Ax n公式，表示G应该从中导出的公理。设R是F VIFT，对于（Ax1，…n ∈Ax n∈αG）+，w i是Ax i上的窗口，g是G上的窗口，则w1，.，w nDg是G的初始任务。但是，当呈现任务时，我们不会区分任务中的窗口和它包含的公式。例如，如果不是W1，...在上面的定义中，我们将写Ax1，.，Ax nDG.63.2任务操作规则任务描述了在证明过程中必须实现的目标。当前任务存储在所谓的议程中。证明过程从只包含初始任务的议程开始。我们可以通过应用任务操作规则将议程上的任务细化为更简单的任务。当议程中的所有任务都被关闭时，证明过程终止任务操作规则可以从执行简单逻辑操作的低级基本规则到复杂规则和推测规则而变化在下文中，我们将给出三种不同类型的任务操作规则及其在CORE中的实现的示例：（1）将连接目标的任务拆分为子任务或分解分离目标的简单规则（第二节）。3.2.1）。（2）通过替换规则和规则应用断言的复杂规则，其提供类似于通过指向方法证明的功能（第3.2.2）。(3)推测性规则，如引理引入（Cut），可用于更紧密地模拟人类推理步骤（Sec. 3.2.3）。事实上，这些规则是由Benzmülleretal的数据来确定的。[4]对本科生如何进行朴素集合论领域的证明进行了研究。虽然这些数据到目前为止只分析了语言现象，新兴的证明模式的初步分析表明，学生经常应用引理，没有明确表示的上下文中，但可以在几个步骤中从现有的假设。3.2.1分解规则图3.2.1显示了使用复合目标公式进行任务分解的规则。这些规则类似于ND和SK演算的通常规则然而，通过利用公式的α-和β-注释，我们可以以紧凑的方式表示规则。为了区分SK规则和任务操作规则，我们以自顶向下的方式给出规则。 也就是说，[6]然而，我们可以遇到形式为A，Ap，ApDG的任务。虽然两个Ap在语法上是相同的公式，但它们是不同的实体，因为它们出现在不同的窗口中。M. Hübner等人理论计算机科学电子笔记103（2004）161171⇒ΔDα（ApA，BpB）p，BpBDApAαLΔDα（ApA，BpB）pApADBpBαRDα（A−p）pA−pα¬βDβ（ApA，BpB）pDApAA−DB+优惠D议事规则如下：议程项目线以下的任务取代议程项目线以上的任务。图二. 任务的基本分解规则我们区分了具有合取目标窗口（β型）的任务和具有析取目标窗口（α型）的任务。α-分解析取目标窗口可以用规则αR、αL和α<$分解，其中规则αR对应于ND演算中的E重要的是（至少对于α规则）任务级的分解在CORE中通过改变相应的FVIFT的窗口结构来模拟。更准确地说，在CORE中通过在ApA和BpB上打开新的子窗口来模拟公式α（ApA，BpB）的分解。 在αR规则的情况下，ApA上的新窗口被添加到相应任务的支持窗口中，而BpB替换目标窗口。另相应地实现了α-分解规则。这样做的好处是可以很容易地撤消分解步骤（参见FocusClose规则）。β-分解β-分解规则将具有合取目标公式β（ApA，BpB）的任务分别约简为目标ApA和BpB的新子任务。然而，将β-分解规则的应用映射到CORE系统中需要比α-分解的情况多一点的扩展原因是根据定义3.2，任务中必须没有条件支持获胜。因此，如果β-规则将被映射到类似于α-分解规则的CORE-系统中，则由该规则引入的任务的目标窗口将是有条件的，因此，将不允许将Shift-规则应用于这些任务以改变目标窗口。为了避免这些限制，当应用β规则时，β（ApA，BpB）中的公式ApA和BpB这可以通过分割目标公式β（G1，G2）来完成，同时保留其周围的上下文我们可以通过应用以下形式的规则来实现这一点172M. Hübner等人理论计算机科学电子笔记103（2004）161⇔ ⇒⇒[ApA]1D A pA ，D.G. nFocusDG GJ=P arent（G）DGJ子窗口（GJ）=焦点关闭A，GDFDG移位当r∈{True+，False−}时，∅DiIDv1. IDvn应用（i→< v，.，v>）1n图三.断言应用和聚焦规则。[18]和[2]中描述的β（β（A，B））→β（β（A），β（B））。Autexier[2]证明了这种Schütte规则在CORE演算中是可接受的。正等价扩展最后，我们引入了一个规则惠来扩展等价A的定义成B和B对于目标窗口包含正等价公式3.2.2断言的应用与指针与上一节介绍的规则相反，我们接下来将介绍操作规则，这些规则将任务层的推理扩展到ND和SK演算的通常范围之外。图3显示了五条规则，这些规则带焦点的规则Focus结合了Sec中的分解规则。第3.2.1条。通过应用焦点，用户可以直接关注目标窗口G内的特定子公式Ap。在FVIFT中，出现在所选子公式Ap和的根G[Ap]之间的路径上的节点的统一类型。目标窗口唯一地定义了一系列分解步骤，为了在单个步骤中获得作为目标窗口的所选公式，需要应用这些分解步骤。 焦点规则执行这些分解步骤，跟踪子目标101 D G1，. ，n ∈D G n，当β-进行分解。 从本质上讲，这是一个指向的想法，M. Hübner等人理论计算机科学电子笔记103（2004）161173联系我们它通过Focus规则集成到任务层中。 我们称之为焦点规则是宏规则，因为它应用一系列基本分解规则。焦点关闭FocusClose规则是由α，β和Focus规则描述的分解的逆规则它关闭了目标公式上的窗口，同时关闭了G的父项之下的所有其他焦点。因此，分解步骤可以一个接一个地撤消。使用Apply为了在任务层应用替换规则，我们引入了Apply-rule。这个想法是为了应用一个断言（即支持窗口中的公式），用户只需要在用户界面上点击一个断言来选择它。然后，系统创建一个由该断言证明的所有替换规则的列表。如果只有一个唯一的适用规则，它将通过Apply-rule自动应用。在更可能的情况下，存在多于一个适用的规则，用户必须选择描述断言的适当应用方向的替换规则。在这一点上，系统将用于缩小用户的选择范围Hübner[10]描述了如何通过基于代理的建议机制来支持一个基于代理的建议规则的选择，该建议机制到目前为止仅与大型[17]定理证明系统结合使用。7使用Close如果任务已关闭，则会将其从议程中删除。这是通过关闭规则完成的，其中从议程中删除了一个如True+，False−的任何标签。使用Shift移动任务的目标Shift规则改变任务的目标窗口.这一点特别重要，因为其他操作规则仅适用于任务的目标窗口例如，考虑一个具有公式Ap的窗口和一个具有（A惠B）− 的窗口是目标G的支持窗口;也就是说，A p，（A惠B）−，ApDG。[7]请注意，在这里定义Apply规则的方式中，它只能应用于目标窗口中最上面的出现i，而不能应用于i的子公式。 然而，这没有问题，因为我们总是可以使用规则Focusfirst来关注子公式。174M. Hübner等人理论计算机科学电子笔记103（2004）161DHGpD.GA−DGA+LemF W公司简介A−DG，A+DG见图4。断言应用和聚焦规则。注意，我们用Schütte规则实现了β-D坐标。因此，我们可以确保目标窗口总是无条件的，这是上述移位规则定义的先决条件。3.2.3推测性证明步骤引入新的引理或情况分裂是推测性的证明步骤，通常对完成证明至关重要。毫不奇怪，这些步骤在自动化和交互式的定理证明中也起着重要的作用。在自动化定理证明中，推理步骤的应用很难控制，它们打开了潘多拉的盒子（可能的引理和情况分裂是先验的，不受限制）。Bundy和Ireland [12]以及Meier [14]描述了在自动证明过程中利用失败来指导引理和案例分割的引入为了能够在任务级对这种推理进行建模，我们通过图中所示的规则LemFW、LemBW和Case来增强推理规则。四、LemFW规则对应于引理的前向应用，并将目标公式G替换为另一公式H。然后，这导致生成一个额外的任务，该任务编码了表明替换所描述的证明步骤实际上是有效的义务。相关的LemBW规则允许将新的引理A插入到任务的支持中，然后可以通过Apply规则应用该任务。Case规则将目标为G的任务简化为两个目标为G的新任务。其中一个新任务具有新的支持窗口A-，而另一个新任务具有支持窗口A+。3.2.4任务和演示文稿到目前为止，我们已经描述了可以在任务层执行的推理。这些推理使CORE在CORE之上发明任务层的另一个动机是证明表示。通过任务提供的证明实际上，使用M. Hübner等人理论计算机科学电子笔记103（2004）161175¬∨任务，我们可以在框线表示中显示子目标，这在ND演算的介绍中是众所周知的（例如，参见[11]），Piroi和Buchberger [15]也建议将其作为交互式证明的适当可视化。在框线表示法中，目标公式在可用断言的下方呈现4）.我们在用户界面中实现这种呈现风格，在目标窗口之上呈现任务这有助于断言的应用，可以通过使用Apply规则以统一的方式应用断言。Box-Line表示使用户能够通过单击相应的支持窗口来应用断言。然后，可以在Apply规则的帮助下应用与断言的适当应用方向相对应的替换规则。4任务-工作示例在本节中，我们将在任务层证明图1这使我们能够说明用户和系统之间的通信，以及比较我们的方法Bornat和Bertot8。 我们使用一个语法上不同，但逻辑上等价的公式来指出我们的方法的优点。我们证明问题的初始任务是：“#（一）+（（P<$Q）<$（<$Q<$R）<$（P<$R））应用焦点来提取最右边的R会导致以下情况：（二）264（P<$Q）−（<$Q<$R）−P−375R+然后，我们可以通过应用断言（Q R）来反向推理，将规则应用于目标窗口。在内部，Apply通过将替换规则（R+→）应用于目标来执行此证明步骤。类似地，我们可以通过应用断言（PQ）-（即，替换规则（P−→））到支持P−。的应用[8]更详细的例子我们可以参考[10]。176M. Hübner等人理论计算机科学电子笔记103（2004）161⇒→⇒ ¬∨向后的步骤导致任务：（三）（P<$Q）−（<$Q<$R）−P−R+Q+类似地，我们可以通过将断言（P Q）-应用于任务的目标窗口来继续向后推理，或者通过将相同的断言应用于支持P-来向前推理。这一次，我们决定支持向前的步骤，我们通过前面提到的Apply规则和替换规则（）的应用在任务级实现向前的步骤。 由此产生的任务是（四）（P<$Q）−（<$Q<$R）−P−R+Q−Q+这可以通过将具有替换规则（Q+→）的应用规则应用于目标来关闭。讨论通过在CORE系统之上构建任务层，这两个概念相互受益。任务允许以面向用户的方式（框和线）来构造和显示CORE证明状态，而底层CORE系统允许在任务级进行灵活的推理。这种灵活性体现在通过指向方法证明与断言应用的统一机制的集成中。这两个概念都可以在任务层得到改进。断言的前向和后向应用可以在任务层自然地执行，并且不必映射到一系列切割步骤中。此外，在任务层，断言可以独立于其语法结构来应用。通过查看示例证明，可以看出应用P Q和Q R所需的相互作用是相同的。在纯SK和ND演算中，相应的步骤将是这两种说法是不同的。用 户 交 互 以 及 我 们 在 这 里 呈 现 的 用 户 界 面 上 的 任 务 呈 现 类 似 于TkWinHOL系统（[13]）。然而，在底层的推理系统的方法不同。而TkWinHOL系统是建立在Grundy [ 8 ]的窗口推理系统之上的在该系统中45263726467375M. Hübner等人理论计算机科学电子笔记103（2004）161177对活动窗口的内容的重写步骤导致需要随后处理的局部引理。这也适用于Robinson和Staples的窗口推断方法[16]。在CORE系统中，这里介绍的任务层的基础上，通过应用替换规则实现的转换保证是合理的，因此不会引入新的子目标。5结论与未来工作我们已经介绍了CORE系统的任务层，并描述了这一层的含义交互式证明建设。我们能够指出任务层如何帮助构建和显示CORE证明。此外，通过利用CORE系统的上下文推理范式，我们能够在单个交互层中组合和扩展现有的概念，如通过指向方法的证明。在本文中，我们给出了一个自下而上的任务层作为核心接口的描述。这种自底向上的方法，以丰富逻辑层的更抽象的层次推理工具是标准的方法，在许多证明助手，以支持抽象层次的证明发展。然而，自底向上方法的一个缺点是，它通常会导致抽象层对逻辑层的不必要因此，我们实际上开发的任务层尽可能独立于底层逻辑层，这样，在理想情况下，逻辑层变得可交换。然而，我们并不建议缺乏合理逻辑基础的证明助手。相反，我们的目标是更好地区分抽象层次的推理和扩展到逻辑层的可验证证明。在任务层，我们感兴趣的是允许面向知识的、直观的证明开发步骤。因此，任务层将通过进一步的任务操纵算子来丰富，这些算子可以是特定于领域的，并且必须在知识工程过程中获得和设计，如从战术定理证明和证明规划中已知的。或者，人类可以通过声明性地描述任务到后续任务的细化来体现操作员的角色;这样的预言步骤适应了[17]中介绍的交互式岛证明的思想因此，具体可用的任务操纵操作符可以不同于相当 构建在逻辑层之上的传统策略）到高度“不安全”的策略（那些具有非尖锐应用约束的策略导致频繁失败的逻辑层扩展，例如，人类建造的甲骨文步骤）。然而，为了将任务级证明分类为合理的，任务级的所有证明步骤必须是成功可扩展的，178M. Hübner等人理论计算机科学电子笔记103（2004）161在逻辑层验证。将任务操作步骤扩展到逻辑层的“代价”有多高在Mega Proof Assistant[17]中，逻辑层由高阶自然演绎演算组成，并且在许多案例研究中，通过扩展到这种特定的基本逻辑，从抽象证明计划到抽象证明计划的距离非常大。巨大的（例如，见[17]）。我们目前正在开始重新实施的核心作为逻辑层和任务层作为抽象证明开发的分离层的MEGA由于这种从高阶自然演绎演算到CORE的移动，我们能够大大减少从抽象层到基本逻辑层的扩展距离。本文提出的任务操纵规则都是“安全的”，即，它们直接保证CORE中的逻辑可靠性。9它们非常我们用相对简单的逻辑问题（如图1所示）对它们进行了测试。该系统被设想为一个数学辅助系统的平台，以及数学辅导工具。与我们当前的应用程序和测试相反，这些应用程序需要在任务层指定域相关和“不安全”的操作符，在本文中，我们给出了一个自下而上的描述，任务层作为接口层的用户在核心之上。这种自下而上的方法通过更抽象的推理工具来丰富逻辑层，这是许多证明助手中的标准方法，以实现（理想地）抽象级别的证明开发。然而，自底向上方法的一个缺点是，它通常会导致抽象层对逻辑层的不必要的强烈依赖。因此，我们实际上是以自顶向下的方法开发任务层，以使其尽可能独立于底层逻辑层，这样，在理想情况下，逻辑层可以互换。然而，我们并不建议缺乏合理逻辑基础的证明助手。相反，我们的目标是更好地区分抽象层次的推理和扩展到逻辑层的可验证证明。在任务层，我们感兴趣的是允许面向知识的、直观的证明开发步骤。因此，具体的任务操作算子可以是特定于领域的，并且必须在从战术定理证明和证明规划已知的知识工程过程中获得和设计。或者，人类可以通过声明性地描述任务到后续任务的细化来体现操作员的角色;例如，9推测性的步骤，如案例分割和引理，可能不会在任务级别产生证明对象。然而，他们向核心的扩张是直截了当的。M. Hübner等人理论计算机科学电子笔记103（2004）161179Oracle步骤采用了[17]中介绍的交互式岛证明的思想。因此，具体可用的任务操纵操作符可以与相当“安全”的操作符（直接保证逻辑层处的逻辑可靠性的操作符，例如，构建在逻辑层之上的传统策略）到高度“不安全”的策略（那些具有非尖锐应用约束的策略导致频繁失败的逻辑层扩展，例如，人工构建的Oracle步骤）。 然而，为了将任务级证明归类为合理的，任务级的所有证明步骤必须在逻辑层成功地扩展和验证。将任务操作步骤扩展到逻辑层的“代价”有多高取决于在任务层使用的具体步骤以及所选择的逻辑层。 [17]逻辑层由以下部分组成高阶自然演绎演算与抽象证明通过扩展到该特定基本逻辑的计划在许多案例研究中是非常巨大的（例如，见[17]）。我们目前正在开始重新实施的核心作为逻辑层和任务层作为抽象证明开发的分离层的MEGA由于这种从高阶自然演绎演算到CORE的移动，我们能够大大减少从抽象层到基本逻辑层的扩展距离。本文提出的任务操纵规则都是“安全的”，即，它们直接保证CORE中的逻辑可靠性。10它们非常我们用相对简单的逻辑问题（如图1所示）对它们进行了测试。该系统被设想为一个数学辅助系统的平台，以及数学辅导工具。与我们当前的应用程序和测试相反，这些应用程序将需要在任务层指定域独立和引用[1] S.奥特西耶基于索引公式的显式抽象的证明规划框架。在Maria Paola Bonacina和BernhardGramlich的编辑，理论计算机科学电子笔记，第58卷。Elsevier Science Publishers，2001.[2] S. 奥特西耶分层上下文推理。博士论文，萨尔大学，2003年。出现。[3] C. Benzmüller，A. Fiedler，M. Gabsdil，H. 霍雷斯克岛 Kruij-Korbayova，M. 平卡阿，J. Siekmann，D.措瓦尔齐湾Quoc Vo和M. 沃尔斯卡 数学证明教学对话中的话语现象。在《教育中的人工智能会议录》（AIED 2003）中，关于对话系统的研讨会：着眼于课堂，澳大利亚悉尼，2003年。10推测性的步骤，如案例分割和引理，可能不会在任务级别产生证明对象。然而，他们向核心的扩张是直截了当的。180M. Hübner等人理论计算机科学电子笔记103（2004）161[4] C. Benzmüller，A. Fiedler，M. Gabsdil，H. 霍雷斯克岛 Kruij-Korbayova，M. 平卡阿，J. Siekmann，D.措瓦尔齐湾Quoc Vo和M.沃尔斯卡关于数学证明的对话。 在IJCAI-03电子学习系统知识表示和自动推理研讨会论文集中，墨西哥阿卡普尔科，2003年。[5] Y. Bertot，G. Kahn和L.特里以指为证。计算机科学的理论方面（TACS），1994。[6] R. 波那特。 I_t_r_i_v_D是Prof：Rende_ring_r_e_profsinBoxForm_I_n_D。 Aspin a l&C.Lüth，Proceedings of CIP03，罗马，意大利，2003年9月。[7] G. 根策; Untersuchunggenuéberd aslogischeSchli e nunII。 Mathem atische Zeitschrift，39：572-595，1935.[8] Grundy，J.，HOL系统中的窗口推理，在：1991年HOL定理证明系统及其应用（1991年），pp.177比190[9] X. 煌 在 断 言 级 重 构 证 明 。 以 . Bundy ， 编 辑 ， Proc.12th Conference on AutomatedDeduction，第738-752页。Springer-Verlag，1994.[10] Hubner，M. ，InteractiveTheo