基于规则的演绎系统中，如何表示和推演证明对象的问题

理论计算机科学电子笔记93（2004）161-182www.elsevier.com/locate/entcsρ测井的推导与表示Mircea Marin米尔恰·马林1，3奥地利科学院约翰·拉东计算与应用数学研究所奥地利林茨Florina Piroi弗洛琳娜·皮洛伊2，4约翰内斯·开普勒大学符号计算研究所哈根贝格摘要我们描述的演绎和证明演示功能的规则为基础的系统中实现的MATHEMATICA。系统可以计算证明对象，证明对象是演绎推导的内部表示，其尊重用户给出的规范。它还可以以人类可读的格式在各种细节级别上可视化这些推论。计算证明对象的表示是以自然语言风格完成的，这种风格是从T定理的证明表示风格中派生出来的，并根据我们的需要进行了简化。关键词：基于规则的演绎，证明呈现，重写。1介绍数学知识管理的主要问题之一是将来自各种数学来源的知识以一种适合于检验和推导新的数学结果的方式进行结构化。一种很有前途的方法1米尔恰·马林得到奥地利科学院的支持。2Florina Piroi得到了奥地利科学基金会FWF的资助，基金编号为F1302。3电子邮件：Mircea. oeaw.ac.at4电子邮件地址：fpiroi@risc.uni-linz.ac.at1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2003.12.033162M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182为了解决这个问题，将知识表示为变换规则的集合，并且通过用户定义的策略来控制对新结果的查找新结果的导出由一系列转换步骤见证，其中每个步骤都是转换规则的实例。策略的目的是通过对构成它们的规则应用程序的序列施加规则结构来这种方法的成功依赖于具有规则和策略的编程原语的系统的可用性。为此，我们开发了一个编程系统ρLOG。ρLOG是基于规则的编程系统FUN LOG的重命 名 版 本 [7 ， 8] 。 我 们 这 样 做 是 为 了 避 免 将 其 与 80 年 代 的 编 程 系 统FUNESCO[13ρLOG是一个合适的环境，用于在基于规则的语言中指定和实现演绎系统，其应用由用户定义的策略控制。更准确地说，ρLOG允许：• 通过使用MATHEMATICA的高级功能对非确定性计算进行编程[15]，例如与序列模式匹配，以及访问最先进的符号和数值计算方法库• 对规则l进行编程，其归约关系→l可以根据已经定义的归约关系→l1，...，→ln;• 对于给定的表达式E和规则l，询问是否存在表达式x，使得导出关系E→lx成立。我们表示这样一个查询由？x：E→1x。• 生成证明对象，该证明对象对决定公式E→lx的有效性的推论进行编码。该系统有能力以人类可读的格式，在各种细节水平我们决定在MATHEMATICA中实现ρLOG，主要是因为这个计算机代数系统具有模式匹配和转换规则计算的高级功能。这些特性提供了良好的支持来实现一个完全基于规则的系统。 MATHEMATICAalso o a非常好的支持符号和数值计算。另一个原因是基于规则的编程，正如我们所设想的，可以有效地用于实现证明器，求解器和简化器，然后可以集成到THEOREMA框架中[3]。由于T定理是在MATHEMATICA中实现的，因此一个强大的基于规则的系统的MATHEMATICA实现可能成为T定理开发人员的方便编程工具。我们参考[10]以获得对我们系统编程能力的完整描述，并参考[15]以获得对MATHEMATICA的模式匹配构造的描述。下面的例子显示了一个可以减少一个关于ρLOG的查询，以及我们如何用ρLOG找到一个解。M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182163例1.1考虑函数f1：（−∞，0）→R，f2：（−∞，1）→R，g：（0，∞）→R定义为f1（x）=x+ 7，f2（x）=x+ 4，g（x）=x/ 2。现在考虑非确定性运算f：（−∞，1）→R，定义为：如果x0，f（x）=如果x为1，则f= 2（x）。我们想编写一个规则，它对所有x ∈ R的g（f（x））的部分定义和非确定性计算进行编码。首先，我们将函数f1，f2和g编码为ρLOG变换规则“f1”、“f2”和“g”：DeclareRule[xReal/; （ x0 ） ： →x+ 7 ，“f1”];DeclareRule[xReal/; （ x1 ） ： →x+4，“f2”];DeclareRule[xReal/;（x>0）：→x/2，“g”];每 次 调 用 DeclareRule[patt ： →rhs ， l] 都 会 声 明 一 个 新 的 规 则 patt ：→rhs，命名为l以备后用。构造xReal指定代表实值的模式变量x在这个例子中，所有的模式都有对允许值施加附加约束的边条件，X.例如，规则“f1”要求x的值为负数（x0）。对于与规则l相关联的约化关系，我们把它写成→l。例如，我们有0。5→“f2”4。5因为0 5是一个小于1的实数，可以用 0 替换为“f2”。5+4 = 4。五、呼叫设置[“f1”|“f2”，“f”];声明规则“f”，其归约关系符合→“f1”→“f2”因此，它对f的计算进行编码。呼叫SetPoint[“f”表示“g”，“fg”];声明规则“fg”，其关联的归约关系→“fg”与关系→“f”和→“g”的合成→“f”→“g”一致。[5]很明显，x→“fg”r i r是计算g（f（x））的一个可能结果。因此，规则“fg”编码了我们所寻找的计算。调用ApplyRule[E，“fg”]询问系统是否决定，给定表达式E，运算g（f（E））是否定义。如果定义了操作，则调用产生一个可能的结果，否则返回E5注意，规则composition“f”“g”与compositionfg如数学中所理解的那样，而是到组成gf。164M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182未经评估。 例如，调用：ApplyRule[-7. 1，“fg”]返回-7。1，因为$x，y：（−7. 1→“f”y）n（y→“g”x），以及ApplyRule [0. 2，“fg”]返回3. 6、因为（0）2→“f”7. 2）（7. 2→“g”3。6）。Q本文其余部分的结构如下。第2节描述了ρLOG的主要编程原理和构造。在第三节中，我们描述了ρLOG中演绎导子的一般结构。第四节是证明对象，证明对象构成演绎推导的内在表征第5节介绍了ρLOG提供的操作证明对象的方法，并以人类可读的方式查看编码的基于规则的证明。格式.第6节结束。2方案拟订原则在这一节中，我们介绍了ρLOG规则，ρ-有效表达式的概念，并描述了如何组合和应用规则。2.1规则和表达式规则是ρLOG的主要编程概念。它们指定部分定义和非确定性计算。形式上，一个规则是一个表达式l：：patt：→rhs，其中l是规则名，patt是一个模式表达式，rhs指定了一个可能不确定的计算，根据patt中出现的变量。规则的主要用途是将它们应用于表达式。任何可以用MATHEMATICA[15]语言表示的表达式都是ρLOG的有效输入表达式。 此外，表达式可以包含一个区别于选定子表达式的数量ρLOG的当前实现是能够对具有所选子表达式E1，...，n，使得Ei+1是Ei的子表达式，只要1 ≤in<。这样的表达式称为ρ-有效的。因此，对ρLOG的当前实现有意义的表达式最多有一个最里面的选择子表达式。当我们想要强调一个ρ-有效的表达式E具有最里面的选择子表达式E J时，我们将写E [[E J]]。当E没有选择的子表达式时，我们也可以写E [[E]]，而表达式E[[EJ/EJJ]]M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182165从E[[EJ]通过将区分的子表达式EJ替换为子表达式EJ J而获得。表示法E[[E]是不明确的：要么E没有选择的子表达式，要么E本身被选择。我们允许这种模糊性，因为它在我们的框架中是无害的。在说明性示例中，我们将简单地对所选择表达式的子表达式，如下所示示例2.1使用表达式E1= f[f[x，e]，e]，E2= f[x，e]，E3= f[f[f[x，e]，x]，y]，E4= f[f[x，e]，f[e，x]]。E1，E2，E3是ρ-有效的，而E4不是ρ-有效的，因为它有两个最里面的选择子表达式。我们可以写E1[[E1]]、E2[[E2]]和E3[[f[x，e]，以给出这些表达式的最里面的我们有E1[[E1/z]]=z，E2[[E2/z]]=z，E3[[f [x，e]/z]]=f [f [z，x]，y].Q在下文中，我们将隐含地假设E，EJ，EJJ，E1，E2，.. . 表示ρ-有效表达式和l，LJ，l1，l2，. . . 表示ρLOG规则。2.2规则应用有两个过程调用触发规则l在ρ有效表达式E上的应用：ApplyRule [E，l]和ApplyRuleList [E，l]。第一个调用试图通过查看E的最里面的选定子表达式（如果有的话），在E上应用已经声明的规则l：：patt：→rhs。ApplyRule[E，l]计算• E1= E [[EJ/EJJ]]，如果我们有E [[EJ]，并且可以识别θ（patt）= EJ的替换θ，并且可以执行计算θ（rhs）以产生结果EJJ。在这种情况下，我们写E→1E1。• E，否则。 在这种情况下，我们写E/→l。我们强调二元关系→l可能不是一对一的，因为（1）匹配替换θ（patt）=EJ不是唯一的，或者(2) 可能有一种以上的可能性来评估实例θ（rhs）得到一个结果（如例1.1）。这两个非决定论的来源在[10]中有更详细的讨论。调用ApplyRuleList [E，l]将计算可能为空的ρ-有效表达式列表{EJ|E→IEJ}。166M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182L1L12.3合并规则ρLOG的编程原语是基本规则。 这些被命名为通过调用声明的MATHEMATICADeclareRule[patt：→rhs，l]其中patt：→rhs是一个转换规则的MATHEMATICA规范[15]，l是一个唯一标识新声明的规则的字符串规则可以组合成更复杂的规则。ρLOG为程序规则提供了以下组合子：choice：如果l1，.，ln是规则，则l1|......这是什么？|...|... |ln E2i对于某个1≤i≤n，E1→liE2合成：如果l1，l2是规则，则l1<$l2是规则，其中E1→l1<$l2E2i <$存在E使得E1→l1E和E→l2E2，反射性封闭：如果l1，l2是规则，则n个Repeat[l1，l2]是规则有E1→Repeat[l，l]E2i <$n存在E使得E1→<$nE和E→lE2.我们写→12升12对于→ l1的自反传递闭包。类似地，Until[l2，l1]是一个规则，其具有如下的对称旋转序列：Repeat[l1，l2];唯一的区别是Repeat[l1，l2]适用于l1，因为对于l 2来说，重复次数最多，而对于l 2来说，重复次数最多，直到l2适用为止。范式：如果l是一个规则，那么NF[l]是一个规则，其中E1→NF[l]E2iE1→E2且E2/→l。此外，E→ NFQ[1]E i = Ei →1。重写规则：如果l1是一个规则，那么我们可以引入规则l，其中E→lE1i，其中存在E的子表达式EJ，使得EJ→lEJJ，并且E1= E[[EJ/EJJ]]。l被称为由l诱导的重写规则。重写的操作语义取决于l1可以作用于的子表达式的选择可以通过RWRule[]调用来引入规则及其选择策略（参见下一节。）为了使规则的组合更简单、更直观，我们可以通过SetPoint []调用来定义别名，就像我们在例1.1中所做的那样。2.4重写现在我们继续描述如何在ρLOG中实现重写。重写步骤可以看作是两个步骤的组合：一个步骤选择要重写的子表达式，然后是另一个步骤重写它。为了获得合适的重写选择策略，我们设计了两种规则：M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182167我(i) 基本规则“Rw”，其关系是E [[EJ]] →“Rw”E [[EJ/EJ]]。 这意味着我们将选择添加到E的最里面的选定子表达式。如果E没有选择的子表达式，那么我们将选择作为一个整体添加到它(ii) 选择移位规则，可以在最内层选定子表达式的适当子表达式上移位最内层的选择。选择移位规则对于浏览表达式的子表达式非常重要，直到我们到达一个可以重写的子表达式。形式上，选择移位规则l由可计算函数移位l和规则rl，使得E1→lE2I∈shiftl[E1]su chthatEJ→rlE2.显然，移 位 [E1]是每 个 输 入 E1 的 值 列 表。ρLOG只有一个内置的选择移位规则SEL[l]，其适用于行为被定义为调用RWRule [l1，l，Traffic→val，Traffic→ {f1，. ，fn}]（1），其中val∈ {“LeftIn”，“LeftOut”}和{f1，. ，fn}是一个MATHEMATICA符号. 选项Traffic定义重写规则的选择策略Traffic→“LeftIn”将使选择过程按照从左到内的顺序查找输入表达式的子表达式，而使用Traffic→“LeftOut”将按最左-最外的顺序查找当给定一个符号列表{f1，. ，fn}，则选择过程将忽略表达式的子表达式，其中最外面的符号是f1，.，fn.默认值为{}，即，可以选择任何子表达式，并且可以在任何地方执行重写调用（1）除了声明l是由l1诱导的重写规则之外，还声明选择移位规则SEL[l]与由下式定义的可计算函数移位SEL[l]相关联：{E J， . . ，EJ}，如果EJ=f[E1， . . ，Em]with移位SEL[l]1[E[[EJ]=Mf/∈ {f1，.，fn}，并且EJ=E[[EJ/f[E1， . . ，Ei， . . . ，Em]对于所有i∈ {1，.，m}，有了规则{}否则第1章|SEL [l] if val =“LeftOut”，rSEL[l]=0SEL [l]|如果val=“LeftIn”，则为l 1。168M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182“集团”调用（1）还将递归定义l=“Rw”rSEL[l]添加到会议记录。在本文中，我们将始终假设rl和移位L表示规则和与SE相关联的可计算函数选择移位规则例2.2考虑声明DeclareRule[f[x，e]：→x，“N“];RWRule[“N”，“N*”，Traffic→“LeftOut”];并且I∈E=f[f[x，e]，y]。 nE→“N*“f[x，y]导致以下结果：“N*”可以将d还原 为 “Rw“rSEL[“N*”] ， 并 且 E→“Rw“f[f[x ， e] ， y];n 我 们 使 kef[f[x ， e] ，y]∈shiftSEL[“N*”][f[x，e]，y]]，并且应用rSEL[“N*”]=“N“|SEL[“N*“];我们选择交替的“N“，并计算f[f[x，e]，y]→“N“f[x，y]。Q选择移位规则也可以由用户定义，但目前的方法相当繁琐。我们正在努力扩展ρLOG的实际实现，为选择移位规则提供一个方便的定义机制现在我们将举一个例子来说明ρLOG如何可以用作一个演绎系统。例2.3 [群论中的可连接性检验]考虑具有结合运算f、右中立元e和逆运算i的非交换群的公理。 这些公理可以用ρL OG规则编码如下：声明规则e[f[f[x， y]， z]：→f[x，f[y，z]]，“A“];DeclareRule[f[x，e]：→x，“N“];DeclareRule[f[x，i[x]]：→e，“I“];调用SetPoint [“A”]|“N”|“I”，“G”]将“G”定义为组合规则“A”的别名|“N”|“我”由“G”引起的重写关系由下式声明：RWRule[“G”，“Group”];关系→“组”是终止的，但不是连续的，因为f[f[x，e]，x]→“群“f[x，x]/→“群“;f[f[x，e]，x]→“群“f[x，f[e，x]]/→“群”和f[x，x]f[x，f[e，x]]。在这里，如果两个项s和t是可连接要求系统地搜索项u，使得s→nu和M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182169∗“集团”联合以ρLLOG为单位对可连接性测试进行编程的一种简单方法是：DeclareRule[eq[x，x]：→True，“Eq”];SetPoint[Until[“Eq”，“Group”]，“Join”];ApplyRule[eq[s，t]，“Join”]如果s和t是可连接的，则最后一个调用返回True，否则返回eq[s，t]。如果我们想看到一个公正的结果，我们可以调用ApplyRule[eq[s，t]，“Join”，TraceStyle→“Compact”];这个调用将生成一个MATHEMATICANotebook，其中包含一个人类可读的底层演 绎 推 导 的 表 示 。 图 1 给 出 了 这 样 的 注 释 ， 其 中 s=f[f[x ， e] ，i[x]] 和t=f[f[e，y]，i[y]]。QFig. 1.基于规则的演绎的“紧凑”我们总结本节，提出以下意见：(i) 将规则应用于整个表达式或表达式的选定子表达式，(ii) 规则应用是非确定性操作，(iii) 规则应用是部分定义的操作，(iv) 规则可以通过各种组合子组合成更复杂的规则t→170M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182我3演绎树直观地说，演绎树（简称D树）是规则应用程序查询的有效性检查的跟踪？x：E→lx，其中给出了ρ-有效表达式E和规则l.一个D-树的建设收益，通过连续减少查询？x：E→lx到有限个简单的查询。这个简化过程是由一组推理规则的应用程序驱动的我们描述我们的推理规则如下：S1.. .Sn你说呢？x：E→lx（二）其中Si（1≤i≤n）是（a）形式为n的查询？x：Ei→li x，或（b）形式为Ei→LEJ的有效约化，或（c）形式为Ei→lJEj？x：EJ→l 其中，Ei→l EJ是一个有效的约简。 我们写i i1 2i[[Si]对于通过删除“？”上标来自Si.有了这个约定，我们系统的每个推理规则将具有以下含义：X：E→IXI X[S1]或.或[Sn]]。在逐一描述推理规则之前，我们想先讨论例2.2中默认使用的规则归约问题，并定义一些辅助概念。如果一个规则是基本的或形式NFQ[11]，则它是基本的。我们在此提醒，“Rw”是一个内置的基本规则。l的约简，记为red[l]，是一条规则，它的适用性与l的适用性一致。这意味着，对于所有的E，E→lEJi E→红色[l]E J。如果l/=red[l]，则规则l是可约的，否则是不可约的。基于red[ ]的定义（在[10]中详细描述），我们可以通过以下方式定义一个有充分根据的关系>：l>lJi lJ=红色[l] 并且lj = LJ。减少查询？x：E→lx到一个更简单的查询是通过使用函数red[]尽可能地减少l来完成的，直到我们到达一个我们试图应用于E的不可约规则。我们最终得到一个不可约规则的事实是由>的良基性保证的。我们现在继续描述推理规则。M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-18217111 2 12(i) 如果l是可约的，那么相应的推理规则是：你说呢？x：E→红色[l]x你说呢？x：E→lx(ii) 如果l是初等的，那么相应的推理规则是：E→ 1 E1..E→ l E n你说呢？x：E→lx其中E1，...，En都是使得E→1Ei的表达式。(iii) 如果l是l1|......这是什么？ |则相应的推理规则为你说呢？x：E →lx.你说呢？x：E→lnx你说呢？x：E→l1|... |ln x(iv) 如果l是选择移位规则，则对应的推理规则是：你说呢？x：E1→ rlx.你说呢？x：En→rlx你说呢？x：E→lx当r e{E1， . . ，En}=shift1[E]。(v) l是l1<$l2，其中l1是基本的或选择移位规则。如果l1是初等的，那么相应的推理规则是：（E→l E1）（？x：E1→l （x）...（E→l En）（？x：En→l x）你说呢？x：E→l1l2x其中E1，...，En（n≥ 0）都是使得E→11Ei.如果l1是选择移位规则，则对应的推理规则是：你说呢？x：E1→rl1 <$l2x.你说呢？x：En→rl1<$l2x你说呢？x：E→l1l2x其中{E1，.，En}=移位11 [E]。red[ ]和规则组合子的定义保证了这些推理规则覆盖了查询形状的所有可能情况查询的D树是什么？x：E→lx，记为T（E，l），通过连续应用上面定义的六个推理规则很容易看出，D-树T（E，l）对于E和l的某些值可能是无限的。考虑表达式E=A<$B和规则“"：：X<$Y：→Y<$X，172M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182那么，D-树T（E，l）对于？x：E→“”x如下.AB→“” BABA→“” ABAB→““BABA →”“ AB为了避免生成这样的无限结构，我们将系统限制为部分D树的构造，这些部分D树是通过限制沿着树的分支的推理应用的最大数量而形式上，查询的最大深度m的部分D树Tm（E，l）你说呢？x：E→lx，定义为：T0（E，l）：：=？x：E→lxTm+1（E，1）：：=E →1 E1 .E→lEn你说呢？x：E→lxTm+1（E，red[l]）l初等|∃? x：E→lxl可约|Tm(E, l1)...Tm（E，ln）你说呢？x：E→lxL =l1 | ... | l n|(E →l1 E1 ) ∧ Tm(E1, l2 ) ... （E→l1Ek）Tm（Ek，l2）你说呢？x：E→lxT m（EJ，r l）...T m（EJ，r l）l=l1l2l1小学l=l1|11n1你说呢？x：E→lxT m（E J，r l l l2） ......这是什么？T m（E J，r l◦ l2）l1选择移位l=l1l2|11K1你说呢？x：E→lxl1选择换挡规律其中k，m∈N且{E，J，.，EJ}=移位I[E]。 这样的部分D树是1k1通过连续应用前面定义的推论直到m得到的在每一个分支上。当计算D树的深度时，不考虑类型（i）的推断步骤在后续中，我们将省略表达式E，规则l和深度m从（部分）D-树Tm（E，l）的符号，只要我们认为它不相关。以下部分D树的分类与解释存储在其结构中的数据成功D-树是一个部分D-树，它至少有一个叶节点，通过应用类型（ii）的推理规则计算，其中n≥1。失败D树是通过应用类型（ii）的推理规则（n≥1）计算的没有叶节点的D树。M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182173挂起D树是一种部分D树，它既不是成功D树，也不是失败D树。部分D-树Tm（E，l）的含义是：如果Tm（E，l）是成功D-树，则$x：E→lx;如果Tm（E，l）是失败D-树，则$ x：E→lx4证明对象在自动推理中使用证明对象的两个最常被引用的原因，以及ρLOG实现其中一个的原因，是：• 保存证明人活动的完整记录• 为用户提供指导（证明对象的图形/自然语言显示）。在推理系统中具有证明对象的其他原因是提取证明策略，稍后检查，提取算法和计算方法。ODS等。[14 ]第10段。ρLOG的证明对象部分D树都是ρLOG的证明对象旨在成为部分D-树结构的紧凑且更明确的表示。它们由以下语法定义：N：：=$SNODE[{E，l，EJ}]| $SNODE [{E , lexpr }, N1,...，Nn]| $FNODE [{E, lexpr}]| $FNODE [{E , lexpr }, N1,...，Nn]| $PNODE [{E , lexpr }, N1,...，Nn]| $EPNODE [{E, lexpr}]lexpr：：= l| {11，.，ln}| 1991年，E.一个成功对象是一个证明对象，格式为$SNODE [. . ]中。成功对象是成功D树的编码，因此它们证明了公式的有效性式（E→l1EJ）<$（Ex：EJ→l2x）的。失败对象是一个形式为$FNODE [. . ].失败对象编码失败D树，因此它们证明公式$x：E→lx或逻辑合取（E→l1EJ）<$（$x：EJ→l2 x）的一种形式。挂起对象是形式为$EPNODE [.]的证明对象。. ]或$PNODE [.. . ].格式为$EPNODE [. . ]被称为基本待定对象，它们对应于D-树的对象，当174M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182LLL达到搜索的深度限制。 对应于挂起的D-树Tm（E，l）的挂起对象证明了这样一个事实，即直到深度m的穷举搜索不足以决定公式Ex：E→lx的有效性。4.1编码过程我们将部分D-树T的编码表示为T。我们将展示如何根据T的部分D-子树递归地定义部分D-树T的编码函数。令Tm是深度为m的部分D-树，d是搜索深度限制。对于T m的证明对象的计算如下进行：(i) 如果Tm不知道？x：E→x，其中m< d，则{\displaystyle\mathbb {T}=$FNODE [{E，l}]。(ii) 否则，如果Tm不？x：E→ x，m = d，则Tm是部分D树最大搜索深度，并且最大搜索深度=$EPNODE [{E，l}]。(iii) 否则，如果TE→lE1.. . E→lEn当n>0时，你好？x：E→x.⟨⟨Tm⟩⟩=$SNODE[{E，l，E1}]如果n= 1，$SNODE [{E，l}，$SNODE [{E，l，E1}]，. ......你好。，$SNODE [{E，l，En}]]，如果n> 1。(iv) 否则，如果存在部分D-树的序列T1，.，Tn的深度最大为m，使得Tm=T1（E，l），li+1=red[li]，Ti（E，li）=Ti+1（E，红色[li]）你说呢？x：E→lix对于1≤i n和Tn（E，ln）Tn，1...Tn，k你说呢？x：E→lnx其中ln不可约，Tn，i为深度mostm− 1，则有以下情况：• 如果有i∈ {1，.，k}使得Tn，i是成功D-树，则SNODE [{E，{11，. ，ln}}，{\displaystyle {\frac {T}n，1}}，. ，T n，k]• 如果所有Tn，1，.，Tn，k是失败D-树，则节点Tm节点=$FNODE [{E，{l1，. ，ln}}，{\displaystyle {\frac {T}n，1}}，. ，T n，k]• 如果有i∈ {1，.，k}，使得Tn，i是未决D树，并且Tn，1，.，Tn，k是成功D树，则PNODE [{E，{11，. ，ln}}，{\displaystyle {\frac {T}n，1}}，. ，T n，k]。M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182175(v) 否则，如果Tm1≤i≤k，则T1... Tk你说呢？x：E→lx其中Ti的深度最多为m−1，• 如果有i∈ {1，.，k}使得Ti是成功D树，则⟨⟨Tm⟩⟩ =$SNODE [{E, l}, ⟨⟨T1⟩⟩,... ，T k]• 如果所有T1，.，Tk是失败D树，则⟨⟨Tm⟩⟩ =$FNODE [{E, l}, ⟨⟨T1⟩⟩,... ，T k]• 如果有i∈ {1，.，k}，使得Ti是待定D树，并且对于所有j∈ {1，.，k} \ {i}，T，j是未决或失败D-树，则PNODE=$PNODE [{E，l}，PNODET1，. ，T k](vi) 否则，Tm（E→l1E1）EBT1. （E→l你说呢？x：E→l1l2xEk）Tk其中Ti在部分D-树的深度最多m-1为m？x：Ei→lx，对于所有1≤i≤k。对于这种情况，我们将使用函数Annotate[E，l，N]，它为表达式E、规则l和证明对象N定义如下：-$SNODE[{E，E1，IJ，E2}]，如果N=$SNODE[{E1，IJ，E2}]，-n[{E，E1，E2，E3}，N1， . . ，Nk]i，如果N=n[{E1，lexpr}，N1， . . ，Nk]withn∈ {$SNODE，$FNODE，$PNODE}。在k= 0的情况下，意味着E1→11，我们有对于k >0的情况，我们有以下子情况：• 如果有i∈ {1，.，k}，使得Ti是成功D树，则T i是$SNODE[{E，l1<$l2}，Annotate[E，l1，注释T1<$l]， . . ，Annotate[E，l1，Ltd.• 如果对于所有i∈ {1，.，k}，Ti是失败D树，则Ti是$FNODE[{E，l1<$l2}，Annotate[E，l1，注释T1<$l]， . . . . ，Annotate[E，l1，Ltd.•如果有i∈ {1，.，k}，使得Ti是待定D树，并且对于所有j∈ {1，.，k} \ {i}，T j是挂起或失败D树，则$PNODE[{E，l1<$l2}，Annotate[E，l1，注释T1<$l]， . . ，Annotate[E，l1，Ltd.下面的示例说明了编码过程在具体情况下的行为。12176M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182例4.1考虑例1.1中声明的规则和查询x：-4。2→“fg”x。 对应的D树是T（−4）。2，“fg”）（-4。2→二、8 →“g”1。4二、8）（-4。2→-0。2）“f1”你说呢？x：2。8→“g”x“f2”你说呢？x：-0。2→“g”x你说呢？x：-4。2→“f1”→“g”x？x：-4。2 →“f2”→“g”x你说呢？x：-4。2 →（“f1”→“g”）|（“f2”）x你说呢？x：-4。2 →（“f1”|“f2”）“g”x你说呢？x：-4。2→“f”→“g”x你说呢？x：-4。2→“fg”x我们通过从叶子向根遍历证明对象来递增地构造它有两种叶子D树：3.第三章。0→“g”1。5T=和 T=一毛钱？x：3。0→“g”x两千块？x：0。 →“g”x与相应的证明对象⟨⟨T1⟩⟩ =$SNODE [{3. 0，“g”，1。5}]和⟨⟨T2⟩⟩ = $FNODE [{0., “g”}]。以T1和T2为直接子树的T的D-子树是T =（−4. 0 →“f1”3。0）T1和T（-4。0→“f2”0。）T2=.三块钱？x：-4。0→“f1”“g”x四块钱？x：-4。0→“f2”“g”x相应的证明对象是⟨⟨T3⟩⟩ =$SNODE [{− 4. 0，0“f1”，3. 0，“g”，1。5}]和⟨⟨T4⟩⟩ =$FNODE [{− 4. 0，0“f2”，0.，“g”}]以编码过程的情况（vi以T3和T4为直接子树的T的D-子树是T3T4T=五块钱？x：-4。0→（“f1”转“g”）|（“f2”）x对应的证明对象是M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182177⟨⟨T5⟩⟩=$SNODE[{−4. 0，（“f1““g“）|（“f1““g”）}，T3，T4]。178M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182下面的D树对应于规则（“f1”转“g”）|（“f2”转“g”），（“f1”|“f2”）“g”，“f”“g”，“fg”其中每个元素都是它后面的元素的约简。因此，通过情况（iv），⟨⟨T ⟩⟩ =$SNODE [−4. 0，{“fg”，“f”“g”，（“f1“）|“f2“）“g“，（“f1““g“）|（“f2““g“）}，T3，T4]。可以容易地检查T具有深度3。Q5可视化和操作ρLog Proof对象在实现了用于存储部分D树的数据结构之后，我们希望以有用的方式查看和处理它。由于速度是我们在设计ρLOG时考虑的主要问题之一，因此默认情况下，系统不会创建证明对象。然而，用户有可能触发它的创建并在不同的表示风格之间进行选择：“对象”风格用于调试;“紧凑”和“冗长”风格用于用户友好的表示。为了实现ρLOG证明对象的自然风格表示，我们调整并简化了THEOREMA系统[3，12]的证明表示例程，该系统还实现了用于存储证明的树型数据结构。我们已经在第1节中看到了ρLOG是如何被调用的。 通过MATHEMATICA的选项 机 制 触 发 不 同 的 呈 现 样 式 [ 15 ， Section 1. 9. 5] 。 ApplyRule [] 和ApplyRuleList []的选项是TraceStyle、MaxDepth和MaxSols。TraceStyle可以具有以下值：• “无” ApplyRule[ ]将只返回一个最终找到的解决方案或原始表达式，如果没有找到解决方案ApplyRuleList[]将返回一个可能为空的解决方案列表。当选择该选项的值时，ρ L og将不会创建任何证明对象。与使用TraceStyle的其他选项创建对象时所需的时间相比，这使得从系统中获得答案所需的时间大大缩短。• “Object”数据结构这可能非常大，检查它需要清楚地了解数据结构是如何定义的（第4节）。•“Compact”MATHEMATICA笔记本与用户友好的介绍部分M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182179证明对象中编码的D树。正如option-value的名字所说，它是重写过程的一个简明表示，跳过了关于减少规则和选择子表达式的所有• “Verbose” 差异在于呈现的信息量。现在向用户显示了减少规则和选择子表达式的步骤。有关此选项的效果的说明，请参见例5.1“紧凑”和“冗长”的表示风格利用了MATHEMATICA的notebook特性，我们在这里提到的最重要的特性是具有嵌套的MaxDepth此选项的目的是避免由搜索空间中无限长分支确定的无限计算。默认值为10000。当TraceStyle具有不同于“None”的值时，MaxDepth的值确定将被创建的证明对象中编码的部分D树的最大深度。MaxSols此选项的目的是对作为查询有效性证明的表达式EJ你说呢？x：E→1x。 例如呼叫ApplyRuleList [E，1，MaxSol →3]找到3个表达式后，将立即停止解决方案搜索过程E1，E2，E3，其中E→1Ei。MaxSols的默认值为∞。这意味着，默认情况下，我们不对要找到的解的数量施加任何上限。ρLOG的一个非常有用的特性是可以进一步扩展编码在证明对象中的未决部分D树，并获得与扩展的部分D树相对应的新证明对象。这可以通过调用int[nums，nums，nums];其中obj是一个证明对象，n∈N是部分D-树的深度限制，这些部分D-树将被计算和编码以替换出现在obj中的基本未决对象。以用户友好的方式创建一个证明对象，不仅可以使用ApplyRule[ ]的TraceStyle选项，还可以通过调用DisplayProof [obj，options];此 时 唯 一 可 用 的 选 项 是 DetailLevel 。 DetailLevel 的 可 能 值 及 其 在DisplayProof []调用中的含义一致180M. Marin，F. Piroi /理论计算机科学电子笔记93（2004）161-182在ApplyRule[]调用中使用TraceStyle。Example 5.1 为 了 说 明 TraceStyle→“Verbose” 的 用 法 ， 我 们 考 虑 了Example1.1中的查询，要求使用“Verbose”表示样式：ApplyRule[-4. 0，“f