1、代数等式理论的自动定理证明计算机科学导论第一讲计算机科学技术学院陈意云0551-课 程 内 容 课程内容围绕学科理论体系中的模型理论 , 程序理论和计算理论1. 模型理论关心的问题给定模型 M，哪些问题可以由模型 M解决；如何比较模型的表达能力2. 程序理论关心的问题 给定模型 M，如何用模型 M解决问题 包括程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等3. 计算理论关心的问题给定模型 M和一类问题 , 解决该类问题需多少资源本次讲座与这些内容关系不大课 程 内 容 本讲座内容 以 代数等式理论中的定理证明为例，介绍怎样从中学生熟知的等式演算 方法 ， 构造自动
2、 定理证明系统，即将问题变为 可用计算机求解 有助于理解什么是计算思维计算思维（译文）运用计算机科学的基础概念进行问题求解、系统设计、以及人类行为理解等涵盖计算机科学之广度的一系列思维活动讲 座 提 纲 基本知识 代数项、代数等式、演绎推理规则、代数等式理论、等式定理证明方法 项重写系统 终止性、良基关系、合流性、局部合流性、关键对 良基归纳法 Knuth-Bendix完备化过程 基 本 知 识 代数 项 仅涉及一个类型的代数项例：自然数类型的项 0, x, x + 1, x + S(y), f(100, y)其中 x和 y变量， f 和 S是一阶函数， S是后继函数 涉及多个类型的代数项若有
3、变量 x : atom, l : list（ list是 atom的表类型）并有函数 nil : list, cons : atom list listfirst : list atom， rest : list list则 nil, cons(x, l), 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 + 5first(cons(x, l) = x x : atom, l : listrest(cons
4、(x, l) = l x : atom, l : list其中方括号中至少列出等式中出现的变量 等式证明例：基于一组等式： x + 0 = x和 x + S(y) = 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 : sM = N , x : s P = Q P/xM = Q/xN 基 本 知 识x不在 中P , Q 是类型 s的项 等式推理的例子等价代换规则：等式公
5、理： 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/xM = Q/xN 基 本 知 识基 本 知 识 代数等式理论（ algebraic equation theory）在
6、项集 T 上 从一组等式 E(公理、公式 )能推出的所有等式的集合称为一个等式理论（通俗的解释） 代数等式理论的定理证明判断等式 M = N 是否在某个代数等式理论中 常用证明方法 把 M和 N分别化简 , 若它们的最简形式一样则相等 分别证明 M和 N都等于 L 证明 MN等于 0 还有其它方法基 本 知 识 哪种证明方法最适合于计算机自动证明？ 把 M和 N分别化简 , 若它们的最简形式一样则相等若基于所给的等式 E，能把 M和 N化简到最简形式，则这种方式相对简单，便于自动证明 分别证明 M和 N都等于 L自动选择 L是非常困难的 证明 MN等于 0不适用于非数值类型的项，例如先前给出的atom类型的表
