代数等式理论的自动定理证明 计算机科学导论第一讲 计算机科学技术学院 陈意云 0551-63607043, yiyun@ustc.edu.cn http://staff.ustc.edu.cn/~yiyun/

课 程 内 容 课程内容 围绕学科理论体系中的模型理论, 程序理论和计算理论 1. 模型理论关心的问题 给定模型M，哪些问题可以由模型M解决；如何比较模型的表达能力 2. 程序理论关心的问题 给定模型M，如何用模型M解决问题 包括程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等 3. 计算理论关心的问题 给定模型M和一类问题, 解决该类问题需多少资源 本次讲座基于中学的等式推理,与这些内容关系不大 2

课 程 内 容 本讲座内容 以代数等式理论中的定理证明为例，介绍怎样从中学生熟知的等式演算方法，构造等式定理的自动证明系统，即将问题变为可用计算机求解 有助于理解计算思维的含义 计算思维（译文） 运用计算机科学的基础概念进行问题求解、系统设计、以及人类行为理解等涵盖计算机科学之广度的一系列思维活动 3

讲 座 提 纲 基本知识 项重写系统 良基归纳法 Knuth-Bendix完备化过程 代数项、代数等式、演绎推理规则、代数等式理论、等式定理证明方法 项重写系统 终止性、良基关系、合流性、局部合流性、关键对 良基归纳法 仅举例说明 Knuth-Bendix完备化过程 也仅举例说明 4

基 本 知 识 代数项和代数等式（仅涉及一个类型） 代数项 例：自然数类型nat 0, 1, 2, … : nat 常量 x, y : nat 变量 +, f : nat  nat  nat 二元函数 S : nat  nat 一元的后继函数 0, x, x + 1, x + S(y)和f(100, y) 都是代数项 代数等式 例： x + 0 = x，x + S(y) = S(x + y) x + y = z + 5 5

基 本 知 识 代数项和代数等式（涉及多个类型） 例：定义有限表：同类数据的有限序列的集合  6, 17, 50, 28, 188, 92, 30, 67, 15  18.8, 9.2, 50, 77, 8.6, 5.5, 40.0  a, b, c, d, e, f, …, z （非数值数据） 上述数据涉及两个类型  序列中元素的类型 — 数值或非数值类型  这些序列所属的类型，称为表（list）类型 —非数值类型 中学所学的代数概念在此已经扩展 6

基 本 知 识 代数项和代数等式（涉及多个类型） 代数项（表类型list ，表元类型atom）  x : atom, l : list 变量  nil : list 零元构造函数 (常量)  cons : atom  list  list 构造函数  first : list  atom，rest : list  list 观察函数  nil, cons(x, l), rest(cons(x, nil)), rest(cons(x, l)), cons(first(l), rest(l)) 都是代数项。用T 表示项集 代数等式(方括号列出等式中出现的变量及类型) first(cons(x, l)) = x [x : atom, l : list] rest(cons(x, l)) = l [x : atom, l : list] 7

基 本 知 识 等式证明 例：基于一组等式（公式、公理）： x + 0 = x 和 x + S(y) = S(x + y) 怎么证明等式： x + S(S(y)) = S(S(x + y)) ? 需要有推理规则 8

基 本 知 识 等式证明的演绎推理规则 自反公理：M  M  对称规则： M = N  传递规则： N = M  加变量规则： 等价代换规则： M = N  N = M  M = N  N = P  M = P  M = N  M = N , x : s x不在中 M = N , x : s P = Q  P/xM = Q/xN  P , Q 是类型s的项 9

基 本 知 识 等式推理的例子 等价代换规则： M = N , x : s P = Q  P/xM = Q/xN  等式公理：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(x + S(y)) 根据S(z) = S(z)，x + S(y) = S(x + y) = S(S(x + y)) 使用等价代换规则得到第二个等式 x + S(S(y)) = S(S(x + y)) 根据传递规则和上面两等式 M = N , x : s P = Q  P/xM = Q/xN  10

