代数等式理论的自动定理证明计算机科学导论第一讲ppt课件

1、代数等式实际的自动定理证明代数等式实际的自动定理证明计算机科学导论第一讲计算机科学导论第一讲计算机科学技术学院计算机科学技术学院陈意云陈意课课 程程 内内 容容 课程内容课程内容 围绕学科实际体系中的模型实际围绕学科实际体系中的模型实际, 程序实际和程序实际和计算实际计算实际 1. 模型实际关怀的问题模型实际关怀的问题 给定模型给定模型M，哪些问题可以由模型，哪些问题可以由模型M处理处理；如何比较模型的表达才干；如何比较模型的表达才干 2. 程序实际关怀的问题程序实际关怀的问题 给定模型给定模型M，如何用模型，如何用模型M处理问题处理问题

2、包括程序设计范型、程序设计言语、程序设包括程序设计范型、程序设计言语、程序设计、方式语义、类型论、程序验证、程序分计、方式语义、类型论、程序验证、程序分析等析等 3. 计算实际关怀的问题计算实际关怀的问题给定模型给定模型M和一类问题和一类问题, 处理该类问题需多处理该类问题需多少资源少资源本次讲座与这些本次讲座与这些内容关系不大内容关系不大课课 程程 内内 容容 本讲座内容本讲座内容 以代数等式实际中的定理证明为例，引见怎以代数等式实际中的定理证明为例，引见怎样从中学生熟知的等式演算方法，构造自动样从中学生熟知的等式演算方法，构造自动定理证明系统，即将问题变为可用计算机求定理证明系统，即将问题

3、变为可用计算机求解解 有助于了解什么是计算思想有助于了解什么是计算思想 计算思想译文计算思想译文 运用计算机科学的根底概念进展问题求解运用计算机科学的根底概念进展问题求解、系统设计、以及人类行为了解等涵盖计算、系统设计、以及人类行为了解等涵盖计算机科学之广度的一系列思想活动机科学之广度的一系列思想活动讲讲 座座 提提 纲纲 根本知识根本知识 代数项、代数等式、演绎推理规那么、代数代数项、代数等式、演绎推理规那么、代数等式实际、等式定理证明方法等式实际、等式定理证明方法 项重写系统项重写系统 终止性、良基关系、合流性、部分合流性、终止性、良基关系、合流性、部分合流性、关键对关键对 良基归纳法良基

4、归纳法 Knuth-Bendix完备化过程完备化过程 基基 本本 知知 识识 代数项代数项 仅涉及一个类型的代数项仅涉及一个类型的代数项例：自然数类型的项例：自然数类型的项0, x, x + 1, x + Sy, f100, y 其中其中x和和y变量，变量，f 和和S是一阶函数，是一阶函数，S是后继函是后继函数数 涉及多个类型的代数项涉及多个类型的代数项假设有变量假设有变量 x : atom, l : listlist是是atom的的表类型表类型 并有函数并有函数 nil : list, cons : atom list list first : list atom，rest : list l

5、ist 那么那么 nil, consx, l, restconsx, nil, restconsx, l和和consfirstl, restl都是代数项都是代数项基基 本本 知知 识识 代数等式代数等式 例：例： x + 0 = x，x + Sy = Sx + y， x + y = z + 5 firstconsx, l = x x : atom, l : list restconsx, l = l x : atom, l : list 其中方括号中至少列出等式中出现的变量其中方括号中至少列出等式中出现的变量 等式证明等式证明 例：基于一组等式：例：基于一组等式：x + 0 = x和和x +

6、Sy = Sx + y 怎样证明等式怎样证明等式x + SSy = SSx + y ? 需求有推理规那么需求有推理规那么 等式证明的演绎推理规那么等式证明的演绎推理规那么 自反公理：自反公理：M M 对称规那么：对称规那么： 传送规那么：传送规那么： 加变量规那么：加变量规那么： 等价代换规那么：等价代换规那么：M = N N = M M = N N = P M = P M = N M = N , x : s M = N , x : s P = Q P/x M = Q/x N 基基 本本 知知 识识x不在不在 中中P , Q 是类型是类型s的项的项 等式推理的例子等式推理的例子 等价代换规那么

