基本知识 ,代数等式理论（algebraic equation theory) 在项集T上从一组等式E(公理)能推出的 所有等式的集合称为一个等式理论（通俗的解释） 代数等式理论的定理证明 判断等式M=NT]是否在某个代数等式理论中 常用证明方法 把M和N分别化简，若它们的最简形式一样则相等 -分别证明M和N都等于L 证明M-N等于0 还有其他方法
基 本 知 识 • 代数等式理论（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
基 本 知 识 • 哪种证明方法最适合于计算机自动证明？ – 把M和N分别化简, 若它们的最简形式一样则相等 若基于等式E，通过等式证明，把M和N化简到 最简形式，则这种方式相对简单，便于自动证明 并且采用适合于计算机使用的单向重写规则 – 分别证明M和N都等于L 自动选择L是非常困难的 – 证明M−N等于0 不适用于非数值类型的项，例如先前给出的 atom类型的表 13
项重写系统 自动证明要解决的问题 项集T上等式集E中的等式要定向为单向项重写规 则，构成重写规则集R,以方便计算机对项化简 若E是：x+0=x,x+Sy=Sx+Jy) x×0=0,x×S0)=x×y+x 定向成如下的项重写系统R w→w既用于 x+0→x,x+Sy)→Sx+y) 规则，也用 x×0→0，x×Sy)→x×y+x于项的归约 记号M→N:用一条规则可将项M归约成N 若规则L→R∈R,含z一次出现的项T,以及使得 SLk T∈T的代换S,则[SLzT→SRIT
项 重 写 系 统 • 自动证明要解决的问题 – 项集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→RR，含z一次出现的项T，以及使得 [SL/z]TT的代换S，则[SL/z]T → [SR/z]T “→”既用于 规则，也用 于项的归约 14
项重写系统 ·自动证明要解决的问题 项集T上等式集E中的等式要定向为单向项重写规 则，构成重写规则集R,以方便计算机对项化简 若E是：x+0=x,x+Sy)=S(x+y) x×0=0,x×S)=x×y+x 定向成如下的项重写系统R w→〃既用于 x+0→x,x+Sy)→S+y) 规则，也用 x×0→0，x×Sy)→x×y+x于项的归约 记号M→N:用一条规则可将项M归约成N 例：x+S(Sy) 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)) “→”既用于 规则，也用 于项的归约 15
项重写系统 ·自动证明要解决的问题 项集T上等式集E中的等式要定向为单向项重写规 则，构成重写规则集R,以方便计算机对项化简 若E是：x+0=x,x+Sy=S(K+Jy) x×0=0,x×Sy)=x×Jy+x 定向成如下的项重写系统R x+0→x,x+Sy)→Sx+y) x×0→0，x×S)→x×y+x 记号M→N:用一条规则可将项M归约成N 例：x+SSy)→Sc+Sy) 代换S:x→x [S +Sy)/S(S+y)/ Jy-→S0y)
项 重 写 系 统 • 自动证明要解决的问题 – 项集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 16 代换S：x→x y→S(y)