基 本 知 识 等式推理的例子 等价代换规则： M = N , x : s P = Q  P/xM = Q/xN  等式公理：x + 0 = x和x + S(y) = S(x + y) 证明等式： x + S(S(y)) = S(S(x + y)) 证明: x + S(S(y)) = S(x + S(y)) 我们的证明演算习惯见左边 = S(S(x + y)) 它是基于刚才所介绍的演绎推理的 若希望计算机来自动推理，严格的推理规则是必 须提供的 M = N , x : s P = Q  P/xM = Q/xN  11

基 本 知 识 代数等式理论（algebraic equation theory） 代数等式理论的定理证明 常用证明方法 在项集T 上从一组等式E（公理）能推出的 所有等式的集合称为一个等式理论（通俗的解释） 代数等式理论的定理证明 判断等式 M = N []是否在某个代数等式理论中 常用证明方法 把M和N分别化简, 若它们的最简形式一样则相等 分别证明M和N都等于L 证明MN等于0 还有其他方法 12

基 本 知 识 哪种证明方法最适合于计算机自动证明？ 把M和N分别化简, 若它们的最简形式一样则相等 若基于等式E，通过等式证明，把M和N化简到最简形式，则这种方式相对简单，便于自动证明 并且采用适合于计算机使用的单向重写规则 分别证明M和N都等于L 自动选择L是非常困难的 证明MN等于0 不适用于非数值类型的项，例如先前给出的atom类型的表 13

项 重 写 系 统 自动证明要解决的问题 项集T 上等式集E中的等式要定向为单向项重写规则, 构成重写规则集R, 以方便计算机对项化简 若E是：x + 0 = x，x + S(y) = S(x + y) x  0 = 0，x  S(y) = x  y + x 定向成如下的项重写系统R x + 0  x，x + S(y)  S(x + y) x  0  0，x  S(y)  x  y + x 记号M  N：用一条规则可将项M归约成N 若规则LRR，含z一次出现的项T，以及使得 [SL/z]TT的代换S，则[SL/z]T  [SR/z]T “”既用于规则，也用于项的归约 14

项 重 写 系 统 自动证明要解决的问题 项集T 上等式集E中的等式要定向为单向项重写规则, 构成重写规则集R, 以方便计算机对项化简 若E是：x + 0 = x，x + S(y) = S(x + y) x  0 = 0，x  S(y) = x  y + x 定向成如下的项重写系统R x + 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)) “”既用于规则，也用于项的归约 15

项 重 写 系 统 自动证明要解决的问题 项集T 上等式集E中的等式要定向为单向项重写规则, 构成重写规则集R, 以方便计算机对项化简 若E是：x + 0 = x，x + S(y) = S(x + y) x  0 = 0，x  S(y) = x  y + x 定向成如下的项重写系统R x + 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(x + S(y))/z]z  [S(S(x + y))/z]z 代换S：xx yS(y) 16

项 重 写 系 统 自动证明要解决的问题 项集T 上等式集E中的等式要定向为单向项重写规则, 构成重写规则集R, 以方便计算机对项化简 若E是：x + 0 = x，x + S(y) = S(x + y) x  0 = 0，x  S(y) = x  y + x 定向成如下的项重写系统R x + 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(x + y)) 子项能与第2条规则的左部匹配 17

项 重 写 系 统 自动证明要解决的问题 问题1：如何从E得到R，保证项的化简能终止 例：若有规则 x + y = y + x，不管怎么定向都有 a + b  b + a  a + b  … 问题2：如何从E得到R，保证对项采用不同化简 策略所得最简项是唯一的（合流性） E： = S(), Eq(x, x) = true, Eq(x, S(x)) = false R：  S(), Eq(x, x)  true, Eq(x, S(x))  false 18