7、：等价代换规那么： 等式公理：等式公理：x + 0 = x和和x + Sy = Sx + y 证明等式：证明等式： x + SSy = SSx + y 证证: x + SSy 根据根据x + Sz = Sx + z，Sy = Sy =Sx + Sy运用等价代换规那么运用等价代换规那么得到第一个等式得到第一个等式 = SSx + y 根据根据Sz = Sz, x + Sy = Sx + y运用等价代换规那么得到运用等价代换规那么得到第二个等式第二个等式 再利用传送规那么可得要证的再利用传送规那么可得要证的等式等式M = N , x : s P = Q P/x M = Q/x N 基基 本本 知知

8、 识识基基 本本 知知 识识 代数等式实际代数等式实际algebraic equation theory在项集在项集T 上从一组等式上从一组等式E公理、公式公理、公式能推出的所能推出的所 有等式的集合称为一个等式实际通俗的解有等式的集合称为一个等式实际通俗的解释释 代数等式实际的定理证明代数等式实际的定理证明判别等式判别等式 M = N 能否在某个代数等式实能否在某个代数等式实际中际中 常用证明方法常用证明方法 把把M和和N分别化简分别化简, 假设它们的最简方式一样假设它们的最简方式一样那么相等那么相等 分别证明分别证明M和和N都等于都等于L 证明证明MN等于等于0还有其它方法还有其它方法基基

9、 本本 知知 识识 哪种证明方法最适宜于计算机自动证明？哪种证明方法最适宜于计算机自动证明？ 把把M和和N分别化简分别化简, 假设它们的最简方式一样假设它们的最简方式一样那么相等那么相等 假设基于所给的等式假设基于所给的等式E，能把，能把M和和N化简化简到最简方式，那么这种方式相对简单，便于到最简方式，那么这种方式相对简单，便于自动证明自动证明 分别证明分别证明M和和N都等于都等于L 自动选择自动选择L是非常困难的是非常困难的 证明证明MN等于等于0 不适用于非数值类型的项，例如先不适用于非数值类型的项，例如先前给出的前给出的atom类型的表类型的表项项 重重 写写 系系 统统 自动证明要处理

10、的问题自动证明要处理的问题 项集项集T 上等式集上等式集E中的等式要定向为单向项重中的等式要定向为单向项重写规那么写规那么, 构成重写规那么集构成重写规那么集R, 以方便计算机以方便计算机对项化简对项化简例如：例如：x + 0 = x，x + Sy = Sx + yx 0 = 0，x Sy = x y + x定向成如下的项重写系统定向成如下的项重写系统Rx + 0 x，x + Sy Sx + yx 0 0，x Sy x y + x 记号记号M N：用一条规那么可将项：用一条规那么可将项M归约成归约成N 例如，例如，x + SSy Sx + Sy SSx + y 两步重写都运用规那么两步重写都运

11、用规那么x + Sy Sx + y“既用既用于规那么，于规那么，也用于项的也用于项的归约归约项项 重重 写写 系系 统统 自动证明要处理的问题自动证明要处理的问题 项集项集T 上等式集上等式集E中的等式要定向为单向项重中的等式要定向为单向项重写规那么写规那么, 构成重写规那么集构成重写规那么集R, 以方便计算机以方便计算机对项化简对项化简例如：例如：x + 0 = x，x + Sy = Sx + yx 0 = 0，x Sy = x y + x定向成如下的项重写系统定向成如下的项重写系统Rx + 0 x，x + Sy Sx + yx 0 0，x Sy x y + x 记号记号M N：用一条规那么

