代数等式理论自动定理证明计算机科学导论一章节.ppt

《代数等式理论自动定理证明计算机科学导论一章节.ppt》由会员分享，可在线阅读，更多相关《代数等式理论自动定理证明计算机科学导论一章节.ppt（51页珍藏版）》请在三一办公上搜索。

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是后继函数涉及多个类型的代数项若有变量 x:atom,l:list（list是atom的表类型）并有函数 nil

3、: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)都是代数项,基 本 知 识,代数等式例：x+0=x，x+S(y)=S(x+y)，x+y=z+5 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)=

4、S(S(x+y)?需要有推理规则,等式证明的演绎推理规则自反公理：M M 对称规则：传递规则：加变量规则：等价代换规则：,基 本 知 识,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(S(x+y)根据S(z)=S(z),x+S(y)=S(x+y)使用等价代换规则得到第二个等式 再利用传递规则可得要证的等式,基 本 知 识,基 本 知 识,代数等式理论（algebrai

5、c equation theory）在项集T 上从一组等式E(公理、公式)能推出的所有等式的集合称为一个等式理论（通俗的解释）代数等式理论的定理证明判断等式 M=N 是否在某个代数等式理论中常用证明方法把M和N分别化简,若它们的最简形式一样则相等分别证明M和N都等于L证明MN等于0,还有其它方法,基 本 知 识,哪种证明方法最适合于计算机自动证明？把M和N分别化简,若它们的最简形式一样则相等 若基于所给的等式E，能把M和N化简到最简形式，则这种方式相对简单，便于自动证明分别证明M和N都等于L 自动选择L是非常困难的证明MN等于0 不适用于非数值类型的项，例如先前给出的atom类型的表,项 重

6、写 系 统,自动证明要解决的问题项集T 上等式集E中的等式要定向为单向项重写规则,构成重写规则集R,以方便计算机对项化简例如：x+0=x，x+S(y)=S(x+y)x 0=0，x S(y)=x y+x定向成如下的项重写系统Rx+0 x，x+S(y)S(x+y)x 0 0，x S(y)x y+x记号M N：用一条规则可将项M归约成N例如，x+S(S(y)S(x+S(y)S(S(x+y)两步重写都使用规则x+S(y)S(x+y),“”既用于规则，也用于项的归约,项 重 写 系 统,自动证明要解决的问题项集T 上等式集E中的等式要定向为单向项重写规则,构成重写规则集R,以方便计算机对项化简例如：x+

7、0=x，x+S(y)=S(x+y)x 0=0，x S(y)=x y+x定向成如下的项重写系统Rx+0 x，x+S(y)S(x+y)x 0 0，x S(y)x y+x记号M N：用一条规则可将项M归约成N通过定向等式来得到确定同样代数理论的重写系统，需解决三个问题：终止性、合流性和完备性,“”既用于规则，也用于项的归约,项 重 写 系 统,终止性1.终止性项集T 上的R不存在无穷归约序列M0M1M2,即:任何项都能归约到范式(不能再归约的项)2.有时很难对等式定向，以得到终止的重写系统例如：对由三角函数公式构成的等式系统 和角公式:sin(+)=sin cos+cos sin,差角公式:sin(

8、)=sin cos cos sin,积化和差:sin cos=(sin(+)+sin()/2,和差化积:sin+sin=2sin(+)/2)cos()/2),项 重 写 系 统,终止性3.定义：良基关系（良基：well-founded）集合A上的一个关系是良基的，若不存在A上元素的无穷递减序列a0 a1 a2（a b iff b a）例：自然数上的关系是良基的，但关系不是4.若项集T 和有良基的集合A有映射f:T A,满足T 上任意归约序列 M0 M1 M2 Mn f f f fA上存在递减序列 a0 a1 a2 an 则T 上不存在无穷的归约序列,项 重 写 系 统,终止性5.定理 令R是项

9、集T 上的一个重写系统，若能找到有良基关系的集合A和映射f:T A，使得对R中每条规则L R都有f(L)f(R),那么R是终止的6.f 的选择基于项的语法特点，或者给项指派一种语义 例1（基于语法特点：根据两边项语法上的繁简）first(cons(x,l)xrest(cons(x,l)l,项 重 写 系 统,终止性例2（逻辑运算系统，给项指派一种语义）x x A N 0,1(x y)(x y)A(x,y)=x+y+1(x y)(x y)A(x,y)=x yx(y z)(x y)(x z)A(x)=2x(y z)x(y x)(z x)A表示f 映射算符的结果，它是A上的二元函数对每条规则L R，

10、都有f(L)f(R)规则1：x 1,有 x规则2：x,y 1,有2(x+y+1)=2x2y2 2x2y,项 重 写 系 统,合流性1.记号 MN：M经若干步(含0步)重写后得到N NM：若有MN M N：若存在P，使得MP且NP2.定义 令R是项集T 上的重写系统,若N M P 蕴涵N P，则R是合流的3.定义 令R是项集T 上的重写系统,若N M P 蕴涵N P，则R是局部合流的 局部合流关系严格弱于合流关系先考虑局部合流的判定方法，然后再考虑合流,项 重 写 系 统,局部合流性的判定1.讨论所选用的例子函数：nil:listcons:atom list list first:list at

11、om，rest:list list cond:bool list list list等式：first(cons(x,l)=x,rest(cons(x,l)=l,cons(first(l),rest(l)=l,下面的讨论选择如下两条定向后的重写规则：rest(cons(x,l)lcons(first(l),rest(l)l,项 重 写 系 统,局部合流性的判定(1)无重叠的归约 归约规则：rest(cons(x,l)l（规则LR）cons(first(l),rest(l)l（规则LR）待归约项：cond(B,rest(cons s l),cons(first(l),rest(l)特点：M中无重叠

12、子项的归约相互不受影响,项 重 写 系 统,局部合流性的判定(1)无重叠的归约图示：LR 和LR是规则图中SL表示代换S作用 于L的结果代换是变量到项的映射,项 重 写 系 统,局部合流性的判定(2)平凡的重叠 归约规则：rest(cons(x,l)l（规则LR）cons(first(l),rest(l)l（规则LR）待归约项：rest(cons(x,cons(first(l),rest(l)特点：SL是SL的子项，且S把L中的某变量(这里是l)用由SL构成的项代换 不同的第1步归约不会影响局部合流，但合流所需归约步数可能不一样（取决于R中有几个l）,项 重 写 系 统,局部合流性的判定(2)

13、平凡的重叠图示：SL是SL的子项，且S把 L中的某变量x用有SL 构成的项代换不同的第1步归约不会影响局部合流，但合流所需归约步数可能不一样,项 重 写 系 统,局部合流性的判定(3)非平凡的重叠 归约规则：rest(cons(x,l)l（规则LR）cons(first(l),rest(l)l（规则LR）待归约项：rest(cons(first(l),rest(l)特点：SL在SL的非变量位置LR 或LR的使用都可能使对方在原定位置 不能使用，故不能保证局部合流,项 重 写 系 统,局部合流性的判定(3)非平凡的重叠图示：SL在SL的非变量位置LR或LR的使用都可能使对方在原定位置不能使用，故

14、不能保证局部合流,项 重 写 系 统,局部合流性的判定若所有含非平凡重叠的项都能局部合流,则R也能把对所有含非平凡重叠的项的检查缩小为对有限的重写规则集的检查 若由R的重写规则确定的所有关键对(critical pair)都能归约到同一个项，则所有项的非平凡重叠都能局部合流（可以证明，但在此不深究）例：重写规则rest(cons(x,l)l，和 cons(first(l),rest(l)l会形成两个关键对,项 重 写 系 统,第1个关键对：选适当的代换，使得两规则代换后绿色部分一样cons(first(l),rest(l)l rest(cons(x,l)l第1条规则中的l用cons(x,l)代

15、换后,其左部是项：cons(first(cons(x,l),(rest(cons(x,l)用这两条规则化简上述项可得第1个关键对：cons(x,l),cons(first(cons(x,l),l)归约关键对：cons(x,l)已经是范式 cons(first(cons(x,l),l)cons(x,l)第1个关键对能归约到同一个项,项 重 写 系 统,第2个关键对：选适当的代换，使得两规则代换后绿色部分一样 cons(first(l),rest(l)lrest(cons(x,l)l第2条规则中的x和l分别代换成first(l)和rest(l)后,其左部是项：rest(cons(first(l),

16、rest(l)用这两条规则化简上述项可得第2个关键对：rest(l),rest(l)显然，第2个关键对也能归约到同一个项,项 重 写 系 统,局部合流性的判定定理 一个重写系统R是局部合流的，当且仅当对每个关键对M,N有M N如果一个有限的重写系统R是终止的，那么该定理就给出一个算法，可用于判定R是否局部合流,项 重 写 系 统,局部合流、终止和合流之间的联系定理 令R是终止的重写系统，那么R是合流的当且仅当它是局部合流的合流蕴含局部合流反方向蕴含的证明需要使用良基归纳法,良 基 归 纳 法,良基归纳法令是集合A上的一个良基关系，令P是A上的某个性质。若每当所有的P(b)(b a)为真则P(a

17、)为真(即a.(b.(b a P(b)P(a)，那么，对所有的aA，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)，那么，对所有的aA，P(a)为真证明步骤：归纳基础:对任意不存在b使得b a的a，证明P(a)归纳步骤：对任意存在b使得b a的a，b.(b a P(b)P(a)的含义是 假定对所有b

18、 a的b，P(b)为真，然后证明P(a)为真,良 基 归 纳 法,良基归纳法令是集合A上的一个良基关系，令P是A上的某个性质。若每当所有的P(b)(b a)为真则P(a)为真(即a.(b.(b a P(b)P(a)，那么，对所有的aA，P(a)为真现在要证明的是：若有M N和 M P，则N P若MN,则规定N M。因是终止的系统，因此是良基的。归纳基础：若不存在N使得N M，即M是范式，显然M具有要证明的性质,良 基 归 纳 法,良基归纳法令是集合A上的一个良基关系，令P是A上的某个性质。若每当所有的P(b)(b a)为真则P(a)为真(即a.(b.(b a P(b)P(a)，那么，对所有的a

19、A，P(a)为真现在要证明的是：若有M N和 M P，则N P归纳步骤：1.若M N 或 M P是0步归约，显然有N P,良 基 归 纳 法,良基归纳法令是集合A上的一个良基关系，令P是A上的某个性质。若每当所有的P(b)(b a)为真则P(a)为真(即a.(b.(b a P(b)P(a)，那么，对所有的aA，P(a)为真2.假定M N1 N并且M P1 P(1)根据局部合流性，存在Q，使得N1 Q P1,良 基 归 纳 法,良基归纳法令是集合A上的一个良基关系，令P是A上的某个性质。若每当所有的P(b)(b a)为真则P(a)为真(即a.(b.(b a P(b)P(a)，那么，对所有的aA，

20、P(a)为真2.假定M N1 N并且M P1 P(1)根据局部合流性，存在Q，使得N1 Q P1,良 基 归 纳 法,良基归纳法令是集合A上的一个良基关系，令P是A上的某个性质。若每当所有的P(b)(b a)为真则P(a)为真(即a.(b.(b a P(b)P(a)，那么，对所有的aA，P(a)为真2.假定M N1 N并且M P1 P(2)由归纳假设，存在R，使得N R Q,良 基 归 纳 法,良基归纳法令是集合A上的一个良基关系，令P是A上的某个性质。若每当所有的P(b)(b a)为真则P(a)为真(即a.(b.(b a P(b)P(a)，那么，对所有的aA，P(a)为真2.假定M N1 N

21、并且M P1 P(2)由归纳假设，存在R，使得N R Q,M,良 基 归 纳 法,良基归纳法令是集合A上的一个良基关系，令P是A上的某个性质。若每当所有的P(b)(b a)为真则P(a)为真(即a.(b.(b a P(b)P(a)，那么，对所有的aA，P(a)为真2.假定M N1 N并且M P1 P(3)再由归纳假设，存在S，使得R S P,M,良 基 归 纳 法,良基归纳法令是集合A上的一个良基关系，令P是A上的某个性质。若每当所有的P(b)(b a)为真则P(a)为真(即a.(b.(b a P(b)P(a)，那么，对所有的aA，P(a)为真2.假定M N1 N并且M P1 P(3)再由归纳

22、假设，存在S，使得R S P(4)N P得证,Knuth-Bendix完备化过程,Knuth-Bendix完备化过程的目的回顾最适合于计算机自动证明代数等式M=N的方式：把M和N分别化简,若它们的最简形式一样则相等由定向代数等式系统E来得到等价的重写系统R，需解决三个问题：终止性、合流性和完备性（完备性在后面的例子中解释）完备化过程的目的为一个代数等式系统E，构造一个确定同样代数理论的终止且合流的重写系统R,Knuth-Bendix完备化过程,Knuth-Bendix完备化过程简介1.把E定向成一个终止的重写系统R（若定向失败，则完备化过程失败）2.检查R的局部合流性并进行完备化for(R的每

23、个关键对M,N)if(不具备M N)把MN或NM加入R（原因稍后解释）（若定向失败，则完备化过程失败）(过程可能因R不断地被加入规则而不终止)3.最终的R为所求,Knuth-Bendix完备化过程,例作为输入的等式系统E如下f(x)f(y)=f(x+y)(x+y)+z=x+(y+z)1.先定向成一个终止的重写系统R f(x)f(y)f(x+y)(x+y)+z x+(y+z)2.检查局部合流性并进行完备化,Knuth-Bendix完备化过程,例作为输入的等式系统E如下f(x)f(y)=f(x+y)(x+y)+z=x+(y+z)1.先定向成一个终止的重写系统R f(x)f(y)f(x+y)(x+y

24、)+z x+(y+z)2.检查局部合流性并进行完备化(1)把两条规则左部的绿色部分进行合一，产生一个临界对 f(x+y)+z,f(x)+(f(y)+z)临界对的两个项都已最简，这个临界对不能合流,第2条规则左部的合一结果：(f(x)f(y)+z,Knuth-Bendix完备化过程,例作为输入的等式系统E如下f(x)f(y)=f(x+y)(x+y)+z=x+(y+z)1.先定向成一个终止的重写系统R f(x)f(y)f(x+y)(x+y)+z x+(y+z)2.检查局部合流性并进行完备化(1)把两条规则左部的绿色部分进行合一，产生一个临界对 f(x+y)+z,f(x)+(f(y)+z)(2)增加

25、重写规则f(x+y)+z f(x)+(f(y)+z),第2条规则左部的合一结果：(f(x)f(y)+z,Knuth-Bendix完备化过程,例解释：增加规则f(x+y)+z f(x)+(f(y)+z)的原因在E中可证f(x+y)+z和f(x)+(f(y)+z)相等等式：f(x)f(y)=f(x+y)和(x+y)+z=x+(y+z)证明：f(x+y)+z=f(x)f(y)+z=f(x)+(f(y)+z)在未加上述重写规则R中证明不了,即R不完备：在R中能证的等式在E中能证，但存在E中能证而在R中不能证的等式向R中加规则是为了完备性,Knuth-Bendix完备化过程,例（续）1.先定向成一个终止

26、的重写系统R f(x)f(y)f(x+y)(x+y)+z x+(y+z)2.检查局部合流性并进行完备化(1)产生一个临界对 f(x+y)+z,f(x)+(f(y)+z)(2)增加重写规则f(x+y)+z f(x)+(f(y)+z)(3)R扩大为：f(x)f(y)f(x+y)(x+y)+z x+(y+z)f(x+y)+z f(x)+(f(y)+z),Knuth-Bendix完备化过程,例（续）1.先定向成一个终止的重写系统R f(x)f(y)f(x+y)(x+y)+z x+(y+z)2.检查局部合流性并进行完备化(1)产生一个临界对 f(x+y)+z,f(x)+(f(y)+z)(2)增加重写规则

27、f(x+y)+z f(x)+(f(y)+z)(3)R扩大为：f(x)f(y)f(x+y)(x+y)+z x+(y+z)f(x+y)+z f(x)+(f(y)+z)两条规则中的绿色部分也可以合一,Knuth-Bendix完备化过程,例（续）1.先定向成一个终止的重写系统R f(x)f(y)f(x+y)(x+y)+z x+(y+z)2.检查局部合流性并进行完备化(1)产生一个临界对 f(x+y)+z,f(x)+(f(y)+z)(2)增加重写规则f(x+y)+z f(x)+(f(y)+z)(3)R扩大为：f(x)f(y)f(x+y)(x+y)+z x+(y+z)f(x+y)+z f(x)+(f(y)

28、+z)将产生无数规则:f n(x+y)+z f n(x)+(f n(y)+z),完备化过程因不断产生新的规则而不终止,构造性证明与传统证明对比,传统证明的一个例子证明根据 是有理数或无理数来讨论,若 是有理数，则取x=3若是无理数，则取x=这种非构造性证明不太可能由计算机自动得到,小 结,本讲座小结以代数等式理论中的定理证明为例，介绍怎样从熟知的等式演算方法，构造自动定理证明系统不同逻辑的自动定理证明方法不同自动定理证明的应用集成电路设计程序验证程序分析相关课程数理逻辑、人工智能,小 结,工具交互式定理证明辅助工具Coqhttp:/coq.inria.fr/，获ACM2013年度软件系统奖自动定理证明器Z31.http:/redmond/projects/z3/old/index.html2.http:/Kroening and Ofer Strichman，Decision Procedures:An Algorithmic Point of View(Texts in Theoretical Computer Science.An EATCS Series),