项 重 写 系 统 自动证明要解决的问题 问题1：如何从E得到R，保证项的化简能终止 例：若有规则 x + y = y + x，不管怎么定向都有 a + b  b + a  a + b  … 问题2：如何从E得到R，保证对项采用不同化简 策略所得最简项是唯一的（合流性） R：  S(), Eq(x, x)  true, Eq(x, S(x))  false 则有： Eq(, )  true Eq(, )  Eq(, S())  false 问题3：如何从E得到R,使得E和R确定同样的代 数理论，即在E中能证则在R中也能证（完备性） 19

项 重 写 系 统 问题一：终止性 1. 终止性 项集T 上的R不存在无穷归约序列M0M1M2  …, 即: 任何项都能归约到范式(不能再归约的项) 2. 有时很难对等式定向，以得到终止的重写系统 例如：对由三角函数公式构成的等式系统 和角公式: sin(+) = sin cos + cos sin, … 差角公式: sin(  ) = sin cos  cos sin, … 积化和差: sin cos = (sin(+)+sin())/2, … 和差化积: sin+sin = 2sin((+)/2)cos(()/2), … … … 20

项 重 写 系 统 问题一：终止性 3. 定义：良基关系（良基：well-founded） 集合A上的二元关系是良基的，若不存在A上元 素的无穷递减序列a0  a1  a2 …（a  b iff b  a） 例：自然数上的‘<’关系是良基的，但‘’关系不是 4. 若项集T 和良基集A有映射f :T A, 满足 T 上任意归约序列 M0 M1 M2 …  Mn f f f f A上存在递减序列 a0  a1  a2  …  an 则T 上不存在无穷的归约序列 21

项 重 写 系 统 问题一：终止性 5. 定理 令R是项集T 上的一个重写系统，若能找到有良 基关系的集合A和映射f :T A，使得对R中每条 规则L R都有f (L)  f (R) ,那么R是终止的 注：由此定理，判断R的终止性成为可能 6. f 的选择 基于项的语法特点，或者给项指派一种语义 例1（基于语法特点：根据两边项语法上的繁简） first(cons(x, l))  x rest(cons(x, l))  l 22

项 重 写 系 统 问题一：终止性 例2（逻辑运算系统）  x  x ：就是C中的&&  (x  y)  (x  y) ：就是C中的 ||  (x  y)  (x  y) ：就是C中的！ x  (y  z)  (x  y)  (x  z) (y  z)  x  (y  x)  (z  x) 23

项 重 写 系 统 问题一：终止性 22 例2（逻辑运算系统，给项指派一种语义）  x  x A  N  0, 1  (x  y)  (x  y) A(x, y) = x + y + 1  (x  y)  (x  y) A(x, y) = x  y x  (y  z)  (x  y)  (x  z) A(x) = 2x (y  z)  x  (y  x)  (z  x) 语义指派f 应用到T 、、 和的结果分别是A、 A、A和A，后三者都是A上的二元或一元函数 对每条规则L  R，都有f (L)  f (R) 规则1：x >1, 有 > x 规则2：x, y >1, 有2(x+y+1) = 2x2y2 > 2x2y 22 x 24

项 重 写 系 统 问题二：合流性 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是局部合流的 局部合流关系严格弱于合流关系 先考虑局部合流的判定方法，然后再考虑合流的判定方法 25

项 重 写 系 统 插曲 在介绍局部合流性之前，先介绍代数项的树形表示 代数项cons(first(cons(x, l)), rest(cons(y, l)))的树形 表示 倒长的树：根在上，叶在下 每棵子树代表一个子项，整个树 代表完整的代数项 cons rest first y l x 26

项 重 写 系 统 局部合流性的判定（问题二的子问题） 1. 讨论所选用的例子 函数：nil : list cons : atom  list  list first : list  atom，rest : list  list cond : bool  list  list  list 等式： first(cons(x, l)) = x, rest(cons(x, l)) = l, cons(first(l), rest(l)) = l, … … 下面的讨论针对如下两条重写规则： rest(cons(x, l))  l cons(first(l), rest(l))  l 27