12、可将项：用一条规那么可将项M归约成归约成N 经过定向等式来得到确定同样代数实际的重经过定向等式来得到确定同样代数实际的重写系统，需处理三个问题：终止性、合流性写系统，需处理三个问题：终止性、合流性和完备性和完备性“既用既用于规那么，于规那么，也用于项的也用于项的归约归约项项 重重 写写 系系 统统 终止性终止性 1. 终止性终止性项集项集T 上的上的R不存在无穷归约序列不存在无穷归约序列M0M1M2 , 即即: 任何项都能归约到范式不能再归任何项都能归约到范式不能再归约的项约的项 2. 有时很难对等式定向，以得到终止的重写系有时很难对等式定向，以得到终止的重写系统统 例如：对由三角函数公式构成

13、的等式系统例如：对由三角函数公式构成的等式系统 和角公式和角公式: sin + = sin cos + cos sin , 差角公式差角公式: sin = sin cos cos sin , 积化和差积化和差: sin cos = sin + +sin/2, 和差化积和差化积: sin +sin = 2sin + /2cos/2, 项项 重重 写写 系系 统统 终止性终止性 3. 定义：良基关系良基：定义：良基关系良基：well-founded集合集合A上的一个关系上的一个关系是良基的，假设不是良基的，假设不存在存在A上元上元 素的无穷递减序列素的无穷递减序列a0 a1 a2 a b iff

14、b a例：自然数上的例：自然数上的1, 有有 x 规那么规那么2： x, y 1, 有有2x+y+1 = 2x2y2 2x2y22x项项 重重 写写 系系 统统 合流性合流性 1. 记号记号 M N：M经假设干步含经假设干步含0步重写步重写后得到后得到N N M：假设有：假设有M N M N：假设存在：假设存在P，使得，使得M P且且N P 2. 定义定义 令令R是项集是项集T 上的重写系统上的重写系统,假设假设N M P 蕴涵蕴涵N P，那么，那么R是合流的是合流的 3. 定义定义 令令R是项集是项集T 上的重写系统上的重写系统,假设假设N M P 蕴涵蕴涵N P，那么，那么R是部分合流的是

15、部分合流的 部分合流关系严厉弱于合流关系部分合流关系严厉弱于合流关系 先思索部分合流的断定方法，然后再思索合先思索部分合流的断定方法，然后再思索合流流项项 重重 写写 系系 统统 部分合流性的断定部分合流性的断定 1. 讨论所选用的例子讨论所选用的例子函数：函数：nil : list cons : atom list list first : list atom，rest : list list cond : bool list list list等式：等式： firstconsx, l = x, restconsx, l = l, consfirstl, restl = l, 下面的讨论选择

16、如下两条定向后的重写下面的讨论选择如下两条定向后的重写规那么：规那么： restconsx, l lconsfirstl , restl l 项项 重重 写写 系系 统统 部分合流性的断定部分合流性的断定 1 无重叠的归约无重叠的归约 归约规那么：归约规那么： restconsx, l l 规那么规那么LR consfirstl , restl l 规那么规那么LR 待归约项：待归约项：cond B, restcons s l, consfirstl , restl 特点：特点：M中无重叠子项的归约相互不受影响中无重叠子项的归约相互不受影响项项 重重 写写 系系 统统 部分合流性的断定部分合流

17、性的断定 1 无重叠的归约无重叠的归约 图示：图示： LR 和和LR 是规那么是规那么 图中图中SL表示代换表示代换S作用作用 于于L的结果的结果 代换是变量到项的映射代换是变量到项的映射MSLS LMSLS RMSRS RS LMSR项项 重重 写写 系系 统统 部分合流性的断定部分合流性的断定 2 平凡的重叠平凡的重叠 归约规那么：归约规那么：restconsx, l l规规那么那么LR consfirstl , restl l 规那么规那么LR 待归约项：待归约项： restconsx, consfirstl , restl 特点：特点：SL 是是SL的子项，且的子项，且S把把L中的某变

