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

1、代数等式理论的自动定理证明代数等式理论的自动定理证明计算机科学导论第一讲计算机科学导论第一讲计算机科学技术学院计算机科学技术学院陈意云陈意云0551-课课 程程 内内 容容 课程内容课程内容围绕学科理论体系中的模型理论围绕学科理论体系中的模型理论, 程序理论和计算理论程序理论和计算理论1. 模型理论关心的问题模型理论关心的问题 给定模型给定模型m，哪些问题可以由模型，哪些问题可以由模型m解决；如何解决；如何比较模型的表达能力比较模型的表达能力2. 程序理论关心的问题程序理论关心的问题 给定模型给定模型m，如何用模型，如何用模型m解决问题解决问题 包括程序设计范型、程序设计语言、程序设计、包括程

2、序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等形式语义、类型论、程序验证、程序分析等3. 计算理论关心的问题计算理论关心的问题给定模型给定模型m和一类问题和一类问题, 解决该类问题需多少资源解决该类问题需多少资源本次讲座与这些本次讲座与这些内容关系不大内容关系不大课课 程程 内内 容容 本讲座内容本讲座内容 以以代数等式理论中的定理证明为例，介绍怎样从代数等式理论中的定理证明为例，介绍怎样从中学生熟知的等式演算中学生熟知的等式演算方法方法，构造自动构造自动定理证明定理证明系统，即将问题变为系统，即将问题变为可用计算机求解可用计算机求解 有助于理解什么是计算思维有助于

3、理解什么是计算思维计算思维（译文）计算思维（译文） 运用计算机科学的基础概念进行问题求解、系统运用计算机科学的基础概念进行问题求解、系统设计、以及人类行为理解等涵盖计算机科学之广度设计、以及人类行为理解等涵盖计算机科学之广度的一系列思维活动的一系列思维活动讲讲 座座 提提 纲纲 基本知识基本知识 代数项、代数等式、演绎推理规则、代数等式理代数项、代数等式、演绎推理规则、代数等式理论、等式定理证明方法论、等式定理证明方法 项重写系统项重写系统 终止性、良基关系、合流性、局部合流性、关键终止性、良基关系、合流性、局部合流性、关键对对 良基归纳法良基归纳法 knuth-bendix完备化过程完备化过

4、程 基基 本本 知知 识识 代数项代数项 仅涉及一个类型的代数项仅涉及一个类型的代数项例：自然数类型的项例：自然数类型的项0, x, x + 1, x + s(y), f(100, y)其中其中x和和y变量，变量，f 和和s是一阶函数，是一阶函数，s是后继函数是后继函数 涉及多个类型的代数项涉及多个类型的代数项若有变量若有变量 x : atom, l : list（list是是atom的表类型）的表类型）并有函数并有函数 nil : list, cons : atom list list first : list atom，rest : list list则则 nil, cons(x, l),

