基本知识 ·代数项和代数等式（涉及多个类型） 代数项（表类型ist,表元类型atom) x:atom, l:list 变量 nil list 零元构造函数（常量 cons:atom×list→list 构造函数 first:list→atom,rest:list→list 观察函数 nil,cons(x,1),rest(cons(x,nil)),rest(cons(x,1)), cons(first((,rest()都是代数项。用T表示项集 代数等式（方括号列出等式中出现的变量及类型 first(cons(x,1)=x [x atom,I list] rest(cons(x,1)=l x atom,1 list]
基 本 知 识 • 代数项和代数等式（涉及多个类型） – 代数项（表类型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+Sy)=Sc+y) 怎么证明等式： x+SS))=S(S+))? 需要有推理规则 8
基 本 知 识 • 等式证明 例：基于一组等式（公式、公理）： x + 0 = x 和 x + S(y) = S(x + y) 怎么证明等式： x + S(S(y)) = S(S(x + y)) ? 需要有推理规则 8
基本知识 等式证明的演绎推理规则 M=N[T] 自反公理：M=M[T] 对称规则： N=M[T] M=NT]N=PT] 传递规则： M=P[] 加变量规则： M=NT] x不在T中 M=NI,x:s] M=NT,x:s]P=0[T] 等价代换规则： [PIx]M [Q/]N [T] P,2是类型s的项
• 等式证明的演绎推理规则 自反公理：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/xM = Q/xN 基 本 知 识 x不在中 P , Q 是类型s的项 9
基本知识 等式推理的例子 等价代换规则： M=NT,x:s]P=0[T] [PIx]M [Q/x]N [T] 等式公理：x+0=x和x+Sy)=S(x+y) 证明等式：x+SSy)=SSc+) 证明：x+SSy)根据x+Sz=Sx+z),Sy=Sy =S(x+S(y)) 使用等价代换规则得到第一个等式 S(x+S(y)) 根据Sz=Sz),x+Sy)=Sx+y S(S(x+y)) 使用等价代换规则得到第二个等式 x+S(Sy)=S(Sc+y)根据传递规则和上面两等式
• 等式推理的例子 等价代换规则： 等式公理：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/xM = Q/xN 基 本 知 识 10
基本知识 等式推理的例子 等价代换规则： M=NT,x:s]P=0[T] [PIx]M [Q/x]N [T] 等式公理：x+0=x和x+Sy)=S(x+y) 证明等式：x+SSy)=S(S(c+) 证明：x+SSy) =S(x+S(y)) 我们的证明演算习惯见左边 S(S(x+y)) 它是基于刚才所介绍的演绎推理的 若希望计算机来自动推理，严格的推理规则是必 须提供的
• 等式推理的例子 等价代换规则： 等式公理：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/xM = Q/xN 基 本 知 识 11