18、量中的某变量这里是这里是l用用 由由SL 构成的项代换构成的项代换 不同的第不同的第1步归约不会影响部分合流，但步归约不会影响部分合流，但合流所合流所 需归约步数能够不一样取决于需归约步数能够不一样取决于R中有几个中有几个l项项 重重 写写 系系 统统 部分合流性的断定部分合流性的断定 2 平凡的重叠平凡的重叠 图示：图示： SL 是是SL的子项，且的子项，且S把把 L中的某变量中的某变量x用有用有SL 构成的项代换构成的项代换 不同的第不同的第1步归约不会影响部分合流，但合流步归约不会影响部分合流，但合流所需所需归约步数能够不一样归约步数能够不一样SLS LSLS RSRS LS LSRS

19、RS R项项 重重 写写 系系 统统 部分合流性的断定部分合流性的断定3 非平凡的重叠非平凡的重叠 归约规那么：归约规那么：restconsx, l l规规那么那么LR consfirstl ,restl l 规那么规那么LR 待归约项：待归约项：restconsfirstl , restl 特点：特点：SL 在在SL的非变量位置的非变量位置LR 或或LR 的运用都能够使对方的运用都能够使对方在原定位置在原定位置 不能运用，故不能保证部分合流不能运用，故不能保证部分合流项项 重重 写写 系系 统统 部分合流性的断定部分合流性的断定3 非平凡的重叠非平凡的重叠 图示：图示： SL 在在SL的非变

20、量位置的非变量位置 LR或或LR 的运用都能够使对方在原定位的运用都能够使对方在原定位置不置不 能运用，故不能保证部分合流能运用，故不能保证部分合流SLS LSLS RSR? 项项 重重 写写 系系 统统 部分合流性的断定部分合流性的断定 假设一切含非平凡重叠的项都能部分合流假设一切含非平凡重叠的项都能部分合流, 那那么么R也能也能 把对一切含非平凡重叠的项的检查减少为对把对一切含非平凡重叠的项的检查减少为对有限的重写规那么集的检查有限的重写规那么集的检查 假设由假设由R的重写规那么确定的一切关键的重写规那么确定的一切关键对对critical pair都能归约到同一个项，那都能归约到同一个项，

21、那么一切项的非平凡重叠都能部分合流可以么一切项的非平凡重叠都能部分合流可以证明，但在此不深究证明，但在此不深究 例：重写规那么例：重写规那么restconsx, l l，和，和 consfirstl , restl l 会构成两个关键对会构成两个关键对项项 重重 写写 系系 统统第第1个关键对：个关键对：选适当的代换，使得两规那么代换后绿色部分一样选适当的代换，使得两规那么代换后绿色部分一样consfirstl , restl l restconsx, l l第第1条规那么中的条规那么中的l 用用consx, l代换后代换后, 其左部是项其左部是项：consfirstconsx, l, res

22、tconsx, l用这两条规那么化简上述项可得第用这两条规那么化简上述项可得第1个关键对：个关键对： consx, l, consfirstconsx, l, l 归约关键对：归约关键对：consx, l曾经是范式曾经是范式 consfirstconsx, l, l consx, l第第1个关键对能归约到同一个项个关键对能归约到同一个项项项 重重 写写 系系 统统第第2个关键对：个关键对：选适当的代换，使得两规那么代换后绿色部分一样选适当的代换，使得两规那么代换后绿色部分一样 consfirstl , restl l restconsx, l l第第2条规那么中的条规那么中的x和和l分别代换成

23、分别代换成firstl 和和restl 后后,其左部是项：其左部是项：restconsfirstl , restl 用这两条规那么化简上述项可得第用这两条规那么化简上述项可得第2个关键对：个关键对： restl , restl 显然，第显然，第2个关键对也能归约到同一个项个关键对也能归约到同一个项项项 重重 写写 系系 统统 部分合流性的断定部分合流性的断定 定理定理 一个重写系统一个重写系统R是部分合流的，当且仅是部分合流的，当且仅当对每个关键对当对每个关键对 M, N 有有M N 假设一个有限的重写系统假设一个有限的重写系统R是终止的，那么该是终止的，那么该定理就给出一个算法，可用于断定定