5、 rest(cons(x, nil), rest(cons(x, l)和和cons(first(l), rest(l)都是代数项都是代数项基基 本本 知知 识识 代数等式代数等式例：例： x + 0 = x，x + s(y) = s(x + y)， x + y = z + 5 first(cons(x, l) = x x : atom, l : list rest(cons(x, l) = l x : atom, l : list其中方括号中至少列出等式中出现的变量其中方括号中至少列出等式中出现的变量 等式证明等式证明例：基于一组等式：例：基于一组等式：x + 0 = x和和x + s(y)

6、= s(x + y) 怎么证明等式怎么证明等式x + s(s(y) = s(s(x + 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 + s(y) = s(x + y)证明等式：证明等式： x + s(s(y) = s(s(x + y)证证: x + s(s(y) 根据根据x + s(z) = s(x + z)，s(y) = s(y)= s(x + s(y)使用等价代换规则得到第一个等式使用等价代换规则得到第一个等式= s(s(x + y) 根据根据s(z) = s(z), x + s(y) = s(x + y)使用等价代换规则得到第二个等式使用等价代换规则得到第二个等式 再利用传递规则可得要证的等式再利用传递规则可得要证的等式m = n , x : s p = q p/x m = q/x

8、n 基基 本本 知知 识识基基 本本 知知 识识 代数等式理论（代数等式理论（algebraic equation theory）在在项集项集t 上上从一组等式从一组等式e(公理、公式公理、公式)能推出的所能推出的所有等式的集合称为一个等式理论（通俗的解释）有等式的集合称为一个等式理论（通俗的解释） 代数等式理论的定理证明代数等式理论的定理证明判断等式判断等式 m = n 是否在某个代数等式理论中是否在某个代数等式理论中 常用证明方法常用证明方法 把把m和和n分别化简分别化简, 若它们的最简形式一样则相等若它们的最简形式一样则相等 分别证明分别证明m和和n都等于都等于l 证明证明m n等于等于

9、0还有其它方法还有其它方法基基 本本 知知 识识 哪种证明方法最适合于计算机自动证明？哪种证明方法最适合于计算机自动证明？ 把把m和和n分别化简分别化简, 若它们的最简形式一样则相等若它们的最简形式一样则相等 若基于所给的等式若基于所给的等式e，能把，能把m和和n化简到最简形化简到最简形式，则这种方式相对简单，便于自动证明式，则这种方式相对简单，便于自动证明 分别证明分别证明m和和n都等于都等于l 自动选择自动选择l是非常困难的是非常困难的 证明证明m n等于等于0 不适用于非数值类型的项，例如先前给出的不适用于非数值类型的项，例如先前给出的atom类型的表类型的表项项 重重 写写 系系 统统

10、 自动证明要解决的问题自动证明要解决的问题 项集项集t 上上等式集等式集e中的等式要定向为单向项重写中的等式要定向为单向项重写规则规则, 构成重写规则集构成重写规则集r, 以方便计算机对项化简以方便计算机对项化简例如：例如：x + 0 = x，x + s(y) = s(x + y)x 0 = 0，x s(y) = x y + x定向成如下的项重写系统定向成如下的项重写系统rx + 0 x，x + s(y) s(x + y)x 0 0，x s(y) x y + x 记号记号m n：用一条规则可将项：用一条规则可将项m归约成归约成n 例如，例如，x + s(s(y) s(x + s(y) s(s(

11、x + y) 两步重写都使用规则两步重写都使用规则x + s(y) s(x + y)“”既用于既用于规则，也用规则，也用于项的归约于项的归约项项 重重 写写 系系 统统 自动证明要解决的问题自动证明要解决的问题 项集项集t 上上等式集等式集e中的等式要定向为单向项重写中的等式要定向为单向项重写规则规则, 构成重写规则集构成重写规则集r, 以方便计算机对项化简以方便计算机对项化简例如：例如：x + 0 = x，x + s(y) = s(x + y)x 0 = 0，x s(y) = x y + x定向成如下的项重写系统定向成如下的项重写系统rx + 0 x，x + s(y) s(x + y)x 0

12、 0，x s(y) x y + x 记号记号m n：用一条规则可将项：用一条规则可将项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( + )/2)cos()/2), 项项 重重 写写 系系 统统 终止性终止性3. 定义：良基关系（良基：定义：良基关系（良基：well-founded）集合集合a上的一个关系上的一个关系 是是良基的良基的，若不

14、存在，若不存在a上元上元素的无穷递减序列素的无穷递减序列a0 a1 a2 （a b iff b a）例：自然数上的例：自然数上的1, 有有 x 规则规则2： x, y 1, 有有2(x+y+1) = 2x2y2 2x2y22x项项 重重 写写 系系 统统 合流性合流性1. 记号记号 mn：m经若干步经若干步(含含0步步)重写后得到重写后得到n nm：若有：若有mn m n：若存在：若存在p，使得，使得mp且且np2. 定义定义 令令r是项集是项集t 上的上的重写系统重写系统, ,若若n m p 蕴涵蕴涵n p，则，则r是是合流的合流的3. 定义定义 令令r是项集是项集t 上的上的重写系统重写系

15、统, ,若若n m p 蕴涵蕴涵n p，则，则r是局部是局部合流的合流的 局部合流关系严格弱于合流关系局部合流关系严格弱于合流关系 先考虑局部合流的判定方法，然后再考虑合流先考虑局部合流的判定方法，然后再考虑合流项项 重重 写写 系系 统统 局部合流性的判定局部合流性的判定1. 讨论所选用的例子讨论所选用的例子函数：函数：nil : listcons : atom list list first : list atom，rest : list list cond : bool list list list等式：等式： first(cons(x, l) = x, rest(cons(x, l)

16、= l, cons(first(l), rest(l) = l, 下面的讨论选择如下两条定向后的重写规则：下面的讨论选择如下两条定向后的重写规则： rest(cons(x, l) lcons(first(l ), rest(l ) l 项项 重重 写写 系系 统统 局部合流性的判定局部合流性的判定 (1) 无重叠的归约无重叠的归约 归约规则：归约规则： rest(cons(x, l) l （规则（规则lr） cons(first(l ), rest(l ) l （规则（规则lr ） 待归约项：待归约项：cond (b, rest(cons s l), cons(first(l ), rest(

17、l ) ) 特点：特点：m中无重叠子项的归约相互不受影响中无重叠子项的归约相互不受影响项项 重重 写写 系系 统统 局部合流性的判定局部合流性的判定 (1) 无重叠的归约无重叠的归约图示：图示： lr 和和lr 是规则是规则 图中图中sl表示代换表示代换s作用作用 于于l的结果的结果 代换是变量到项的映射代换是变量到项的映射mslsl mslsr msrsr sl msr项项 重重 写写 系系 统统 局部合流性的判定局部合流性的判定 (2) 平凡的重叠平凡的重叠 归约规则：归约规则：rest(cons(x, l) l（规则（规则lr） cons(first(l ), rest(l ) l （规

18、则（规则lr ） 待归约项：待归约项： rest(cons(x, cons(first(l ), rest(l ) 特点：特点：sl 是是sl的子项的子项，且，且s把把l中的某变量中的某变量(这里是这里是l)用用由由sl 构成的项代换构成的项代换 不同的第不同的第1步归约不会影响局部合流，但合流所步归约不会影响局部合流，但合流所需归约步数可能不一样（取决于需归约步数可能不一样（取决于r中有几个中有几个l）项项 重重 写写 系系 统统 局部合流性的判定局部合流性的判定 (2) 平凡的重叠平凡的重叠图示：图示： sl 是是sl的子项的子项，且，且s把把 l中的某变量中的某变量x用有用有sl 构成的

19、项代换构成的项代换 不同的第不同的第1步归约不会影响局部合流，但合流所需步归约不会影响局部合流，但合流所需归约步数可能不一样归约步数可能不一样slsl slsr srsl sl srsr sr 项项 重重 写写 系系 统统 局部合流性的判定局部合流性的判定(3) 非平凡的重叠非平凡的重叠 归约规则：归约规则：rest(cons(x, l) l（规则（规则lr） cons(first(l ),rest(l ) l （规则（规则lr ） 待归约项：待归约项：rest(cons(first(l ), rest(l ) 特点：特点：sl 在在sl的非变量位置的非变量位置lr 或或lr 的使用都可能使的

20、使用都可能使对方在原定位置对方在原定位置 不能使用，故不能保证局部合流不能使用，故不能保证局部合流项项 重重 写写 系系 统统 局部合流性的判定局部合流性的判定(3) 非平凡的重叠非平凡的重叠图示：图示： sl 在在sl的非变量位置的非变量位置 lr或或lr 的使用都可能使的使用都可能使对方在原定位置不对方在原定位置不能使用，故不能保证局部合流能使用，故不能保证局部合流slsl slsr sr? 项项 重重 写写 系系 统统 局部合流性的判定局部合流性的判定 若所有含非平凡重叠的项都能局部合流若所有含非平凡重叠的项都能局部合流, 则则r也能也能 把对所有含非平凡重叠的项的检查缩小为对有限把对所

21、有含非平凡重叠的项的检查缩小为对有限的重写规则集的检查的重写规则集的检查 若由若由r的重写规则确定的所有关键对的重写规则确定的所有关键对(critical pair)都能归约到同一个项，则都能归约到同一个项，则所有项的非平凡重所有项的非平凡重叠都能局部合流（可以证明，但在此不深究）叠都能局部合流（可以证明，但在此不深究） 例：重写规则例：重写规则rest(cons(x, l) l，和，和 cons(first(l ), rest(l ) l 会形成两个关键对会形成两个关键对项项 重重 写写 系系 统统第第1个关键对：个关键对： 选适当的代换，使得两规则代换后绿色选适当的代换，使得两规则代换后绿

22、色部分一样部分一样cons(first(l ), rest(l ) l rest(cons(x, l) l 第第1条规则中的条规则中的l 用用cons(x, l)代换后代换后, 其左部是项：其左部是项：cons(first(cons(x, l), (rest(cons(x, l) 用这两条规则化简上述项可得第用这两条规则化简上述项可得第1个关键对：个关键对： cons(x, l), cons(first(cons(x, l), l) 归约关键对：归约关键对：cons(x, l)已经是范式已经是范式 cons(first(cons(x, l), l) cons(x, l) 第第1个关键对能归约到

23、同一个项个关键对能归约到同一个项项项 重重 写写 系系 统统第第2个关键对：个关键对： 选适当的代换，使得两规则代换后绿色选适当的代换，使得两规则代换后绿色部分一样部分一样 cons(first(l ), rest(l ) l rest(cons(x, l) l 第第2条规则中的条规则中的x和和l分别代换成分别代换成first(l )和和rest(l )后后,其左部是项：其左部是项：rest(cons(first(l ), rest(l ) 用这两条规则化简上述项可得第用这两条规则化简上述项可得第2个关键对：个关键对： rest(l ), rest(l ) 显然，第显然，第2个关键对也能归约到

24、同一个项个关键对也能归约到同一个项项项 重重 写写 系系 统统 局部合流性的判定局部合流性的判定 定理定理 一个重写系统一个重写系统r是局部合流的，当且仅当对是局部合流的，当且仅当对每个关键对每个关键对 m, n 有有m n 如果如果一个有限的重写系统一个有限的重写系统r是终止的，那么该定是终止的，那么该定理就给出一个算法，可用于判定理就给出一个算法，可用于判定r是否局部合流是否局部合流项项 重重 写写 系系 统统 局部合流、终止和合流之间的联系局部合流、终止和合流之间的联系定理定理 令令r是终止的重写系统，那么是终止的重写系统，那么r是合流的当是合流的当且仅当它是局部合流的且仅当它是局部合流

25、的 合流蕴含局部合流合流蕴含局部合流 反方向蕴含的证明需要使用良基归纳法反方向蕴含的证明需要使用良基归纳法良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合a上的一个良基关系，令上的一个良基关系，令p是是a上的某上的某个性质。若每当所有的个性质。若每当所有的p(b) (b a)为真则为真则p(a)为真为真(即即 a.( b.( (b a p(b) p(a) )，那么，对所有的那么，对所有的a a，p(a)为真为真证明步骤：证明步骤： 归纳基础归纳基础: 对任意不存在对任意不存在b使得使得b a的的a，证明，证明p(a) 在不存在在不存在b使得使得b a的情况下，的情况下， b

26、.( (b a p(b) p(a)等价于等价于 true p(a)等价于等价于 p(a)良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合a上的一个良基关系，令上的一个良基关系，令p是是a上的某上的某个性质。若每当所有的个性质。若每当所有的p(b) (b a)为真则为真则p(a)为真为真(即即 a.( b.( (b a p(b) p(a) )，那么，对所有的那么，对所有的a a，p(a)为真为真证明步骤：证明步骤： 归纳基础归纳基础: 对任意不存在对任意不存在b使得使得b a的的a，证明，证明p(a) 归纳步骤：对任意存在归纳步骤：对任意存在b使得使得b a的的a， b.(

27、(b a p(b) p(a)的含义是的含义是 假定对所有假定对所有b a的的b，p(b)为真，为真， 然后证明然后证明p(a)为真为真良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合a上的一个良基关系，令上的一个良基关系，令p是是a上的某上的某个性质。若每当所有的个性质。若每当所有的p(b) (b a)为真则为真则p(a)为真为真(即即 a.( b.( (b a p(b) p(a) )，那么，对所有的那么，对所有的a a，p(a)为真为真现在要证明的是：若有现在要证明的是：若有m n和和 m p，则，则n p若若mn, 则规定则规定n m。因是终止的系统，因此因是终止的系统

28、，因此 是良基的。是良基的。归纳基础：若不存在归纳基础：若不存在n使得使得n m，即，即m是范式，是范式，显然显然m具有要证明的性质具有要证明的性质mnp良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合a上的一个良基关系，令上的一个良基关系，令p是是a上的某上的某个性质。若每当所有的个性质。若每当所有的p(b) (b a)为真则为真则p(a)为真为真(即即 a.( b.( (b a p(b) p(a) )，那么，对所有的那么，对所有的a a，p(a)为真为真现在要证明的是：若有现在要证明的是：若有m n和和 m p，则，则n p归纳步骤：归纳步骤：1. 若若m n 或或 m

29、 p是是0步归约，显然有步归约，显然有n pm (n)p良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合a上的一个良基关系，令上的一个良基关系，令p是是a上的某上的某个性质。若每当所有的个性质。若每当所有的p(b) (b a)为真则为真则p(a)为真为真(即即 a.( b.( (b a p(b) p(a) )，那么，对所有的那么，对所有的a a，p(a)为真为真2. 假定假定m n1 n并且并且m p1 p(1) 根据局部合流性，根据局部合流性，存在存在q，使得，使得n1 q p1mn1p1np良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合a上的一个良

30、基关系，令上的一个良基关系，令p是是a上的某上的某个性质。若每当所有的个性质。若每当所有的p(b) (b a)为真则为真则p(a)为真为真(即即 a.( b.( (b a p(b) p(a) )，那么，对所有的那么，对所有的a a，p(a)为真为真2. 假定假定m n1 n并且并且m p1 p(1) 根据局部合流性，根据局部合流性，存在存在q，使得，使得n1 q p1mn1p1qnp良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合a上的一个良基关系，令上的一个良基关系，令p是是a上的某上的某个性质。若每当所有的个性质。若每当所有的p(b) (b a)为真则为真则p(a)为真

31、为真(即即 a.( b.( (b a p(b) p(a) )，那么，对所有的那么，对所有的a a，p(a)为真为真2. 假定假定m n1 n并且并且m p1 p(2) 由归纳假设，由归纳假设，存在存在r， 使得使得n r qmn1p1qnp良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合a上的一个良基关系，令上的一个良基关系，令p是是a上的某上的某个性质。若每当所有的个性质。若每当所有的p(b) (b a)为真则为真则p(a)为真为真(即即 a.( b.( (b a p(b) p(a) )，那么，对所有的那么，对所有的a a，p(a)为真为真2. 假定假定m n1 n并且并

32、且m p1 p(2) 由归纳假设，由归纳假设，存在存在r， 使得使得n r qmn1p1qnrp良良 基基 归归 纳纳 法法 良基归纳法良基归纳法令令 是集合是集合a上的一个良基关系，令上的一个良基关系，令p是是a上的某上的某个性质。若每当所有的个性质。若每当所有的p(b) (b a)为真则为真则p(a)为真为真(即即 a.( b.( (b a p(b) p(a) )，那么，对所有的那么，对所有的a a，p(a)为真为真2. 假定假定m n1 n并且并且m p1 p(3) 再由归纳假设，再由归纳假设，存在存在s， 使得使得r s pmn1p1qnrp良良 基基 归归 纳纳 法法 良基归纳法良基

33、归纳法令令 是集合是集合a上的一个良基关系，令上的一个良基关系，令p是是a上的某上的某个性质。若每当所有的个性质。若每当所有的p(b) (b a)为真则为真则p(a)为真为真(即即 a.( b.( (b a p(b) p(a) )，那么，对所有的那么，对所有的a a，p(a)为真为真2. 假定假定m n1 n并且并且m p1 p(3) 再由归纳假设，再由归纳假设，存在存在s， 使得使得r s p(4) n p得证得证mn1p1qnrspknuth-bendix完备化过程完备化过程 knuth-bendix完备化过程的目的完备化过程的目的回顾回顾 最适合于计算机自动证明最适合于计算机自动证明代数

34、代数等式等式m=n的方式：的方式： 把把m和和n分别化简分别化简, 若它们的最简形式一样则相等若它们的最简形式一样则相等 由由定向代数等式系统定向代数等式系统e来得到等价的重写系统来得到等价的重写系统r，需解决三个问题：终止性、合流性和完备性需解决三个问题：终止性、合流性和完备性（完备性在后面的例子中解释）（完备性在后面的例子中解释）完备化过程的目的完备化过程的目的 为一个代数等式系统为一个代数等式系统e，构造一个确定同样代数，构造一个确定同样代数理论的终止且合流的重写系统理论的终止且合流的重写系统rknuth-bendix完备化过程完备化过程 knuth-bendix完备化过程简介完备化过程

35、简介1. 把把e定向成一个终止的重写系统定向成一个终止的重写系统r（若定向失败，则完备化过程失败）（若定向失败，则完备化过程失败）2. 检查检查r的局部合流性并进行完备化的局部合流性并进行完备化for(r的每个关键对的每个关键对 m, n ) if (不具备不具备m n) 把把mn或或nm加入加入r（原因稍后解释）（原因稍后解释） （若定向失败，则完备化过程失败）（若定向失败，则完备化过程失败） (过程可能因过程可能因r不断地被加入规则而不终止不断地被加入规则而不终止)3. 最终的最终的r为所求为所求knuth-bendix完备化过程完备化过程 例例作为输入的等式系统作为输入的等式系统e如下如

36、下f(x) f(y) = f(x + y)(x + y) + z = x + (y + z)1. 先定向成一个终止的重写系统先定向成一个终止的重写系统r f(x) f(y) f(x + y) (x + y) + z x + (y + z)2. 检查局部合流性并进行完备化检查局部合流性并进行完备化knuth-bendix完备化过程完备化过程 例例作为输入的等式系统作为输入的等式系统e如下如下f(x) f(y) = f(x + y)(x + y) + z = x + (y + z)1. 先定向成一个终止的重写系统先定向成一个终止的重写系统r f(x) f(y) f(x + y) (x + y) +

37、 z x + (y + z)2. 检查局部合流性并进行完备化检查局部合流性并进行完备化(1) 把两条规则左部的绿色部分进行合一，把两条规则左部的绿色部分进行合一，产生产生一一个个临界临界对对 f(x + y) + z, f(x) + (f(y) + z) 临界对的两个项都已最简，这个临界对不能合流临界对的两个项都已最简，这个临界对不能合流 第第2条规则左部的合一条规则左部的合一结果：结果： (f(x) f(y) + z knuth-bendix完备化过程完备化过程 例例作为输入的等式系统作为输入的等式系统e如下如下f(x) f(y) = f(x + y)(x + y) + z = x + (y

38、 + z)1. 先定向成一个终止的重写系统先定向成一个终止的重写系统r f(x) f(y) f(x + y) (x + y) + z x + (y + z)2. 检查局部合流性并进行完备化检查局部合流性并进行完备化(1) 把两条规则左部的绿色部分进行合一，把两条规则左部的绿色部分进行合一，产生产生一一个个临界临界对对 f(x + y) + z, f(x) + (f(y) + z) (2) 增加增加重写规则重写规则f(x + y) + z f(x) + (f(y) + z) 第第2条规则左部的合一条规则左部的合一结果：结果： (f(x) f(y) + z knuth-bendix完备化过程完备化

39、过程 例例解释：增加规则解释：增加规则f(x + y) + z f(x) + (f(y) + z)的原因的原因 在在e中可证中可证f(x + y) + z和和f(x) + (f(y) + z)相等相等等式等式：f(x) f(y) = f(x + y)和和(x + y) + z = x + (y + z) 证明：证明：f(x + y) + z = f(x) f(y) + z = f(x) + (f(y) + z) 在未加上述重写规则在未加上述重写规则r中证明不了中证明不了, 即即r不不完备完备： 在在r中能证的等式在中能证的等式在e中中能证，但存在能证，但存在e中中能证而能证而在在r中不能证的等

40、式中不能证的等式 向向r中加规则是为了完备性中加规则是为了完备性knuth-bendix完备化过程完备化过程 例（续）例（续）1. 先定向成一个终止的重写系统先定向成一个终止的重写系统r f(x) f(y) f(x + y) (x + y) + z x + (y + z)2. 检查局部合流性并进行完备化检查局部合流性并进行完备化(1) 产生一个临界对产生一个临界对 f(x + y) + z, f(x) + (f(y) + z) (2) 增加重写规则增加重写规则f(x + y) + z f(x) + (f(y) + z)(3) r扩大为：扩大为： f(x) f(y) f (x + y) (x + y) + z x + (y + z) f(x + y) + z f(x) + (f(y) + z)knuth-bendix完备化过程完备化过程 例（续）例（续）1. 先定向成一个终止的重写系统先定向成一个终止的重写系统r f(x) f(y