蜘蛛图自动证明算法及其应用

理论计算机科学电子笔记91（2004）246-263www.elsevier.com/locate/entcs用蜘蛛图实现定理的自动证明Jean Flower1，3和Gem Stapleton2，4The Visual Modeling Group布莱顿大学英国布莱顿摘要蜘蛛图是一种用于表达逻辑语句的可视化符号。 本文介绍一个工具，支持推理与健全和完整的蜘蛛图系统。 该工具允许用户构建图表和证明。 我们提出了一个算法，该工具使用以确定一个图是否在语义上包含另一个图。如果前提图在语义上确实包含结论图，则向用户呈现证明。 否则，它给出了一个反例：前提的模型不是结论的模型。 [8]中给出的完备性证明可以用来创建另一种证明编写算法。这里描述的算法通过提供反例和明显更短的证明来改进这一点。关键词：蜘蛛图，图解推理，自动推理，证明写作。1介绍在本文中，我们提出了一个图解推理系统的定理证明算法。这样一个系统包括三个方面。首先，我们要明确所考虑的图的语法。第二，一个是给语法正确的图赋予意义：语义。最后，推理1这项工作是在EPSRC赠款GR/R63516的支持下完成的感谢Andrew Fish、Chris John、John Howse和John Taylor对本文早期草稿的评论2这项工作是在EPSRC赠款01800274的支持下完成的3电子邮件：j.a. bton.ac.uk4电子邮件：g.e. bton.ac.uk1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2003.12.016J. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-247Mic eCatsDo g sd1d2Fig. 1. 一个维恩图和一个蜘蛛图。将一个图转换为另一个图的规则是特定的。这些规则必须健全，最好是一套完整的规则。简单的图解系统的例子是维恩图和欧拉图.在维恩图[18]中，轮廓（区域）之间所有可能的交点都必须出现，阴影用于表示空集。图d11是一个维恩图。由Shin [11]形式化的Venn-II系统可能是最著名的-图解推理系统的实现。Venn-II图扩展了Venn-diagram符号，使用额外的语法来表示非空集。欧拉图利用包围、排斥和交的拓扑性质分别表示子集、不相交集和集交。蜘蛛图[6，7，8]基于欧拉图。蜘蛛用于表示元素的存在，阴影用于设置集合基数的上限。蜘蛛被画成由线连接的点（脚）的集合。图1中的图d2是蜘蛛图，并且表示“不是老鼠就是狗”蜘蛛图系统的合理而完整的推理规则已经给出[7，8]。概念图[12，10]和基于欧拉的图都被用来直观地表达逻辑语句和推理[1]。在这两种情况下，都有一种文本形式，可以用作 图，这是特别有用的工具建设。给定一个简单的概念图，可以绘制一个蜘蛛图来表达相同的信息。每一种类型都会在蜘蛛图中产生一个轮廓。在概念图中绘制的概念将给出一个蜘蛛（命名或以其他方式），概念图中的关系可以用轮廓表示。随着概念图的语法变得越来越丰富，例如嵌套图，要看到这样的语句如何表现为蜘蛛图就变得越来越困难。事实上，概念图的表达能力[9]超过了蜘蛛图[14]。一个更有趣的表达性比较是概念图和约束图之间的比较，约束图包括对象之间关系的自然表示[2]。如果图解推理是实用的，那么工具支持是必不可少的。在没有软件支持的图表系统中，一BC248J. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-既费时又容易出错。如果我们希望找到一个证明，证明一个diagram在语义上包含另一个diagram，一个策略可以是将两个diagram转换为一阶逻辑语句，并使用现有的证明环境。然而，我们寻求创建纯粹的图表证明，这可以为使用图表建模的用户提供反馈。在[15]中，提出了一种使用有向无环图实现Euler/Venn推理系统的方法。这些图类似于我们的抽象语法，它们捕获了类似于Venn-II diagrams的图的在[16]中进一步讨论了该实现，该工具的重点是检查用户应用的推理步骤的正确性，但该工具不会自动编写证明。在本文中，我们讨论了蜘蛛图的证明环境，在Java中实现。通过实现这个工具，我们表明，它是可以完全自动化的图解定理证明。我们实现的工具允许用户构建蜘蛛图和编写证明，以及自动化证明建设。给定两个图d1和d2，如果我们想知道无论D1在语义上是否包含D2，该工具将给出两个响应之一如果d1在语义上包含d2，那么工具将提供一个证明，否则它将提供一个反例。蜘蛛图构成了更具表现力的约束图表示法的基础约束图还包括其他语法元素，例如通用蜘蛛和箭头。泛蜘蛛代表泛量化（蜘蛛图中的蜘蛛代表存在量化）。箭头表示关系导航。文[2]给出了约束图的语义，文[13]介绍了一个约束图推理系统（具有约束的由于约束图符号扩展了蜘蛛图符号，因此开发此工具是朝着开发此类约束图工具迈出该实现使用了一个算法，该算法具有[8]中给出的完整性证明中使用的一些步骤。在[13]中，作者指出，用于证明蜘蛛图系统中的完整性的策略扩展到了约束图系统。因此，很可能我们在这里提出的证明写作算法（因此我们的工具）可以扩展到用约束图证明定理。图解推理系统的一个应用是表达和推理面向对象模型中的约束统一建模语言（UML）是软件工程师在面向对象建模过程中使用的主要图形符号的集合。在UML中唯一的非图解符号是对象约束语言（OCL）。OCL本质上是一阶谓词的程式化形式J. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-249HH逻辑，用于表达正式的陈述。蜘蛛图和约束图补充了UML的图解主题，并提供了OCL的替代，也许更直观的符号2蜘蛛图我们现在给出酉蜘蛛图的非正式描述。更多的细节可以在[8]中找到。 等高线是一条有标号的简单闭平面曲线。边界矩形是一个简单的封闭平面曲线，没有标记。 基本区域是由轮廓或边界矩形包围的点的集合。区域是递归定义的：任何基本区域都是区域，任何非空的区域的并集、交集或差都是区域。区域是指其中不包含其他区域的区域。如果区域的每个组成区域都被着色，则该区域被着色蜘蛛是一棵树，它的节点被称为脚，被放置在不同的区域。如果蜘蛛的一只脚出现在某个区域，它就会接触到该区域。一只蜘蛛，s，据说居住在它所接触的区域的联合区域。这个地区被称为S的栖息地。一个酉图是一个边界矩形适当包含的轮廓，阴影和蜘蛛的有限集合。区域可以由包含它的等高线的标签集（包含标签集）和排除它的等高线的标签集（排除标签集）来描述。 我们将定义两个区域相等，如果它们具有相同的包含标签集和排除标签集，即使它们在不同的图中。图1（第1节）中的图d2包含三个带标记的等高线和五个区域，其中一个区域是阴影。有两只蜘蛛。一只脚的蜘蛛栖息在猫的内部（标记的轮廓），但在狗和老鼠的外部。另一种蜘蛛栖息在由老鼠体内的区域和狗体内猫体外的区域组成的区域。酉图构成了复合图的构建块。为了使我们能够表达析取和合取信息，我们使用连接词：H和H。 如果 D1和D2是蜘蛛图，那么 D1HD2也是蜘蛛图（“D1或D2”）D2D2（图2示出了复合图d1d2。我们的约定是使用小写d表示酉图，对于可能是单一的或复合的图表。蜘蛛图中的区域表示集合。在酉图中包含所有带的区域表示全集。一个蜘蛛代表一个元素在由其栖息地代表的集合中的存在。不同的蜘蛛代表不同元素的存在。在由阴影区域表示的集合中，所有元素都由蜘蛛表示。因此，我们可以表达集合基数的上下界的化合物所250J. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-|D=图二. 蜘蛛图D=d1Hd2.图D1HD2（D1HD2）的语义通过取D 1和D 2的语义的析取（合取）来给出。给定一个解释m，即一个全称集U，以及从区域到U的子集的映射，我们可以决定D的语义在m中是否为真。如果D的语义为真，我们说m是D的模型，记为m=D，并且说m满足D.每一个酉图都是令人满意的。 形式语义可以在[8]中找到。图2中的图d1表示（由表示的集合）A−B是空的，并且A<$B中至少有一个元素。图d2表示A−B中至少有两个元素，B.因此，如果我们将全称集定义为U={ 1， 2}，并将外部区域映射为n，仅A中的区域映射为n，A和B中的区域映射为{1}，仅B中的区域映射为{2}，那么这种解释是d1的模型，而不是d2的模型。由于这种解释是d1的模型，因此它也是d1Hd2的模型。3推理规则在本节中，我们给出了蜘蛛图的语法推理规则的非正式描述。每个规则都表示为一个蜘蛛图到另一个蜘蛛图的转换。规则的正式描述可以在[8]中找到。首先，我们考虑适用于酉图的规则规则1引入轮廓（可逆）。一个轮廓可以被引入到一个单一的图提供了以下情况。 新等高线的标签在图表中不存在。 每个区域分为两个区域，并且保留着色。每只蜘蛛的每只脚都被一对相连的脚所取代，每个新区域都有一只脚。规则2引入阴影区（可逆）。 如果酉图d不是基于维恩图，那么我们可以在d中引入一个新的阴影区域，该区域不是任何蜘蛛栖息地的一部分。在图3中，通过应用规则1，加上标记为B的轮廓，从d1获得图d2。为了从d2得到d3，使用与规则2相反的规则，去掉一个区域.规则3：分离蜘蛛（可逆）。设d是一个酉图，一BABD1D2J. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-251一ABABd1d2d3图三. 规则1和规则2（相反）的适用。D图四、规则3的应用。D图五、第四条规则的适用。捕获蜘蛛E，其栖息地被划分为区域R1和R2。 我们可以用d1H d2代替d，其中d1和d2是d的副本，只是e的栖息地在d 1中被简化为r1，在d2中被简化为r 2。图4中的图d有一个有两只脚的蜘蛛。它的栖息地分为两个区域，一个在B内，另一个在U−（A<$B）内。我们可以把这个蜘蛛分成两部分，得到d1Hd2。规则4排除中间（可逆）。 设d是一个酉图，有一个非阴影区域r。 我们可以用d1H d2来代替d，其中d1和d2是d的副本，除了r在d1中被阴影化，并且在d2中有一个额外的蜘蛛，其栖息地为r。排除中间规则应用于图5中的图d。 我们遮蔽B-C（给出d1）并将蜘蛛添加到B−C（给出d2），如d1Hd2所示。第5条阴影的消除。 如果d是有阴影区域的酉图我们可以从r中删除阴影规则6蜘蛛的擦除。如果d是带有蜘蛛s的酉图它的栖息地是一个完全没有阴影的区域，那么我们可以从d中删除s我们给出的下一个规则用一个单一的酉图来代替所有组成部分都是酉的合取复合图。这个过程是在α图- 有相同的区域设置。例如，图6中的图d1Hd2可以由酉图d3代替。d3中任意区域的蜘蛛数量A B一BABD1D2一BACBCD1D2一BC252J. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-⊥H⊥{∈ D}∈ D∈ D≤►⟨⟩一BCD3见图6。 结合酉α图。是该区域在d1和d2中的最大数，如果该区域在d1或d2中被着色，则该区域在d3中被着色。 生成的图d3称为D1D2的组合图。有时候合取词的成分代表矛盾的信息。这个符号被称为伪图，它被定义为一个没有模型的酉图。这个符号可以使用类似于谓词逻辑中的推理规则来引入或删除。它也可以使用我们现在定义的组合规则来引入对于图D=di，其中每个di是酉α-图，并且每个对di∈Ddi，dj，具有相同的区域集或其中一个dis，我们定义组合图D是一个酉图（unitary diagram）：(i) 如果对任意di∈ D，di=<$，则D<$=<$。(ii) 如果一个区域在D的一个幺正分量中被遮蔽，而在另一个幺正分量中包含更多的蜘蛛，则D=。(iii) 否则，D的分区与每个D的分区相同，. 阴影区域 D是至少在一个D中着色的区域，. 对于每个区域，z，in D如果d i在z中有n i个蜘蛛，则D有max n i：d i蜘蛛在z。规则7合并（可逆）。我们可以替换D =di，其中每个di∈Ddi是酉α图，并且每对di，dj具有相同的区域集或一个的d i s是由组合图D。有许多规则（并非都是可逆的），由于空间原因而被省略，在命题逻辑中具有类比，例如不一致性和结合性。设D1和D2是图.我们说D2可以从D1得到，记为D1D2，当且仅当存在一个图序列D1，D2，.，Dm使得D1= D1，Dm= D2，并且对于每个k，其中1km<，Dk可以通过一个推理规则的单一应用被变换为Dk +1。这样的一系列图被称为从前提D1到结论D2的证明. 如果D 1的每个模型也是D 2的模型，则D1在语义上蕴涵D2，记为D1<$D2。 一个推理规则r是有效的，如果只要D2是通过一次r的应用从D 1得到的，则D1≠D2。上述推理规则均成立。因此，这个制度是健全的。定理3.1可靠性和完备性 设D1和D2是蜘蛛一BACBCD1D2J. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-253一B==2ABABAB图. 则D1<$D2当且仅当D1<$D2[8]。4一种证明写作算法文[8]中给出的完备性证明被直接转化为一个效率很低的证明书写算法。在本文中，我们提出了一个更有效的算法，产生更短的证明，见4.4小节。给定D1和D2，我们的算法证明了D1<$D2（当D1<$D2）或找到一个反例（当D1/<$D2）。我们算法的第一步是DD12我们的公司A d d z o n e ss pl its pi d er sDi s jun cti v e n orrABformc ombin eABD*=见图7。 应用算法。将轮廓（规则1）引入到D1和D2的分量，直到每个酉分量具有相同的标签集。其次，我们引入区域（规则2）到每个酉成分，直到所有的酉成分具有相同的区域集。接下来，我们分裂蜘蛛（规则3），将图转换为α图。在这个阶段，所有的单一组件具有相同的轮廓标签集，相同的区域集，并且所有的蜘蛛都只有一只脚。接下来我们AB一BAB一BAB一BABAB一BD*=1B一B一B一AB254J. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-222222222221D*=图8.第八条。 D2期追踪。转换为析取范式。 我们通过组合（规则7）删除所有合取项，并表示结果图D1和D2。到目前为止，这个过程的一个例子可以在图中看到7 .第一次会议。如果D1有0个幺正子作为它的幺正子，则我们完成。Suppose因此D1编码器可以获得非伪码。我们考虑到所有的情况，此外，对于符号经济学，我们可以把结果图称为 D1图。该算法的下一步是压缩D2-排除中间（规则4），直到不可能进一步应用排除中间，给出图DC。为例如图8图d1Hd2Hd3Hd4可缩小（复制d2）至d8Hd9。注意这里D C=D2，因为所有用于获得D C的规则是可靠的。 还要注意，D1不等于D1，所以有一个从D1到D2的过程当且仅当有一个从D1到DC 的 过 程。我们寻求从一般D1到D2的概率的任务已经减少到寻求从D1到DC的概率，其中这些是酉α图的两个（双）析取。我们将D1的每一个酉成分d1与DC 进 行 了 比 较. F或每个ch比较-我们将检查以下情况之一是否成立：(i) d1与DC（在第4.1小节中定义）相矛盾(ii)d1是DC的某个分量d2的超图（定义如下：（第4.2段）当（i）对某些d1成立或（ii）对所有d1成立时，算法终止。如果（i）对于某个d1成立，则可以从d1生成矛盾，如4.1小节所述。若（ii）对所有d1成立，则D1可变换为dc. 转换D1转换为DC，我们从DC的酉成分中删除了阴影和蜘蛛，B ABBD1D2D3BABABD5D6D7一BABDC=2D8D9一D4一一ABJ. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-255222⊥⊥2H将每个组件转换为在DC中出现的子图，我们再次将结果图称为D1图。接下来，在图1中定义一个新的酉复合，C不发生在D1中。我们使用规则DDHDJ加入所有DC到D的酉分量。 为了完成转变，我们改变2 1D1通过删除重复的图表或根据需要复制图表（使用相同性），直到D1=DC。最后，如果有一个d1（i）和（ii）都不成立（也就是说，算法没有终止），那么对d1应用排中律根据第4.3节。一旦应用了排中律，就重复D1中的成分对DC 的 检 查。4.1矛盾中的图解设d1和d2是具有相同区集的酉α图。我们说d1和d2是矛盾的，如果d1Hd2的组合图是π。如果d1与图D的所有酉分量矛盾，那么我们说d1与D矛盾。引理4.1设d（k）是一个酉α-图，它是矛盾的其中D是酉α图的析取还假设D的每个酉分量都是或具有与d相同的区域。那么存在一个d的模型，它不是D的模型。证据我们生成这样一个模型，m，通过将全集作为d中的蜘蛛集。在m中，d中的每个区域代表居住在该区域的蜘蛛的集合如果D只包含假成分，那么m不是D的模型，我们就完成了。相反，假设D包含至少一个非假成分。选择任意非假分量dJ。由于d dJ的组合图是，因此我们可以选择一个区域z，该区域在d和dJ中的一个中具有更多的蜘蛛，并且在另一个中具有阴影。如果z在d中包含的spider比在dJ中包含的spider多，那么不是所有的元素都由z中的spider表示，所以m不是dJ的模型。或者，z在d中被阴影化，并且在DJ中包含更多的蜘蛛。在这种情况下，dJ中z中的不同蜘蛛并不代表不同的元素，所以m不是dJ的模型。由于DJ是D的任意非假分量，因此m不是D的任何分量的模型。因此m不是D的模型。Q因此，如果在D1中存在与DC矛盾的酉成分d1，则存在D1的模型不是DC的模型（因为D1是2 1 2 1是酉图的析取）。D256J. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-2Σ4.2超图和子图图d1是d2的超图，d2是d1的子图，当且仅当下列成立。(i) 图d1和d2具有相同的区域。(ii)d2中的所有阴影都发生在d1中。(iii)d2中的所有蜘蛛都出现在d1中。(iv) 如果一个区域z在d2中是阴影的，那么z在d1中有相同数量的蜘蛛D2。一个图可以通过首先删除额外的阴影（规则5）然后删除额外的蜘蛛（规则6）来转换为任何子图。4.3排除中间规则（Exclusive Middle Rule）在本节中，我们描述如何智能地将排除中间规则应用于D 1的组合d1。我们将发现，在DC，酉图D1与D1不矛盾。定义两个酉图之间的排除中间测度，记为m（d1，d2），如下所示。设d1和d2是两个具有相同区集的酉α图。设Sh（d1，d2）表示在d2中有阴影但在d1中没有阴影的区域的数量。令Zu表示d1中的非阴影区域的集合。设Sp（z，di）表示di中栖息在z上的蜘蛛的数量。如果d1和d2不矛盾，m（d1，d2）= Sh（d1，d2）+max{Sp（z，d2）-Sp（z，d1），0}.z∈Zu粗略地说，这意味着如果d2比d1有更多的蜘蛛和阴影区域，则该度量是大的。注意，如果m（d1，d2）= 0，则d2是d1的子图。对于矛盾的图d1和d2，测度定义为∞。给定d1和DC，不矛盾，求DC中每个d2的m（d1，d22 2选择一个d2，m（d1，d2）最小 这个最小的尺度是有限的。 我们定义Z为一个集合，包含d2的所有区域，并带有额外的阴影或蜘蛛。这些区域对和m=m（d1，d2）有贡献。对d1，及其导数依次应用排中律，m次，生成一个序列d1=e0，dJ1He1，dJ1HdJ2He2，J. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-257221一BABD3D4BA B A Bdd1'd2'e2图9.第九条。应用排除中间来创建超级图。.DJ1HDJ2HDJ3. He m−1，dJ1HdJ2HdJ3. DJmHe m.Z中的区域在em和目标组件d2中具有匹配的蜘蛛和阴影。其他区域在em中的蜘蛛和阴影至少与d2中的一样多。因此em是d2的超图。从这个意义上说，应用排中图后的复合图D1-D更接近于DC。例如，在图9中，d1和d3具有m（d1，d3）= 2。为了将d1转换为d3，我们需要在A区域中添加蜘蛛，而不是B区域，并在A和B区域中添加阴影。排中律的两个应用可以用来把这些元素加到d1上，得到dJ1HdJ2He2。图dJ1和dJ2都与d3相矛盾：dJ1在d3的阴影区域中包含更多的蜘蛛，而dJ2在d3的阴影区域中包含更多的蜘蛛。而且，图d1与图d4矛盾.因为我们在创建dJ1和dJ2时没有擦除元素，所以dJ1和dJ2也与d4矛盾。为了确保算法的终止，必须考虑每个中间图DJ1，..，dJm. 回想一下，我们正在改变D1的单位，直到它的所有酉成分都是某些DC的分量或DC的某个分量与DC矛盾。通过2 1 2将排中律应用于d1，我们用一个析取替换d1，一元图这些新的图之一，em，是d2的超级图。其它分量dj1，.，dJm与D C比d 1有更多的幺正分量相矛盾，正如我们现在所示。如果d1与d矛盾在DC中，则所有dJ都与d矛盾。此外，每个dJ都是相反的，2i i用d2表示。这可以通过注意区域z的存在来看出，的(i) z在DJi中被阴影化，而在d2中不被阴影化，或者(ii) z在DJi中比在d2中恰好多一个蜘蛛。一258J. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-222►n24 0 03 0 02 0 01 0 000 1 0 02 0 03 0 04 0 05 0 0n 2图10个。原始数据和显示每个比率频率的直方图如果z在DJi中有阴影，那么z在d2中包含更多的蜘蛛。如果z在DJi中恰好包含一个蜘蛛，则z在d2中被阴影化。因此，对于每个DJi，在DC中存在比d1更多的矛盾分量。等价地，对于每个dJi，DC的酉分量dJjj比对于d1，m（dJi，dJjJ）是有限的酉分量d j j少。因为在DC中只有有限个酉分量，所以算法将终止。定理4.2可判定性设D1和D2为蜘蛛图.有一种算法可以确定D1是否等于D2.4.4实证结果为了证明我们在本文中提出的证明写作算法比[ 8 ]中的完备性证明推导出的算法更有效，我们生成了一个随机样本（大小n= 4000），这些样本是成对的“小”图，D1和D2，其中D1 ≠ D2。小的意思是有很少的轮廓（每个酉图中≤ 3个）和很少的酉部分（≤4个）。一旦我们随机生成了D1，我们（随机）对D1应用一系列推理规则，得到D2。然后我们用这些图中的每一对，用每一种算法，构造出D1D2对于每一对图，我们计算了比率n1，其中n1是从我们提出的算法生成的证明的长度，n2是从完备性证明产生的算法生成的证明的长度。原始数据的散点图和显示所得比率及其频率的直方图见图10。我们发现，我们提出的算法创建，平均而言，不到35%的证明步骤，算法产生的完整性证明创建。5 0 04 0 03 0 02 0 01 0 006007000800 1n 1/ n 22n 1Fre q u e n c yJ. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-259*Dialdre nuOnrdCDoimapgoAB5执行上面给出的算法已经用java实现，可以从[19]下载。该应用程序允许用户创建和编辑图表。图是由它们的抽象语法而不是它们的具体语法表示的（参见[8]）。这意味着一个图仅仅是根据它所拥有的标签、区域、阴影和蜘蛛来建模的每个区域都根据其内部和外部的轮廓进行建模对于酉图，用户指定轮廓集，区域集，阴影和蜘蛛。区域在屏幕上显示为其所在轮廓的列表。图11中的图对用户来说将表现为：等高线：[A，B]区域：[外部，A，B]阴影区域：[B]蜘蛛：[[A]，[A]，[A，B]]。见图11。 一张图表：从具体到抽象。复合图可以从它们的单一组件构建。图12所示的复合模式用于构建复合图。类型为OrCompoundDiagram和AndCompoundDiagram的对象保存其他图对象的集合，称为其子对象。图d1H（d2Hd3）的类型为AndCompoundDiagram，具有两个子级，一个用于图d1，另一个类型为OrCompoundDiagram，具有子级d2和d3。二、.中希gr amnUdnDiitagryaDmiagram或ruanmdDiagram图12个。复合图的复合模式在实现过程中做出的一个决定是尽可能地扁平化复合图结构。从复合模式构建的对象结构包括具有子级的AndCompoundDiagramAn d CompCo mp o u260J. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-HH包含其他图表对象。原则上，AndCompoundDiagram可以有一个子对象，它是另一个AndCompoundDiagram对象，表示D1（D2D3）.但是在实现中，这些结构立即被分配到一个单独的AndCompoundDiagram对象中，并具有组合的子对象集：D1HD2HD3。因此，我们不实现关联规则。最后，我们考虑一个复合图的孩子的集合作为一个无序的集合。之所以做出这个决定，是因为一组子元素的具体图示表示可能无法显示组件之间的明确顺序因此，我们不执行交换规则。图十三.上下文相关菜单。图14. 自动生成的证明。该工具允许用户构建自己的证明，防止规则的错误应用。通过在用户界面上使用上下文敏感菜单来防止不正确的应用：仅选择可应用于图的规则，参见图13。此外，该工具可以自动生成证明，给出前提和结论。如果存在证明，则向用户呈现一个证明，否则给出一个反例（参见图1A和1B）。14和15）。对于许多示例，自动生成的证明不是最短的，并且用户可能希望自己编写证明。当将此工具扩展到更具表达性、可能不可判定的图形语言时，J. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-261图15.自动生成的反例。决策程序可能不存在。因此，它可能是更有用的用户编写自己的证明。6结论和进一步工作在本文中，我们描述了一个工具，支持推理与蜘蛛diagrams。该工具允许用户构建自己的证明，并在任何给定的证明步骤中，只向用户提供有效的规则应用程序另外，给定D1和D2，它可以构造D1蕴涵D2的证明或反例。自动生成的证明比使用直接从[8]中的完备性证明导出的算法生成的证明要短得多。我们的计划是将本文的工作扩展到更具表现力的约束图推理系统。理想情况下，我们将能够找到并实现一种算法来构造约束图的证明或反例约束图是否表达了一阶谓词逻辑的可判定片段还不清楚 众所周知，蜘蛛图语言是等价的，一元一阶逻辑与等式的表达能力[14]。约束图符号的限制形式，包括箭头和通用蜘蛛，产生可判定系统[13]。当我们进一步扩展符号，增加表达能力时，就有牺牲可判定性的风险一个启发式的方法来生成更短的证明已经开发了酉图之间的证明[4]。启发式算法搜索长度小于给定限制的证明。如果它没有找到证据，可能是因为需要更多的步骤，或者因为不存在证据。当启发式方法无法找到证明时，这里概述的算法是必不可少的。在任何情况下，启发式算法不搜索复合图之间的证明262J. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-目前，我们的工具的输出以文本形式出现，而不是以语法形式出现。为了向用户展示一系列绘制的图表，我们需要从抽象描述中创建图表。文[3]给出了从抽象描述中绘制一类蜘蛛图的算法。使用迭代方法和布局度量[5]改进了图布局的质量。到目前为止在布局方面所做的工作解决了在证明中不考虑上下文而绘制图表的问题需要对证明序列的绘制策略进行更多的研究，以便在应用规则后，图表看起来非常相似，突出显示应用规则所做的更改我们的目标是开发一套应用程序，包括图表查看器，编辑器和证明写作环境，包括自动证明写作。这样的工具可以集成到UML环境中，就像[17]中的Key项目的图解版本，它将OCL证明义务和自动证明生成构建到TogetherControl Center CASE工具中。引用[1] 阿马蒂湾和I.吴文，概念图与一阶逻辑，计算机学报，43（1），1-12页[2] Fish，A.，李文，一种基于约束图的算法，计算机视觉技术，北京，2003。[3] Flower，J.，和J. Howse，Generating Euler diagrams，In Proceedings of Diagrams 2002，pages 61-75，Springer-Verlag，2002。[4] Flower，J.，J. Mastho和G. Stapleton，Generating readable proofs：A heuristic approach totheorem proofing with spier diagrams ， Submitted to 3rd International Conference ，Diagrams 2004，Cambridge，2004。[5] Flower，J.，张文，张文龙，张文龙，2003。[6] 吉 尔 ， J. ， J. Howse 和 S. Kent ， Formalising spider diagrams ， In Proceedings of IEEESymposium on Visual Languages（VL99），pages 130-137，IEEE Computer Society Press，1999.[7] Howse，J.，F. Molina和J. Taylor，SD 2：一个健全而完整的图形推理系统，IEEE Symposiumon Visual Languages（VL 2000），IEEE Computer Society Press，第127-136页，2000年。[8] Howse， J. ，G. Stapleton and J. Taylor ， Spider diagrams ， In preparation ， to appear ：www.cmis.brighton.ac.uk/research/vmg.[9] Niniméaki，M.，理解概念语法的语义，清华大学计算机科学系，http://www.cs.uta.fi/reports/pdf/A-1999-4.pdf，1999。[10] 使用概念图进行知识表示的在线课程，http://www.hum.auc。dk/cg/，由丹麦奥尔堡大学传播系人文信息学和南丹麦大学信息科学Flexnet项目制作。[11] 申J.， “The logical status of diagrams,”J. Flower，G. Stapleton / Electronic Notes in Theoretical Computer Science 91（2004）246-263[12] Sowa，J.F.，概念图摘要，在概念结构：当前的研究和实践，P。Eklund，T.Nagle，J.Nagle和L.Gerholz编，Ellis Horwood，pp.三比五十二，一九九二年[13] Stapleton，G.，J. Howse和J. Taylor，一个约束图推理系统，在第九届分布式多媒体系统国际会议论文集，视觉语言和计算国际会议，第263-270页，迈阿密，2003年。[14] Stapleton，G.，J. Howse、J. Taylor和S.汤普森蜘蛛图能说明什么？提交给第三届国际会议，2004年图表，剑桥，2004年。[15] Swoboda，N.，实现欧拉/维恩推理系统，在图解表示和推理，安德森，M。迈耶湾，和Oliver，P.，编，Springer-Verlag，2001。[16] Swoboda，N.和G.Allwein，异构推理系统的设计和实现的案例研究基于模型的推理的逻辑和计算方面，Manani，L.，和新泽西州的内尔塞西安，编，Kluwer Academic，2002年。[17] 卡尔斯鲁厄大学逻辑、复杂性和演绎系统研究所（Institute of Logic，Complexity and DeductiveSystems）http://i12www.ira.uka.de/密钥。[18] Venn，J.，论命题和推理的图解和机械表示菲尔·麦格1880年[19] 的视觉建模组网站，可执行Java程序可用从http://www.cmis.brighton.ac.uk/research/vmg网站。