电子笔记在理论计算机科学50第3期（2001年）。GT-VMT 2001网址：http://www.elsevier.nl/locate/entcs/volume50.html8页一个支持视觉推理的Agg应用程序1Andrea Formisano2大学数学与信息学系di PerugiaMarta Simeoni3Dipartimento di Informatica，Universita`C a Foscari'di Venezia1引言地图演算，并元关系的算术（参见。[9])是一个基本的方程形式主义，其中人们可以在一个未指定的话语域上陈述二元关系的性质。它可以被看作是关系理论的一种演变，关系理论是一种代数逻辑方法，A. 德摩根角S. Peirce和E. SCHROder[8，7].对人类来说，直接对地图表达式进行代数操作似乎比在一阶逻辑中进行推理要不自然得多;事实上，对于直接基于手的开发来说，它可能显得过于面向机器。然而，当人们诉诸于基于标记图的地图表达式的方便表示除了允许对表达式的非本质特征进行抽象之外，这种表示还允许对地图规范进行简单且直观的视觉处理。例如，在[2，1，3，6]中已经提出了这种方法。在这项工作中，我们移动的第一步实现的自动化工具的机械化视觉地图推理。为此，我们利用Agg|代数图语法|[4]，它为基于图变换的应用程序提供了一个可视化的编程环境。这种应用程序描述的图形文法，其中包括一个初始图和一组图重写规则。Agg支持开始图和重写规则的可视化处理我们使用1 这项研究的部分资金来自意大利IASI-CNR（协调项目日志（SETA））; MURST|PGR-2000;由EC TMR网络GETGRATS（GRAph转换系统的通用理论）;和由Esprit工作组APPLIGRAPH。2 电子邮件：formis@dipmat. 联合国工业发展组织It3 电子邮件：simeoni@dsi. uni ve. Itc2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2DefDef U ==U2的子集p=; p=; p=; ：与 ps，each映射表达式相对应。GT-VMT 2001 { A. Formisano和M. SimeoniAgg作为地图推理的视觉证明助手：推理机制被实现为图重写规则和技术，允许将前提转换为结论（正向推理），或减少论题|目标|转化为更简单的目标，并最终转化为已知的事实（逆向推理）。本文的主题的详细阐述，包括一系列的工作exampes，可以在[5]中找到。2方程规格映射演算基于L，一种没有变量的等式语言它的基本组成部分是三个常数11，;在nitely许多地图字母p1;p2;p3; ：：;三个dydic结构11，4，;的地图interest，地图sym-metricdierence，和地图composition;和monadic结构^的地图转换。映射表达式是以通常方式从该签名构建的任何项。映射等式是Q = R形式的书写，其中Q和R都是映射表达式。一旦一个非空的域U被 xed，映射常量，11，和解释为：=-，1l==2Def UU和=Deff[a;a]：a2Ug. 在一般评价准则的基础1 2 3 i符号P开始指定一个空间映射P=，并且每个ch等于Q=R圈要么是真的要么是假的现在让我们假设'是原子的合取（9 × 1）（9 × k）（L1^^Ln），并且var s （'）fv1;v2; ：g是'中所有变量的集合。更进一步地，假设x1; ：;xk2vars（i），并且eachLi具有xLiPLiyLi的形式，其中xLi;yLi 2var s（'）是变量（假设范围在话语的域U上），PLi 是L的映射表达式。 显然，自由变量可以与存在量化变量混合出现。本文定义了一个“表示”的Agg图G：给定两个αbAN=Def fg和AE=Def f;g;用于节点和边（图形）标记，其中G'= hGE; GN; Gs; Gt; Gle;Glni，其中：GE=Deff1; ：;ng是边的集合 GN=Defvars（'）是n个边的集合Gs：GE！GN将eachi2GEin映射到xLi（源函数）;Gt：GE！GN将eachi2GEin映射到yLi（targetfunction）;G N！N将每个节点映射到唯一可用标签;G le：G E！A E将每条边映射到。Agg图可以归因于Java对象（即Java类的实例，无论是从标准库导入或用户定义的）：我们利用的at-可扩展的机制，以允许适当的操作地图expres- sions。更准确地说，我们引入节点属性函数类型：G N！fB;Fg使得，对于每一个x，type（x）是B（相应地， F）i fx是一个bound（resp. 自由的）可变的。因此，如果相应的3ELi1GT-VMT 2001 { A. Formisano和M. Simeoni变量是绑定在'。 我们进一步考虑了边属性函数Esp：G！L，其将每个边i与映射表达式P相关联。下面的Agg规则明显地保留了所涉及的图的含义，可以组合起来构成一种算法，用于将“展开”图G到给定的（复合）映射表达式P。两个指定的（自由）节点，命名为source和sink，表示P的两个参数，并且每个不同于这两个的节点都被认为是绑定的。请注意，X、Y和P是变量，当左侧的图应用于某个图时，这些变量将使用具体的属性值进行实例化当P由P1、P2（第一规则）、P1、P2（第二规则）和P^2（最后规则）表示时，这些规则是适用的。通过Java方法检查它们的适用性此外，Java方法proj1和proj2分别返回映射表达式P1和P2。代表地图平等。现在让我们扩展我们的方法，以便适当地表示地图等式。为此，我们将关系P的图形表示（即，（xP y））转化为涉及P的等式的表示，通过用泛量子或存在量子来界定源x和汇y下面的等式（显示在左手边），对应于封闭的一阶公式（显示在中间），并通过特定的节点属性值（显示在右手边）在我们的图形符号P P PP=1l;;1l=1l，即，共））的情况下;（8x）（8y））type（一、一、E，NE，类型（y）AEEE4计（P6=，即，总（1l;P为（xPy）（8x）（9y）（xPy）（9x）（9y）（xPy）：（9x）（9y）（xPyx）=type（x）=type（x）=type（x）==类型（y）=类型（y）=type（y）=5GT-VMT 2001 { A. Formisano和M. Simeoni属性函数的类型为：GN！ fB;F;A;E;NEg和表示P的图的源x和汇y根据所要表达的等式来归属。我们把上面列出的四种图分别记为88、89、99和：99。处理互补。为了允许（部分）处理互补，我们引入了边标签：，以表示相关的属性表达式，比如P，必须是互补的。以下是与此约定相关的简单图形重写规则：正如我们将看到的，一个简单的（尽管是部分的），互补的处理，允许一个模型/表示形式P Q的地图包含，因此，描述简单的重写规则推断（新的）地图包含。3一种基于图重写技术的证明辅助系统在我们的上下文中，从适当的公理和已知的定律导出映射等式可以被看作是一种图重写活动。在这里，我们把我们的治疗集中在两个特殊类别的图：存在图的两种类型88和：99。我们分别称它们为正图和负图。这些图被用来表示前提和结论、论题等。从这个角度来看，推理机制被看作是图重写技术：在正向推理中，重写规则用于将前提转换为结论;在反向推理中，重写规则用于减少论题。|“目标”，正如他们通常所说的那样。|更简单的目标，最终，变成已知的，也许是客观的，显而易见的事实。作为一项基本原则，用一个更有要求的目标取代一个积极的目标，用一个不那么有要求的目标取代一个消极的目标是合理的。例如，在一个示例中， 新的属性边可以随意添加到正目标，而边可以从负目标中移除。 解决新的目标，虽然不一定等同于解决以前的目标，但实际上会满足目的。一个否定的前提常常代表一个包含P Q，即，：（9 x）（9 y）（xP\Q y）：如果一个正目标的子图与前提中表示Q的部分相匹配，那么它可以被表示P的部分替换;相反，在一个负目标中，Q可以替换P。从现在开始，为了更具体，让我们只考虑负图6GT-VMT 2001 { A. Formisano和M. Simeoni上面概述的基本规则用Agg图形语言来表述，如图1（1）所示，其中标记为4：和5：的节点（与标记为10：和12：的边一起）构成否定前提;而标记为6：以及9：识别在规则的环期间要被替换的边通知否定前提P Q在变换后的图中保持不变。此外，为了确保规则的健全性，必须附加进一步的条件。实际上，在应用该规则时，否定前提必须与图的完全连通分支匹配。内含物的性质（例如，传递性）很容易确定图2的简单推理规则;图3显示了否定目标的进一步规则。如前所述，在这个可视化框架中证明一个特定的映射相等相当于重复地将相应的图/目标简化为更简单的目标，直到导出已知的事实。与映射包含有关的一些事实或公理是：（A1）P1l， （A 2）PP， （A 3）1lP[P，（A4）;P的值P.一个公理对应于一个Agg产生式，它的左边包含明显的包含，而右边是空的。应用这种产生式会从图中去掉明显的事实我们现在描述一个简单的辅助推理的例子。更确切地说，我们证明了对于任何映射表达式N，以下成立：函数（N^）！1 l;N N=;N ：我们把问题分成两个更简单的命题：（a）1l;NN;N;和(b)函数（N^）！;N1l;NN，下面是通过利用Agg得到的（a）和（b）的证明。(a) 1 l;N的表示N;N 如：99图：在右边我们增加了公理（A4）的一个实例，因为第一步是应用图1的规则（2） 因此，我们得到图(i) 下面，它可以重写成图（ii），通过应用一个规则，实现推广的'德摩根'lawP;T\Q;T=（P[Q）;T。(i)（二）7通过图3的（1）Agg将目标（ii）简化为两个目标：4 这里Func（P）代表映射等于yP\P;=P。8GT-VMT 2001 { A. Formisano和M. Simeoni（一）（二）Fig. 1. 基本推理规则：99目标（一）（二）图二. 映射包含然后分别用（A3）和（A2）立即证明。这就完成了证明的第一部分。(b) 假设Func（N^）可以重写为;N N，并由下面的图（ i）表示;而我们的论文起源于起始图（ ii）9GT-VMT 2001 { A. Formisano和M. Simeoni（一）其中R必须是映射的合成（二）其中R必须是映射的交集图三. 简单的归约规则：99-涉及地图包含的(i)（二）通过应用图3的规则（2）的实例，|在（2）中识别P和Q获得|Agg将论文简化为两个子目标：右边的目标对应于我们的假设Func（N^）;另一个可以进一步简化如下10通过应用第3页的“复合成分”规则。另一步骤通过图3的（1）减少剩余目标，产生两个目标：11GT-VMT 2001 { A. Formisano和M. Simeoni它们分别是（A1）和（A2）的实例。这就完成了证明。4结束语本文报道了在地图表示和推理中实现图形技术的首次尝试。一个有趣的进一步发展将包括设计和实现一个更复杂的证明助手：例如考虑执行回溯或建议用户应用“更好”规则的能力。这些功能的实现可以被认为是实现基于图变换技术的自动地图推理工具的第一步。引用[1] Cantone，D.， A. Formisano，E. G. Omodeo和C. G. Zarba，编译并矢一阶Speci阳离子到映射代数，在：Proc. 第二届AMAST| AMILP2000（2000），pp. 35{54.[2] Chiacchiaretta，A.，A. Formisano和E. G. Omodeo，通过存在多重图进行地图推理，技术。Rep. 05/00，Dip. di Matematica Pura ed Appliata，Univ. diL'Aquila（2000）.[3] Curtis，S.和G. Lowe，计算机程序设计科学，图形证明26（1996），pp.197{216，程序构造的数学，Kloster Irsee。[4] Ermel ， C. ， M. Rudolf 和 G. Taentzer ， Theaggapproach ： LanguageandEnvironment，in：H. Ehrig，G.恩格斯，H.J. Kreowski和G.罗森伯格，编 辑 ， 图 文 法 和 计 算 手 册 的 图 变 换 ， 第 2 卷 。 ， World Scienti c ，Singapore（1999）.[5] Formisano，A.和M. Simeoni，图表和地图：工作中的重写技术，技术。Rep. 2001-01，TU-Berlin（2001年）。[6] 卡 尔 ， W. ， Relational Matching for Graphical Calculi of Relations ，Information Sciences119（1999），pp. 253{273.[7] 马杜克斯河D、关系代数在关系演算的发展和公理化中的起源，StudiaLogica50（1991）。[8] SCHRoder，E.，\VorlesungenberdieAlgebraderLogik（exakteLogik），”B.Teubner，Leipzig，1891{95，[Reprinted by Chelsea Pub.有限公司、NewYork，（1966）]。[9] Tarski，A.和S.Givant，\A formalization of Set Theory without12Variables，”Colloquium Publications41，American MathematicalSociety（1987）.
我的内容管理
展开
