良基归纳法良基归纳法.ppt

代数等式理论的自动定理证明计算机科学导论第一讲计算机科学技术学院陈意云0551-63607043,******@://./~yiyun/课程内容课程内容围绕学科理论体系中的模型理论, 给定模型M,哪些问题可以由模型M解决;,如何用模型M解决问题包括程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、 给定模型M和一类问题,解决该类问题需多少资源本次讲座基于中学的等式推理,与这些内容关系不大*课程内容本讲座内容以代数等式理论中的定理证明为例,介绍怎样从中学生熟知的等式演算方法,构造等式定理的自动证明系统,即将问题变为可用计算机求解有助于理解计算思维的含义计算思维(译文)运用计算机科学的基础概念进行问题求解、系统设计、以及人类行为理解等涵盖计算机科学之广度的一系列思维活动*讲座提纲基本知识代数项、代数等式、演绎推理规则、代数等式理论、等式定理证明方法项重写系统终止性、良基关系、合流性、局部合流性、关键对良基归纳法仅举例说明Knuth-Bendix完备化过程也仅举例说明*基本知识代数项和代数等式(仅涉及一个类型)代数项 例:自然数类型nat 0,1,2,…:nat 常量 x,y:nat 变量+,f:natnatnat 二元函数 S:natnat 一元的后继函数 0,x,x+1,x+S(y)和f(100,y) 都是代数项代数等式 例:x+0=x,x+S(y)=S(x+y) x+y=z+5*基本知识代数项和代数等式(涉及多个类型)例:定义有限表:同类数据的有限序列的集合 6,17,50,28,188,92,30,67,15 ,,50,77,,, a,b,c,d,e,f,…,z (非数值数据)上述数据涉及两个类型 序列中元素的类型—数值或非数值类型 这些序列所属的类型,称为表(list)类型—非数值类型中学所学的代数概念在此已经扩展*基本知识代数项和代数等式(涉及多个类型)代数项(表类型list,表元类型atom) x:atom, l:list 变量 nil:list 零元构造函数(常量) cons:atomlistlist 构造函数first:listatom,rest:listlist观察函数 nil,cons(x,l),rest(cons(x,nil)),rest(cons(x,l)),cons(first(l),rest(l)) 都是代数项。用T表示项集代数等式(方括号列出等式中出现的变量及类型) first(cons(x,l))=x[x:atom,l:list] rest(cons(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:sM=N,x:sP=QP/xM=Q/xN基本知识x不在中P,Q是类型s的项*等式推理的例子等价代换规则:等式公理: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))根据传递规则和上面两等式M=N,x:sP=QP/xM=Q/xN基本知识*