24、理就给出一个算法，可用于断定R能否部分能否部分合流合流项项 重重 写写 系系 统统 部分合流、终止和合流之间的联络部分合流、终止和合流之间的联络 定理定理 令令R是终止的重写系统，那么是终止的重写系统，那么R是合流是合流的当且仅当它是部分合流的的当且仅当它是部分合流的 合流蕴含部分合流合流蕴含部分合流 反方向蕴含的证明需求运用良基归纳法反方向蕴含的证明需求运用良基归纳法良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合A上的一个良基关系，令上的一个良基关系，令P是是A上的某上的某 个性质。假设每当一切的个性质。假设每当一切的Pb b a为为真那么真那么Pa为真为真 即即 a.

25、 b.b a Pb Pa ， 那么，对一切的那么，对一切的a A，Pa为真为真证明步骤：证明步骤： 归纳根底归纳根底: 对恣意不存在对恣意不存在b使得使得b a的的a，证明，证明Pa 在不存在在不存在b使得使得b a的情况下，的情况下， b.b a Pb Pa等价于等价于 true Pa等价于等价于 Pa良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合A上的一个良基关系，令上的一个良基关系，令P是是A上的某上的某 个性质。假设每当一切的个性质。假设每当一切的Pb b a为为真那么真那么Pa为真为真 即即 a. b.b a Pb Pa ， 那么，对一切的那么，对一切的a A，

26、Pa为真为真证明步骤：证明步骤： 归纳根底归纳根底: 对恣意不存在对恣意不存在b使得使得b a的的a，证明，证明Pa 归纳步骤：对恣意存在归纳步骤：对恣意存在b使得使得b a的的a， b.b a Pb Pa的含义是的含义是 假定对一切假定对一切b a的的b，Pb为真，为真， 然后证明然后证明Pa为真为真良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合A上的一个良基关系，令上的一个良基关系，令P是是A上的某上的某 个性质。假设每当一切的个性质。假设每当一切的Pb b a为为真那么真那么Pa为真为真 即即 a. b.b a Pb Pa ， 那么，对一切的那么，对一切的a A，P

27、a为真为真如今要证明的是：假设有如今要证明的是：假设有M N 和和 M P，那么，那么N P假设假设MN, 那么规定那么规定N M。因是终止的系统，因此因是终止的系统，因此 是良基的。是良基的。归纳根底：假设不存在归纳根底：假设不存在N使得使得N M，即，即M是范式，是范式， 显然显然M具有要证明的性质具有要证明的性质MNP良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合A上的一个良基关系，令上的一个良基关系，令P是是A上的某上的某 个性质。假设每当一切的个性质。假设每当一切的Pb b a为为真那么真那么Pa为真为真 即即 a. b.b a Pb Pa ， 那么，对一切的那

28、么，对一切的a A，Pa为真为真如今要证明的是：假设有如今要证明的是：假设有M N 和和 M P，那么，那么N P归纳步骤：归纳步骤：1. 假设假设M N 或或 M P是是 0步归约，显然有步归约，显然有N PM (N)P良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合A上的一个良基关系，令上的一个良基关系，令P是是A上的某上的某 个性质。假设每当一切的个性质。假设每当一切的Pb b a为为真那么真那么Pa为真为真 即即 a. b.b a Pb Pa ， 那么，对一切的那么，对一切的a A，Pa为真为真2. 假定假定M N1 N并且并且 M P1 P1 根据部分合流性，根据

29、部分合流性， 存在存在Q，使得，使得N1 Q P1MN1P1NP良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合A上的一个良基关系，令上的一个良基关系，令P是是A上的某上的某 个性质。假设每当一切的个性质。假设每当一切的Pb b a为为真那么真那么Pa为真为真 即即 a. b.b a Pb Pa ， 那么，对一切的那么，对一切的a A，Pa为真为真2. 假定假定M N1 N并且并且 M P1 P1 根据部分合流性，根据部分合流性， 存在存在Q，使得，使得N1 Q P1MN1P1QNP良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合A上的一个良基关系，令上

