代数等式理论的自动定理证明.ppt

代数等式理论的自动定理证明计算机科学导论第一讲课程内容课程内容讲座提纲基本知识基本知识基本知识基本知识等式证明的演绎推理规则
自反公理：MM 对称规则：
传递规则：
加变量规则：
等价代换规则：
等式推理的例子
等价代换规则：

等式公理：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))根据传递规则和上面两等式等式推理的例子
等价代换规则：

等式公理：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)) 它是基于刚才所介绍的演绎推理的
若希望计算机来自动推理，严格的推理规则是必
须提供的基本知识基本知识项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统项重写系统良基归纳法良基归纳法良基归纳法良基归纳法良基归纳法良基归纳法良基归纳法良基归纳法良基归纳法良基归纳法良基归纳法Knuth-Bendix完备化过程Knuth-Bendix完备化过程Knuth-Bendix完备化过程Knuth-Bendix完备化过程Knuth-Bendix完备化过程Knuth-Bendix完备化过程Knuth-Bendix完备化过程Knuth-Bendix完备化过程Knuth-Bendix完备化过程Knuth-Bendix完备化过程自动定理证明构造性证明与传统证明对比小结小结小结