项 重 写 系 统 局部合流性的判定（问题二的子问题） (1) 无重叠的归约 归约规则： rest(cons(x, l))  l （规则LR） cons(first(l), rest(l))  l （规则LR） 待归约项： cond (B, rest(cons s l), cons(first(l), rest(l)) )  方式1: 原式  cond(B, l, cons(first(l), rest(l)) )  cond(B, l, l)  方式2: 原式  cond (B, rest(cons s l), l) 特点：M中无重叠子项的归约相互不受影响 28

项 重 写 系 统 局部合流性的判定 cond (B, rest(cons s l), (1) 无重叠的归约 图示： LR 和LR是规则 图中SL和SR分别表示 代换S作用于L的 结果 S : T T 代换S的最主要部分 是把变量映射到项 cond (B, rest(cons s l), cons(first(l), rest(l))) M SL SL SR SR 29

项 重 写 系 统 局部合流性的判定（问题二的子问题） (2) 平凡的重叠 归约规则： rest(cons(x, l))  l （规则LR） cons(first(l), rest(l))  l （规则LR） 待归约项： rest(cons(x, cons(first(l), rest(l)))  方式1: 原式  cons(first(l), rest(l))  l  方式2: 原式  rest(cons(x, l))  l 30

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

项 重 写 系 统 局部合流性的判定 rest(cons(x, (2) 平凡的重叠 cons(first(l), rest(l))) 图示： SL是SL的子项，且S把 L中的某变量x用有SL 构成的项代换 不同的第1步归约 不会影响局部合流， 但合流所需归约 步数可能不一样 rest(cons(x, cons(first(l), rest(l))) SL SL SR SR 32

项 重 写 系 统 局部合流性的判定（问题二的子问题） (3) 非平凡的重叠 归约规则： rest(cons(x, l))  l （规则LR） cons(first(l), rest(l)) l （规则LR） 待归约项： rest(cons(first(l), rest(l)))  方式1: 原式  rest(l) （用规则LR）  方式2: 原式  rest(l) （用规则LR） 该例比较特殊，都一步归约就到范式 33

项 重 写 系 统 局部合流性的判定（问题二的子问题） (3) 非平凡的重叠 归约规则： rest(cons(x, l))  l （规则LR） cons(first(l), rest(l)) l （规则LR） 待归约项： rest(cons(first(l), rest(l))) 特点： SL在SL的非变量位置 LR 或LR的使用都可能使对方在原定位置 不能使用，故不能保证局部合流 34

项 重 写 系 统 局部合流性的判定 (3) 非平凡的重叠 rest(cons(first(l), rest(l))) 图示： SL在SL的非变量位置 LR或LR的使用 都可能使对方在原定 位置不能使用，故不 能保证局部合流 rest(cons(first(l), rest(l))) SL SL SR SR ???  35

项 重 写 系 统 局部合流性的判定 若所有含非平凡重叠的项都能局部合流, 则R也能 把对所有含非平凡重叠的项的检查缩小为对有限的重写规则集的检查 若由R的重写规则确定的所有关键对(critical pair)都能归约到同一个项，则所有项的非平凡重叠都能局部合流（课堂上不介绍） 例：重写规则 rest(cons(x, l))  l，和 cons(first(l), rest(l))  l 会形成两个关键对 36

项 重 写 系 统 第1个关键对：（课堂上不介绍） 选适当的代换，使得两规则代换后绿色部分一样 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个关键对能归约到同一个项 37

项 重 写 系 统 第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个关键对也能归约到同一个项 38

项 重 写 系 统 局部合流性的判定 定理 一个重写系统R是局部合流的，当且仅当对每个关键对M, N有M    N 如果一个有限的重写系统R是终止的，那么该定理就给出一个算法，可用于判定R是否局部合流 39

项 重 写 系 统 局部合流、终止和合流之间的联系 定理 令R是终止的重写系统，那么R是合流的当且仅当它是局部合流的 合流蕴含局部合流（这是显然的） 反方向蕴含的证明需要使用良基归纳法 40

良 基 归 纳 法 良基归纳法 用一个简单例子说明它比自然数归纳法更一般 证明：对任何自然数的有限集合，每次删除一个元 素，最终会到达空集 证明：对任何自然数的有限集合，每次删除一个元 素，最终会到达空集 1. 若忽略集合中元素的个性，只关心集合中元素 的个数，则可以用自然数归纳法 2. 若关注元素个性（虽无必要）  ：集合之间的归约 规则: {x1, …, xn}{x2, …, xn} 其中x1是左边集合的任意元素 3.良基关系：A  B则A  B {0, 1, 2} {1, 2} {0, 2} {0, 1} {0} {1} {2}  41

良 基 归 纳 法 良基归纳法 需要证明：任何自然数的有限集合可归约到空集 1. 对所有的归约路径进行归纳 2. 良基归纳证明 归纳基础：经0步归约到 归纳假设：对所有的s  s1, s  s2, …, s  sn, s1, s2, …, sn都能归约 到 归纳证明：证明s能归约到 {0, 1, 2} {1, 2} {0, 2} {0, 1} {0} {1} {2}  42

良 基 归 纳 法 良基归纳法（课堂上不介绍） 令是集合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.(b  a  P(b))  P(a) 等价于 true  P(a) 等价于 P(a) 43

良 基 归 纳 法 良基归纳法（课堂上不介绍） 令是集合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.(b  a  P(b))  P(a)在此得出归纳假设： 假定对所有b  a的b，P(b)为真，然后证明： 归纳证明：证明P(a)为真 44

良 基 归 纳 法 用良基归纳法证明合流性 证明：若有M N和 M P，则N  P 若MN, 则规定NM。因系统终止, 故是良基的 归纳基础： 若不存在N使得N  M， 即M是范式，显然M具有 要证明的性质 因为M只能0步归约到 M本身，图上的N和P都只 能是M M N P (M) M 45

良 基 归 纳 法 用良基归纳法证明合流性 证明：若有M N和 M P，则N  P 若MN, 则规定NM。因系统终止, 故是良基的 归纳步骤： 假定M N1 N并且 M P1 P (1) 根据局部合流性， 存在Q，使得N1 Q P1 M N1 P1 N P 46

良 基 归 纳 法 用良基归纳法证明合流性 证明：若有M N和 M P，则N  P 若MN, 则规定NM。因系统终止, 故是良基的 归纳步骤： 假定M N1 N并且 M P1 P (1) 根据局部合流性， 存在Q，使得N1 Q P1 M N1 P1 Q N P 47

良 基 归 纳 法 用良基归纳法证明合流性 证明：若有M N和 M P，则N  P 若MN, 则规定NM。因系统终止, 故是良基的 归纳步骤： 假定M N1 N并且 M P1 P (2) 由归纳假设， 存在R， 使得N R Q M N1 P1 Q N P 48

良 基 归 纳 法 用良基归纳法证明合流性 证明：若有M N和 M P，则N  P 若MN, 则规定NM。因系统终止, 故是良基的 归纳步骤： 假定M N1 N并且 M P1 P (2) 由归纳假设， 存在R， 使得N R Q M N1 P1 Q N R P 49

良 基 归 纳 法 用良基归纳法证明合流性 证明：若有M N和 M P，则N  P 若MN, 则规定NM。因系统终止, 故是良基的 归纳步骤： 假定M N1 N并且 M P1 P (3) 再由归纳假设， 存在S， 使得R  S P M N1 P1 Q N R P 50

良 基 归 纳 法 用良基归纳法证明合流性 证明：若有M N和 M P，则N  P 若MN, 则规定NM。因系统终止, 故是良基的 归纳步骤： 假定M N1 N并且 M P1 P (3) 再由归纳假设， 存在S， 使得R  S P (4) N  P得证 M N1 P1 Q N R S P 51

Knuth-Bendix完备化过程 问题三：完备性 回顾 最适合于计算机自动证明代数等式M=N的方式： 由定向代数等式系统E来得到等价的重写系统R，需解决三个问题：终止性、合流性和完备性 完备性：从E可得到R，E和R确定同样的代数理论 概要介绍Knuth-Bendix完备化过程 给出一个完备化过程不终止的例子。由此可知，并非对任何E都可以得到与之有同样代数理论的R 52

Knuth-Bendix完备化过程 Knuth-Bendix完备化过程的目的 完备化过程的目的 为一个代数等式系统E，构造一个确定同样代数理论的终止且合流的重写系统R 53

Knuth-Bendix完备化过程 Knuth-Bendix完备化过程简介 1. 把E定向成一个终止的重写系统R （若定向失败，则完备化过程失败） 2. 检查R的局部合流性并进行完备化 for(R的每个关键对M, N) { if (不具备M  N){ 把MN或NM加入R（原因稍后解释） } } (过程可能因R不断地被加入规则而不终止) 3. 最终的R为所求 54

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) + z  x + (y + z) 2. 检查局部合流性并进行完备化 55

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) + z  x + (y + z) 2. 检查局部合流性并进行完备化 (1) 把两条规则左部的绿色部分进行合一，产生一 个临界对 f(x + y) + z, f(x) + (f(y) + z)  临界对的两个项都已最简，这个临界对不能合流 因第2条规则左部的合一结果： (f(x)  f(y)) + z 56

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) + 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 57

Knuth-Bendix完备化过程 例：完备化过程不终止 解释：增加规则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中不能证的等式 向R中加规则是为了完备性 58

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) f(x + y) + z  f(x) + (f(y) + z) 59

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) f(x + y) + z  f(x) + (f(y) + z) 两条规则中的绿色部分也可以合一 60

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) f(x + y) + z  f(x) + (f(y) + z) 将产生无数规则: f n(x + y) + z  f n(x) + (f n(y) + z) 完备化过程因不断产生新的规则而不终止 61

