理论计算机科学电子笔记174（2007）109-123www.elsevier.com/locate/entcs交互式派生查看器Steven Trac，Yury Puzis，Geo Sutzagrabe1迈阿密大学计算机科学系美国科勒尔盖布尔斯摘要这项工作介绍了交互式派生查看器（IDV）工具的图形化呈现的派生，写在TPTP语言。IDV提供了一个交互式界面，允许用户快速查看派生的各种功能。 IDV的一个特别新颖的特征是它能够提供通过识别推导中有趣的引理，并隐藏不太有趣的中间公式来进行推导。IDV作为SystemOnTPTP接口的一部分在线部署，因此可以通过任何Web浏览器随时访问。保留字：推导查看器，证明概要1引言由自动推理系统输出的证明向系统用户提供有用的信息，例如，证明结构，可能在未来的证明中有用的引理，最常用的公理等。即使是不形成完整证明的推导也是有趣的，因为它们可能提供导致问题公式或系统应用程序变化的见解，从而导致发现证明-自动推理系统通常以这种方式进行调试。然而，自动推理系统输出的证明往往不适合人类消费。对于一阶自动定理证明（ATP）系统，原因包括：• 将“自然”一阶形式（FOF）描述的问题转换• 矛盾证明的使用，它引入了不是公理的逻辑结果的公式。• 使用细粒度的推理步骤，如二进制解析，夸大了证明的大小。1 电子邮件地址：strac@mail.cs.miami.edu1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.09.025110S. Trac等人理论计算机科学电子笔记174（2007）109已经开发了几种类型的工具，使ATP系统的输出更容易为人类所理解。这些包括推导的图形化呈现[10]，通过引理的识别来构造证明[1]，将归结反驳证明转换为自然演绎证明[4]，以及将证明完全转换为自然语言形式[2]。这项工作描述了交互式派生查看器（IDV）工具，用于以TPTP [13]语言[12]编写的派生的图形渲染。IDV提供了一个交互式界面，允许用户快速查看派生的各种功能。IDV的一个特别新颖的功能是它能够通过识别推导中有趣的引理来提供推导的概要IDV作为SystemOnTPTP接口的一部分在线部署[11]，因此可以通过任何Web浏览器进行访问。第2节描述了基本的IDV工具及其渲染过程。第三节说明证据概要的制作第4节解释了IDV如何部署在Web上，并提供了一个说明性的应用程序。第5节总结并讨论了IDV计划的未来发展。2基本IDV导出是一个有向无环图（DAG），其叶节点是从输入问题中导出的公式，其内部节点是从父公式中推导出的公式，其根节点是最终导出的公式。例如，CNF反驳证明是一个推导，其叶节点是由公理和否定猜想形成的子句，其根节点是false子句。记录推导所需的信息至少是叶公式和每个推导公式及其父公式的引用。可以记录和有用的更详细的信息包括：每个公式的作用，例如，公理、猜想、简单推导等;在每个推理步骤中使用的推理规则的名称;关于每个推理步骤的足够细节以确定性地再现该步骤;以及每个推理公式相对于其父公式的语义关系，例如，逻辑推论、计数器定理等。TPTP语言足以记录所有这些以及更多内容。用TPTP语言编写的推导是一个带注释的公式列表。每个带注释的公式都包含一个名称、一个角色、逻辑公式、一个源记录和一个字段，用于记录用户应用程序所需的任意有用信息。每个推断公式的源是包含推断的推断规则名称，一个状态记录，包含公式与其作为SZS本体值[14]的父母，以及对其父母公式的引用列表IDV采用TPTP语言进行派生，并使用Java的Swing组件呈现DAGIDV可以作为一个独立的应用程序运行，也可以作为一个Web浏览器小程序运行;这里的描述主要集中在Web选项上，因为它提供了ready（重新配置）功能。mote）访问IDV而无需任何安装。S. Trac等人理论计算机科学电子笔记174（2007）1091112.1接口图1显示了ATP系统EP 0.91 [9]针对TPTP问题PUZ 001 +1的推导输出的渲染。2IDV窗口分为三个窗格：顶部控制条窗格提供控制按钮和滑块，中间主窗格显示渲染的DAG，底部窗格提供鼠标指向的节点Fig. 1. EP控制条窗格中的按钮和滑块从左到右为• 放大-放大50%2PUZ 001 +1是“阿加莎阿姨”问题，描述了一个场景，三个人住在一座豪宅里，阿加莎阿姨被杀了。目的是证明阿 加莎 阿姨 是自 杀的所 有的TPTP 问 题， 他们 的解 决方 案 ，以 及解 决方 案的 IDV 效 果图 ，都 可以 通过http://www.tptp.org/在线获得。- 通过问题链接找到问题，通过TSTP链接找到解决方案，然后通过查看IDV树链接到任何解决方案页面（具有TPTP格式的解决方案）的顶部，以生成IDV渲染。112S. Trac等人理论计算机科学电子笔记174（2007）109• 垂直调整-缩放渲染以适应中间窗格的高度• 适应水平-缩放渲染以适应中间窗格的宽度• 缩小-缩小50%• 显示高度-设置底部窗格中的文本行数• 概要级别-设置显示的最低兴趣级别-参见第3节。• 重绘-重绘推导。这通常在提取概要后使用- 参见第3节。• 概要撤销-将最小兴趣度级别设置为其先前值。• 概要重做-在任何撤消步骤之后，将最小兴趣度级别设置为它的下一个值。• 关于按钮派生DAG的呈现使用形状和颜色来可视地提供有关派生的信息。每个节点对应于推导中的一个公式公式的作用通过节点的形状来表示：三角形表示公理，六边形表示引理，倒三角形表示假设，房子表示公理，倒房子表示否定公理（如将FOF问题转换为CNF时所做的那样），圆形表示普通导出公式，正方形表示false公式。节点可以在上面用圆圈中的=符号来注释，以指示等式推理被在其推理中使用，例如，一种调节推理。可以对节点进行注释在顶部的内部有一个红色圆圈，表示公式不是其父项的逻辑结果，例如，在Skolemization和分裂推理中，如SZS状态所示。节点可以在下面用红色三角形注释，以指示它是分裂推断的父节点，例如，SPASS [15]实现的显式分裂或Vampire[7，8]或E [9]实现的伪分裂用户可以通过两种方式与派生渲染进行交互。首先，将鼠标移动到任何节点上，将导致与该节点对应的带注释的公式显示在底部窗格中。同时，鼠标悬停的节点以蓝色突出显示，从叶节点向下到鼠标悬停的节点的所有节点以绿色突出显示，从鼠标悬停的节点向下到根节点的所有节点以红色突出显示。效果在图1中是明显的。绿色突出显示显示鼠标悬停在节点上的公式，红色突出显示鼠标悬停在节点上的公式高亮显示的强度根据从鼠标悬停的节点到高亮显示的节点的最小路径长度而减小。这使得较近和较远的祖先和后代之间的差异变得容易一个特别有用的效果是识别哪些公理（叶节点）是最接近的祖先。第二种交互形式是单击任何节点。这将创建一个弹出窗口，其中包含所单击节点及其父节点的注释公式，如图2所示。点击节点的注释公式显示两次，一次在父节点上方，一次在父节点下方，允许推理步骤的双向读取S. Trac等人理论计算机科学电子笔记174（2007）109113图二. EP对PUZ 001 +1的反驳证明中的弹出2.2执行IDV读取TPTP格式的派生。它对FOF或CNF的形式敏感。渲染分两个阶段执行：第一阶段确定DAG节点和边的布局，第二阶段实现派生DAG的图形显示。DAG的布局是在五遍算法中确定的，类似于[3]中的算法。第一遍为每个节点分配一个等级。rank是渲染树中节点的级别，顶部行包含级别1的节点，并向下增加。在第三遍中使用秩来确定每个节点的Y坐标。 第一行FOF节点（叶节点）被放置在第一个等级中。 然后使用深度优先搜索（DFS）将增加的排名分配给其余的FOF节点。接下来，第一行CNF节点被放置在最大FOF节点排名之上的排名中。最后，再次运行DFS算法，以将增加的排名分配给其余的CNF节点。在所有节点都被分配了等级后，边被如下划分：如果一条边连接了两个相距超过一个等级的节点，则该边被虚拟节点和边的链所取代。虚拟节点在两个端节点的等级之间被给予递增等级。 如果一个非虚节点有多个虚节点链从它向下延伸，那么这些链将尽可能地合并，并在链的末端节点上方立即分割。第二遍直接遵循[3]中的算法，设置从左到右114S. Trac等人理论计算机科学电子笔记174（2007）109顶点顺序的行列内的迭代启发式结合权重函数和本地换位，以减少边缘交叉。在每个列处引入虚拟节点保证了边缘交叉只能发生在相邻列之间。第三遍为每个节点设置初始X坐标和最终Y坐标。具有最大数目的节点的秩确定图的最大宽度。从第二遍开始，秩内的顶点从左到右排序，等距X坐标被赋予每个秩中的节点，在0和图的最大宽度之间。最终的Y坐标线性地基于节点第四遍为每个节点找到最佳X坐标。对于此过程，使用弹簧嵌入。3弹簧嵌入是一种图形绘制技术，它将图形建模为弹簧系统，然后使用能量最小化来分隔节点。以下力是平衡的：用于保持边在一定长度的边弹簧力，用于保持节点不太靠近的节点到节点排斥力，用于保持所有边指向下的重力，以及用于保持节点不水平地分散得太远的排斥边界在第四遍之后，X和Y坐标被固定-节点不能通过用户交互移动。第五个过程生成Bezier曲线以绘制节点之间的边。如果两个非虚拟节点由虚拟节点链连接，则虚拟节点节点用于绘制贝塞尔曲线的点由第一阶段确定的布局并不能保证节点不会重叠（或者，如果使用虚拟节点来引导边生成，则边不会穿过节点）。避免节点重叠的程度由弹簧嵌入中的迭代次数确定。已经发现当前实现中的迭代次数足以避免大多数重叠。确定布局后，将呈现界面和DAG。IDV是用Java实现的，主要使用基本的Swing组件。使用StreamTokenizer读入TPTP公式。IDV窗口是一个JFrame，呈现是一个JPanel。JPanel中使用MouseMotionMap来检测鼠标何时移动到节点上，以实现节点着色功能。JPanel中使用鼠标按钮来检测节点何时被单击，以实现弹出窗口功能。JFrame是用JavaScript和ChangeJavaScript实现的，用于检测用户3衍生概要如第1节所述，ATP系统输出的推导的特征之一是使用细粒度的推理步骤，如二进制解析，这夸大了证明的大小。由人类输出的派生通常使用粗粒度的推理步骤，将中间步骤留给“读者”。的推导公式3感谢Christian Duncan提供了原始的Spring嵌入代码。S. Trac等人理论计算机科学电子笔记174（2007）109115这种较粗粒度的推理步骤是它们的叶祖先的逻辑结果通过只考虑那些高于一定显著性水平的逻辑结果（隐藏那些低于该水平的逻辑结果），形成了详细推导的概要。在概要中，隐藏公式的最低可见子代成为最高可见子代的父代。摘要隐藏了最终的粒度推理步骤和中间公式，从而使用户更容易掌握证明的概述。用户可以稍后选择检查细节。句法可以类似地用于概括非常大的推导。IDV能够通过CNF反驳形成证明的概要。 这是通过对推断的CNF公式的兴趣度进行评级，并隐藏公式评级低于用户指定阈值的节点来实现的。推断CNF公式的兴趣度评级由AGInT系统计算[6] -参见第3.3节，用户使用控制条窗格中的滑块设置阈值3.1接口每个公式的兴趣度是范围为0的值。0比1。0. 一些公式具有预设的兴趣度评级：叶公式被设置为1。0时，最高CNF公式设置为1。0时，叶FOF公式和最顶层CNF公式之间的中间公式被设置为0。0，所有从否定一个猜想得出的公式都设为1。0，根公式设置为1。0.其他公式的值的兴趣度，即，推导的内部CNF公式由AGInT系统计算，如3.3节所述。最初，顶部窗格中的阈值滑块设置为兴趣度值0。0，并且所有节点都显示在渲染中。当滑块向上移动时，兴趣度阈值增加，并且公式评级低于阈值的节点被隐藏。图3示出了图1中的推导，其中兴趣度阈值为0。5.提取概要后，可以放大，仅渲染可见节点。这是在IDV中通过控制条中的重画按钮完成的。图4示出了图3的概要导出渲染。在重画之后，可以移动阈值滑块并且再次重画推导，以产生不同级别的概要。请注意，在重画之后，如果阈值被移动到低于用于重画的兴趣度水平，则隐藏节点不会立即变得可见-需要另一次重画。通过以红色显示的阈值警告用户此状态。重画序列可以使用大纲撤消和重做按钮撤消和重做。当使用滑块调整兴趣度级别时，节点的布局不会改变-只是隐藏了更多或更这提供了派生的同一性心理地图（心理地图是用户当重新绘制大纲时，尽可能保持头脑中的地图是很重要的。为此，大纲中未隐藏的所有节点都将按照与原始内容相同的顺序保留。连接可见节点的Bezier曲线将重新计算，但保持与原始曲线相同的形式116S. Trac等人理论计算机科学电子笔记174（2007）109图三. EP对PUZ 001 +1的反驳证明的有趣节点如第2.1节所述，当单击节点时，会出现一个弹出窗口，其中包含节点及其父节点的注释公式。在reddraw之后，弹出窗口中显示的父项是此渲染中公式的父项它们可能不是公式的原始父母。如果某些父信息与原始信息不同，则弹出窗口会通知用户这一点。3.2执行可用性评级存储在注释公式的有用信息字段中的记录中。公式有两种方法来进行兴趣度评级。首先，输入到IDV的注释公式可能已经具有兴趣度值。其次，输入公式没有兴趣评级，AGInT系统必须由IDV调用。在这种情况下，一旦用户使用阈值，就会调用AGInTS. Trac等人理论计算机科学电子笔记174（2007）109117见图4。 EP对PUZ 001 +1的反驳证明简介控制面板中的滑块。当用户点击重画按钮时，导出概要被渲染如下：首先，如果DAG中的非虚拟节点的兴趣度评级大于阈值，则将它们设置为感兴趣，并且将所有虚拟节点设置为不感兴趣。然后检查每个秩以查看其是否包含任何中间节点。如果排名包含至少一个感兴趣的节点，则排名被保留，否则排名为空，并且排名下面的所有节点被向上移动排名（即，其等级递减）。每个节点的原始等级被存储用于重绘目的。在等级被更新之后，保留等级中的节点的Y坐标被更新，如第2.2节所示。最后，更新Bezier曲线以唯一地将每个感兴趣的节点连接到其最近的感兴趣的祖先，这些祖先是使用DFS搜索DAG找到的。所有不感兴趣的节点在重画后保持隐藏状态。当单击概要撤消/重做按钮时，当前感兴趣的阈值将更改为推送到撤消/重做堆栈上的最后一个值，并调用上面的重绘过程。3.3兴趣度评级推导中推导的CNF公式的兴趣度评级由AGInT系统的运行时过滤器和静态排名器组件计算。 AGInT是一个发现给定公理集的有趣定理的系统。AGInT118S. Trac等人理论计算机科学电子笔记174（2007）1092级1级忠诚，归一化和平均2级店预处理明显性、重要性、复杂性、惊奇性、强度、适应性、焦点更新滑动窗口使用演绎方法来发现-它使用ATP系统来生成给定公理集的CNF逻辑结果，过滤逻辑结果以提取有趣的定理，然后计算每个定理的兴趣度评级。这一基本过程发生在外层控制循环的上下文中，该循环定期重新聚焦逻辑结果的生成，从而使AGInT能够深入到逻辑结果的搜索空间中。详情见[6]。在IDV的上下文中，推导的导出CNF公式作为最顶层CNF公式的逻辑结果（即，最上面的CNF公式被认为是导出公式的公理AGInT图5显示了这两个组件的组合架构运行时筛选静态排序器图五. AGInT的过滤器和静态排序器的结构运行时过滤器的任务是积极地过滤并丢弃无聊的公式。每个公式必须首先通过预处理器，然后必须通过大多数（即，至少有四个）的七个过滤器：明显性，重量，复杂性，清晰度，强度，适应性和重点。每个过滤器都保持一个滑动窗口，该窗口由迄今为止过滤器对公式的评估中的最佳不同分数定义。每个窗口的上限和下限都被初始化为该过滤器的最差可能得分。如果传入公式的得分等于或优于下限，则它通过过滤器，得分用于更新窗口。将上界和下界初始化为最差的可能分数，允许所有公式通过，直到窗口开始向上滑动。因此，流中早期的一些无聊公式可能会通过运行时过滤器。因此，存储在第一遍中通过运行时滤波器的公式，并且在处理完所有公式之后，再次对存储的公式进行滤波，其中窗口从第一遍开始被固定。这将删除任何不符合最终下限的内容。个别过滤器如下：预处理器：预处理器检测并丢弃明显的重言式，例如，包含原子及其否定的子句明显性：明显性估计证明公式的难度。公式的显而易见性得分是其推导过程中的推理次数一分数越高越好。权重：权重估计读取公式所需的时间。包含很多符号（变量、函数和谓词符号）的公式不那么有趣。公式的权重分数是它包含的符号数。分数越低越好。S. Trac等人理论计算机科学电子笔记174（2007）109119复杂度：复杂度估计理解公式所需的时间。公式包含非常多的不同的功能和谓词符号，代表许多不同的概念和属性，是不太有趣的。公式的复杂性得分是它包含的不同函数和谓词符号的数量。分数越低越好。惊奇度：惊奇度测量概念和属性之间的新关系包含函数和谓词符号的公式更有趣，这些符号很少在公式中一起出现。一对符号的符号对重复性得分是包含两个符号的公理的数量除以包含任一符号的公理的数量。公式的重复性得分是公式中所有不同符号对的符号对重复性得分之和分数越低越好。强度：强度度量公式从其派生树中的叶祖先总结信息的程度公式（或公式集合）的多个分数是公式中的函数和谓词符号的数量除以公式中的不同函数和谓词符号的数量公式的强度分数是其叶祖先的复数除以公式本身的复数。分数越高越好。自适应性：自适应性衡量公式中普遍量化的变量受到约束的程度。一个小句的适应性得分是小句中不同变量的数量除以小句中变量出现的数量分数越低越好。焦点：焦点衡量公式做出积极或消极陈述的程度。令FPL和FNL是子句中正文字和负文字的分数。小句的焦点得分是1 +FPLlog2（FPL）+FNLlog2（FNL）。具有多达三个文字的子句被认为具有完美焦点，因为它们的极性分布是有限的。分数越高越好。通过运行时过滤器的公式被认为是有趣的。静态排名器的任务是计算公式的最终兴趣度评级这分两个阶段完成：首先为每个公式计算有用性分数，其次，将所有分数单独归一化，然后取平均值。复杂性：复杂性度量一个有趣的公式对进一步有趣的公式的证明有多大贡献，即它作为引理的有用性。公式的有用性得分是其感兴趣的下降项的数量的比率（即，已通过运行时过滤器的后代）超过其后代总数。分数越高越好。归一化和平均：来自每个运行时过滤器和静态评估的公式的分数被归一化到范围0。0比1。0. 得分最差的公式最终得分为0。0，则具有最佳得分的公式的最终得分为1。0，所有其他分数都是线性插值的。如果一个特定过滤器的最差和最好分数相等，那么该过滤器不会在公式之间区分，并且这些分数被删除。每个公式的余下分数取平均值以产生最终兴趣评级。120S. Trac等人理论计算机科学电子笔记174（2007）109带有APPLET>tags的IDV小程序推导AGInT服务4部署和应用程序IDV作为SystemOnTPTP接口的一部分在线部署，http://www.tptp.org/cgi-bin/SystemOnTPTPFormMakerIDV代码被包装为Web浏览器applet，所有渲染计算都在客户端完成。构成要呈现的推导的带注释的公式可以作为
我的内容管理
收起
我的收益 登录查看自己的收益
我的积分
登录查看自己的积分
我的C币
登录后查看C币余额
我的收藏 
我的下载 
下载帮助 