30、的一个良基关系，令P是是A上的某上的某 个性质。假设每当一切的个性质。假设每当一切的Pb b a为为真那么真那么Pa为真为真 即即 a. b.b a Pb Pa ， 那么，对一切的那么，对一切的a A，Pa为真为真2. 假定假定M N1 N并且并且 M P1 P2 由归纳假设，由归纳假设， 存在存在R， 使得使得N R QMN1P1QNP良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合A上的一个良基关系，令上的一个良基关系，令P是是A上的某上的某 个性质。假设每当一切的个性质。假设每当一切的Pb b a为为真那么真那么Pa为真为真 即即 a. b.b a Pb Pa ， 那

31、么，对一切的那么，对一切的a A，Pa为真为真2. 假定假定M N1 N并且并且 M P1 P2 由归纳假设，由归纳假设， 存在存在R， 使得使得N R QMN1P1QNRP良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合A上的一个良基关系，令上的一个良基关系，令P是是A上的某上的某 个性质。假设每当一切的个性质。假设每当一切的Pb b a为为真那么真那么Pa为真为真 即即 a. b.b a Pb Pa ， 那么，对一切的那么，对一切的a A，Pa为真为真2. 假定假定M N1 N并且并且 M P1 P3 再由归纳假设，再由归纳假设， 存在存在S， 使得使得R S PMN1

32、P1QNRP良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合A上的一个良基关系，令上的一个良基关系，令P是是A上的某上的某 个性质。假设每当一切的个性质。假设每当一切的Pb b a为为真那么真那么Pa为真为真 即即 a. b.b a Pb Pa ， 那么，对一切的那么，对一切的a A，Pa为真为真2. 假定假定M N1 N并且并且 M P1 P3 再由归纳假设，再由归纳假设， 存在存在S， 使得使得R S P4 N P得证得证MN1P1QNRSPKnuth-Bendix完备化过程完备化过程 Knuth-Bendix完备化过程的目的完备化过程的目的回想回想最适宜于计算机自动证

33、明代数等式最适宜于计算机自动证明代数等式M=N的方的方式：式： 把把M和和N分别化简分别化简, 假设它们的最简方式一样假设它们的最简方式一样那么相等那么相等由定向代数等式系统由定向代数等式系统E来得到等价的重写系统来得到等价的重写系统R，需处理三个问题：终止性、合流性和完备，需处理三个问题：终止性、合流性和完备性性完备性在后面的例子中解释完备性在后面的例子中解释完备化过程的目的完备化过程的目的为一个代数等式系统为一个代数等式系统E，构造一个确定同样代，构造一个确定同样代数实际的终止且合流的重写系统数实际的终止且合流的重写系统RKnuth-Bendix完备化过程完备化过程 Knuth-Bendi

34、x完备化过程简介完备化过程简介 1. 把把E定向成一个终止的重写系统定向成一个终止的重写系统R假设定向失败，那么完备化过程失败假设定向失败，那么完备化过程失败 2. 检查检查R的部分合流性并进展完备化的部分合流性并进展完备化forR的每个关键对的每个关键对 M, N if 不具备不具备M N 把把MN或或NM参与参与R缘由稍后解缘由稍后解释释 假设定向失败，那么完备化过程失假设定向失败，那么完备化过程失败败 过程能够因过程能够因R不断地被参与规那么而不断地被参与规那么而不终止不终止 3. 最终的最终的R为所求为所求Knuth-Bendix完备化过程完备化过程 例例 作为输入的等式系统作为输入的

35、等式系统E E如下如下f fx x f fy y = f = fx + yx + yx + yx + y + z = x + + z = x + y + zy + z 1. 1. 先定向成一个终止的重写系统先定向成一个终止的重写系统R R f fx x f fy y f fx + yx + y x + yx + y + z + z x + x + y + zy + z 2. 2. 检查部分合流性并进展完备化检查部分合流性并进展完备化Knuth-Bendix完备化过程完备化过程 例例 作为输入的等式系统作为输入的等式系统E E如下如下f fx x f fy y = f = fx + yx + y

