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

* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 项 重 写 系 统 局部合流性的判定 定理 一个重写系统R是局部合流的，当且仅当对每个关键对?M, N?有M ? ? ? N 如果一个有限的重写系统R是终止的，那么该定理就给出一个算法，可用于判定R是否局部合流 * 项 重 写 系 统 局部合流、终止和合流之间的联系 定理 令R是终止的重写系统，那么R是合流的当且仅当它是局部合流的 合流蕴含局部合流（这是显然的） 反方向蕴含的证明需要使用良基归纳法 * 良 基 归 纳 法 良基归纳法 用一个简单例子说明它比自然数归纳法更一般 证明：对任何自然数的有限集合，每次删除一个元 素，最终会到达空集 1. 若忽略集合中元素的个性，只关心集合中元素 的个数，则可以用自然数归纳法 2. 若关注元素个性（虽无必要） ? ：集合之间的归约 例：{0, 1, 2} ? {0, 1} 例：{0, 2} ? {2} 3.良基关系：A ? B则A ? B * {0, 1, 2} {1, 2} {0, 2} {0, 1} {0} {1} {2} ? 良 基 归 纳 法 良基归纳法 需要证明：任何自然数的有限集合可归约到空集 1. 对所有的归约路径进行归纳 2. 良基归纳证明 归纳基础：?经0步归约到? 归纳假设：对所有的s ? s1, s ? s2, …, s ? sn, s1, s2, …, sn都能归约 到? 归纳证明：证明s能归约到? * {0, 1, 2} {1, 2} {0, 2} {0, 1} {0} {1} {2} ? 良 基 归 纳 法 良基归纳法 令?是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b ? a)为真则P(a)为真 (即?a.(?b.(b ? a ? P(b)) ? P(a)) )， 那么，对所有的a?A，P(a)为真 证明步骤： 归纳基础: 对任意不存在b使得b ? a的a，证明P(a) 在不存在b使得b ? a的情况下， ?b.(b ? a ? P(b)) ? P(a) 等价于 true ? P(a) 等价于 P(a) * 良 基 归 纳 法 良基归纳法 令?是集合A上的一个良基关系，令P是A上的某 个性质。若每当所有的P(b) (b ? a)为真则P(a)为真 (即?a.(?b.(b ? a ? P(b)) ? P(a)) )， 那么，对所有的a?A，P(a)为真 证明步骤： 归纳基础: 对任意不存在b使得b ? a的a，证明P(a) 归纳步骤：对任意存在b使得b ? a的a， ?b.(b ? a ? P(b)) ? P(a))在此转化为： 假定对所有b ? a的b，P(b)为真 归纳证明：证明P(a)为真 * 良 基 归 纳 法 良基归纳法 证明：若有M? N和 M? P，则N? ? ?P 若M?N, 则规定N?M。因系统终止, 故?是良基的 归纳基础： 若不存在N使得N ? M， 即M是范式，显然M具有 要证明的性质 因为M只能0步归约到 M本身，图上的N和P都只 能是M M N P * (M) (M) M 良 基 归 纳 法 良基归纳法 证明：若有M? N和 M? P，则N? ? ?P 若M?N, 则规定N?M。因系统终止, 故?是良基的 归纳步骤： 假定M? N1? N并且 M? P1? P (1) 根据局部合流性， 存在Q，使得N1? Q ?P1 M N1 P1 N P * 良 基 归 纳 法 良基归纳法 证明：若有M? N和 M? P，则N? ? ?P 若M?N, 则规定N?M。因系统终止, 故?是良基的 归纳步骤： 假定M? N1? N并且 M? P1? P (1) 根据局部合流性， 存在Q，使得N1? Q ?P1 M N1 P1 Q N P * 良 基 归 纳 法 良基归纳法 证明：若有M? N和 M? P，则N? ? ?P 若M?N, 则规定N?M。因系统终止, 故?是良基的 归纳步骤： 假定M? N1? N并且 M? P1? P (2) 由归纳假设， 存在R， 使得N? R ?Q M N1 P1 Q N P * 良 基 归 纳 法 良基归纳