自 动 定 理 证 明 不同逻辑的自动定理证明方法可能不一样 本讲座介绍代数等式理论的自动定理证明，并未 彻底解决 其他还有： 命题逻辑的自动定理证明 几何定理的自动证明 … … 多种理论组合的自动定理证明 其中有些已彻底解决，有些在一定约束下可以解决 62

构造性证明与传统证明对比 传统证明的一个例子 证明 根据 是有理数或无理数来讨论 若 是有理数，则取x = 3 若 是无理数，则取x = 根据 是有理数或无理数来讨论 若 是有理数，则取x = 3 若 是无理数，则取x = 这种非构造性证明不太可能由计算机自动得到 63

小 结 本讲座小结 自动定理证明的应用 相关课程 以代数等式理论中的定理证明为例，介绍怎样从熟知的等式演算方法，构造自动定理证明系统 小 结 本讲座小结 以代数等式理论中的定理证明为例，介绍怎样从熟知的等式演算方法，构造自动定理证明系统 不同逻辑的自动定理证明方法不同 自动定理证明的应用 集成电路设计 程序验证 程序分析 相关课程 数理逻辑、人工智能 64

小 结 工具 交互式定理证明辅助工具Coq http://coq.inria.fr/，获ACM 2013年度软件系统奖 自动定理证明器Z3 小 结 工具 交互式定理证明辅助工具Coq http://coq.inria.fr/，获ACM 2013年度软件系统奖 自动定理证明器Z3 1. http://research.microsoft.com/en-us/um/ redmond/projects/z3/old/index.html 2. http://z3.codeplex.com/，获ACM 2015年度编程语言软件奖 65

小 结 参考文献 Daniel Kroening and Ofer Strichman，Decision 小 结 参考文献 Daniel Kroening and Ofer Strichman，Decision Procedures: An Algorithmic Point of View (Texts in Theoretical Computer Science. An EATCS Series) 陈意云、张昱，程序设计语言理论（第二版），高等教育出版者，2010年2月 备注：本次课的内容取自该书前两章中有关代数数据类型的部分 66