36、x + yx + y + z = x + + z = x + y + zy + z 1. 1. 先定向成一个终止的重写系统先定向成一个终止的重写系统R R f fx x f fy y f fx + yx + y x + yx + y + z + z x + x + y + zy + z 2. 2. 检查部分合流性并进展完备化检查部分合流性并进展完备化1 1 把两条规那么左部的绿色部分进展把两条规那么左部的绿色部分进展合一，产生一合一，产生一 个临界对个临界对 f fx + yx + y + z, f + z, fx x + + f fy y + z + z 临界对的两个项都已最简，这个临界对不

37、临界对的两个项都已最简，这个临界对不能合流能合流 第第2条规那么左部的合条规那么左部的合一结果：一结果： fx fy + z Knuth-Bendix完备化过程完备化过程 例例 作为输入的等式系统作为输入的等式系统E E如下如下f fx x f fy y = f = fx + yx + yx + yx + y + z = x + + z = x + y + zy + z 1. 1. 先定向成一个终止的重写系统先定向成一个终止的重写系统R R f fx x f fy y f fx + yx + y x + yx + y + z + z x + x + y + zy + z 2. 2. 检查部分合

38、流性并进展完备化检查部分合流性并进展完备化1 1 把两条规那么左部的绿色部分进展把两条规那么左部的绿色部分进展合一，产生一合一，产生一 个临界对个临界对 f fx + yx + y + z, f + z, fx x + + f fy y + z + z 2 2 添加重写规那么添加重写规那么f fx + yx + y + z + z f fx x + + f fy y + z + z 第第2条规那么左部的合条规那么左部的合一结果：一结果： fx fy + z Knuth-Bendix完备化过程完备化过程 例例 解释：添加规那么解释：添加规那么f fx + yx + y + z + z f fx

39、x + + f fy y + z + z的缘由的缘由 在在E E中可证中可证f fx + yx + y + z + z和和f fx x + + f fy y + z + z相等相等等式：等式：f fx x f fy y = f = fx + yx + y和和x + yx + y + z = x + + z = x + y + zy + z 证明：证明：f fx + yx + y + z = f + z = fx x f fy y + z = f + z = fx x + + f fy y + z + z 在未加上述重写规那么在未加上述重写规那么R R中证明不了中证明不了, , 即即R R不不完

40、备：完备： 在在R R中能证的等式在中能证的等式在E E中能证，但存在中能证，但存在E E中中能证而在能证而在R R中不能证的等式中不能证的等式 向向R R中加规那么是为了完备性中加规那么是为了完备性Knuth-Bendix完备化过程完备化过程 例续例续 1. 1. 先定向成一个终止的重写系统先定向成一个终止的重写系统R R f fx x f fy y f fx + yx + y x + yx + y + z + z x + x + y + zy + z 2. 2. 检查部分合流性并进展完备化检查部分合流性并进展完备化1 1 产生一个临界对产生一个临界对 f fx + yx + y + z,

41、+ z, f fx x + + f fy y + z + z 2 2 添加重写规那么添加重写规那么f fx + yx + y + z + z f fx x + + f fy y + z + z3 3 R R扩展为：扩展为： f fx x f fy y f f x + yx + y x + yx + y + z + z x x + + y + zy + z f fx + yx + y + z + z f fx x + + f fy y + z + zKnuth-Bendix完备化过程完备化过程 例续例续 1. 1. 先定向成一个终止的重写系统先定向成一个终止的重写系统R R f fx x f fy y f fx + yx + y x + yx + y + z + z x + x + y + zy + z 2. 2. 检查部分合流性并进展完备化检查部分合流性并进展完备化1 1 产生一个临界对产生一个临界对 f fx + yx + y + z, + z, f fx x + + f fy y + z + z 2 2 添加重写规那么添加重写规那么f fx + yx + y + z + z f fx x + + f fy y + z + z3 3 R