代數等式理论的自动定理证明计算机科学导论一讲.pptVIP

* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 良 基 归 纳 法 良基归纳法 令?是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b ? a)为真则P(a)为真 (即?a.(?b.(b ? a ? P(b)) ? P(a)) )， 那么，对所有的a?A，P(a)为真 现在要证明的是：若有M? N 和 M? P，则N? ? ?P 若M?N, 则规定N ? M。 因是终止的系统，因此?是良基的。 归纳基础：若不存在N使得N ? M，即M是范式， 显然M具有要证明的性质 M N P 良 基 归 纳 法 良基归纳法 令?是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b ? a)为真则P(a)为真 (即?a.(?b.(b ? a ? P(b)) ? P(a)) )， 那么，对所有的a?A，P(a)为真 现在要证明的是：若有M? N 和 M? P，则N? ? ?P 归纳步骤： 1. 若M? N 或 M? P是 0步归约，显然有N? ? ?P M (N) P 良 基 归 纳 法 良基归纳法 令?是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b ? a)为真则P(a)为真 (即?a.(?b.(b ? a ? P(b)) ? P(a)) )， 那么，对所有的a?A，P(a)为真 2. 假定M? N1? N并且 M? P1? P (1) 根据局部合流性， 存在Q，使得N1? Q ?P1 M N1 P1 N P 良 基 归 纳 法 良基归纳法 令?是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b ? a)为真则P(a)为真 (即?a.(?b.(b ? a ? P(b)) ? P(a)) )， 那么，对所有的a?A，P(a)为真 2. 假定M? N1? N并且 M? P1? P (1) 根据局部合流性， 存在Q，使得N1? Q ?P1 M N1 P1 Q N P 良 基 归 纳 法 良基归纳法 令?是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b ? a)为真则P(a)为真 (即?a.(?b.(b ? a ? P(b)) ? P(a)) )， 那么，对所有的a?A，P(a)为真 2. 假定M? N1? N并且 M? P1? P (2) 由归纳假设， 存在R， 使得N? R ?Q M N1 P1 Q N P 良 基 归 纳 法 良基归纳法 令?是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b ? a)为真则P(a)为真 (即?a.(?b.(b ? a ? P(b)) ? P(a)) )， 那么，对所有的a?A，P(a)为真 2. 假定M? N1? N并且 M? P1? P (2) 由归纳假设， 存在R， 使得N? R ?Q M N1 P1 Q N R P 良 基 归 纳 法 良基归纳法 令?是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b ? a)为真则P(a)为真 (即?a.(?b.(b ? a ? P(b)) ? P(a)) )， 那么，对所有的a?A，P(a)为真 2. 假定M? N1? N并且 M? P1? P (3) 再由归纳假设， 存在S， 使得R ? S ?P M N1 P1 Q N R P 良 基 归 纳 法 良基归纳法 令?是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b ? a)为真则P(a)为真 (即?a.(?b.(b ? a ? P(b)) ? P(a)) )， 那么，对所有的a?A，P(a)为真 2. 假定M? N1? N并且 M? P1? P (3) 再由归纳假设， 存在S， 使得R ? S ?P (4) N? ? ?P得证 M N1 P1 Q N R S P Knuth-Bendix完备化过程 Knuth-Bendix完备化过程的目的 回顾 最适合于计算机自动证明代数等式M=N的方式： 把M和N分别化简, 若它们的最简形式一样则相等 由定向代数等式系统E来得到等价的重写系统R，需解决三个问题：终止性、合流性和完备性 （完备性在后面的例子中解释） 完备化过程的目的 为一个代数等式系统E，构造一个确定同样代数理论的终止且合流的重写系统R Knuth-Bendix完备化过