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

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

1、代数等式理论的自动定理证明计算机科学导论第一讲,计算机科学技术学院陈意云0551-63607043,http:/,课 程 内 容,课程内容围绕学科理论体系中的模型理论,程序理论和计算理论1.模型理论关心的问题 给定模型M，哪些问题可以由模型M解决；如何比较模型的表达能力2.程序理论关心的问题给定模型M，如何用模型M解决问题包括程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等3.计算理论关心的问题给定模型M和一类问题,解决该类问题需多少资源,本次讲座基于中学的等式推理,与这些内容关系不大,2,课 程 内 容,本讲座内容以代数等式理论中的定理证明为例，介绍怎样从中学生熟

2、知的等式演算方法，构造等式定理的自动证明系统，即将问题变为可用计算机求解有助于理解计算思维的含义计算思维（译文）运用计算机科学的基础概念进行问题求解、系统设计、以及人类行为理解等涵盖计算机科学之广度的一系列思维活动,3,讲 座 提 纲,基本知识代数项、代数等式、演绎推理规则、代数等式理论、等式定理证明方法项重写系统终止性、良基关系、合流性、局部合流性、关键对良基归纳法仅举例说明Knuth-Bendix完备化过程也仅举例说明,4,基 本 知 识,代数项和代数等式（仅涉及一个类型）代数项例：自然数类型nat 0,1,2,:nat常量 x,y:nat变量+,f:nat nat nat 二元函数 S:

3、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,5,基 本 知 识,代数项和代数等式（涉及多个类型）例：定义有限表：同类数据的有限序列的集合 6,17,50,28,188,92,30,67,15 18.8,9.2,50,77,8.6,5.5,40.0 a,b,c,d,e,f,z（非数值数据）上述数据涉及两个类型 序列中元素的类型 数值或非数值类型 这些序列所属的类型，称为表（list）类型 非数值类型中学所学的代数概念在此已经扩展,6,基 本 知 识,代数项和代数等式（涉及多个类型）代数项（

4、表类型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,7,基 本 知 识,等式证明例：基于一组等

5、式（公式、公理）：x+0=x 和 x+S(y)=S(x+y)怎么证明等式：x+S(S(y)=S(S(x+y)?需要有推理规则,8,等式证明的演绎推理规则自反公理：M M 对称规则：传递规则：加变量规则：等价代换规则：,基 本 知 识,x不在中,P,Q 是类型s的项,9,等式推理的例子等价代换规则：等式公理：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)使用

6、等价代换规则得到第二个等式x+S(S(y)=S(S(x+y)根据传递规则和上面两等式,基 本 知 识,10,等式推理的例子等价代换规则：等式公理：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)它是基于刚才所介绍的演绎推理的若希望计算机来自动推理，严格的推理规则是必须提供的,基 本 知 识,11,基 本 知 识,代数等式理论（algebraic equation theory）在项集T 上从一组等式E（公理）能推出的所有等式的集合称为一个等式理论（通俗的解释）代数等式理论的定理证

7、明判断等式 M=N 是否在某个代数等式理论中常用证明方法把M和N分别化简,若它们的最简形式一样则相等分别证明M和N都等于L证明MN等于0还有其他方法,12,基 本 知 识,哪种证明方法最适合于计算机自动证明？把M和N分别化简,若它们的最简形式一样则相等 若基于等式E，通过等式证明，把M和N化简到最简形式，则这种方式相对简单，便于自动证明 并且采用适合于计算机使用的单向重写规则分别证明M和N都等于L 自动选择L是非常困难的证明MN等于0 不适用于非数值类型的项，例如先前给出的atom类型的表,13,项 重 写 系 统,自动证明要解决的问题项集T 上等式集E中的等式要定向为单向项重写规则,构成重写

8、规则集R,以方便计算机对项化简若E是：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 若规则LRR，含z一次出现的项T，以及使得SL/zTT的代换S，则SL/zT SR/zT,“”既用于规则，也用于项的归约,14,项 重 写 系 统,自动证明要解决的问题项集T 上等式集E中的等式要定向为单向项重写规则,构成重写规则集R,以方便计算机对项化简若E是：x+0=x，x+S(y)=S(x+y)x 0=0，x S(y)=x y+x定向成如下的项重

9、写系统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),“”既用于规则，也用于项的归约,15,项 重 写 系 统,自动证明要解决的问题项集T 上等式集E中的等式要定向为单向项重写规则,构成重写规则集R,以方便计算机对项化简若E是：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(x+S(y)/zz S(S(x+y)/zz

10、,16,代换S：xx yS(y),项 重 写 系 统,自动证明要解决的问题项集T 上等式集E中的等式要定向为单向项重写规则,构成重写规则集R,以方便计算机对项化简若E是：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)子项能与第2条规则的左部匹配,17,项 重 写 系 统,自动证明要解决的问题问题1：如何从E得到R，保证项的化简能终止例：若有规则 x+y=y+x，不管怎么定向都有 a+b

11、 b+a a+b 问题2：如何从E得到R，保证对项采用不同化简策略所得最简项是唯一的（合流性）E：=S(),Eq(x,x)=true,Eq(x,S(x)=falseR：S(),Eq(x,x)true,Eq(x,S(x)false,18,项 重 写 系 统,自动证明要解决的问题问题1：如何从E得到R，保证项的化简能终止例：若有规则 x+y=y+x，不管怎么定向都有 a+b b+a a+b 问题2：如何从E得到R，保证对项采用不同化简策略所得最简项是唯一的（合流性）R：S(),Eq(x,x)true,Eq(x,S(x)false则有：Eq(,)true Eq(,)Eq(,S()false问题3：如

12、何从E得到R,使得E和R确定同样的代数理论，即在E中能证则在R中也能证（完备性）,19,项 重 写 系 统,问题一：终止性1.终止性 项集T 上的R不存在无穷归约序列M0M1M2,即:任何项都能归约到范式(不能再归约的项)2.有时很难对等式定向，以得到终止的重写系统例如：对由三角函数公式构成的等式系统 和角公式:sin(+)=sin cos+cos sin,差角公式:sin()=sin cos cos sin,积化和差:sin cos=(sin(+)+sin()/2,和差化积:sin+sin=2sin(+)/2)cos()/2),20,项 重 写 系 统,问题一：终止性3.定义：良基关系（良基

13、：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 上不存在无穷的归约序列,21,项 重 写 系 统,问题一：终止性5.定理令R是项集T 上的一个重写系统，若能找到有良基关系的集合A和映射f:T A，使得对R中每条规则L R都有f(L)f(R),那么R是终止的注：由此定理，判断R的终止性成为可能6.f 的选择基于项的语法特点，或者给

14、项指派一种语义例1（基于语法特点：根据两边项语法上的繁简）first(cons(x,l)xrest(cons(x,l)l,22,项 重 写 系 统,问题一：终止性例2（逻辑运算系统）x x：就是C中的&(x y)(x y)：就是C中的|(x y)(x y)：就是C中的！x(y z)(x y)(x z)(y z)x(y x)(z x),23,项 重 写 系 统,问题一：终止性例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)语

15、义指派f 应用到T、和的结果分别是A、A、A和A，后三者都是A上的二元或一元函数对每条规则L R，都有f(L)f(R)规则1：x 1,有 x规则2：x,y 1,有2(x+y+1)=2x2y2 2x2y,24,项 重 写 系 统,问题二：合流性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是局部合流的 局部合流关系严格弱于合流关系先考虑局部合流的判定方法，然后再考虑合流的判定方法,25,项 重 写 系

16、统,插曲在介绍局部合流性之前，先介绍代数项的树形表示代数项cons(first(cons(x,l),rest(cons(y,l)的树形表示倒长的树：根在上，叶在下每棵子树代表一个子项，整个树代表完整的代数项,26,项 重 写 系 统,局部合流性的判定（问题二的子问题）1.讨论所选用的例子函数：nil:listcons:atom list list first:list atom，rest:list list cond:bool list list list等式：first(cons(x,l)=x,rest(cons(x,l)=l,cons(first(l),rest(l)=l,下面的讨论针对如

17、下两条重写规则：rest(cons(x,l)lcons(first(l),rest(l)l,27,项 重 写 系 统,局部合流性的判定（问题二的子问题）(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)方式1:原式 cond(B,l,cons(first(l),rest(l)cond(B,l,l)方式2:原式 cond(B,rest(cons s l),l)cond(B,l,l)特点：M中无重叠子项的归约相互不受影响,28

18、,项 重 写 系 统,局部合流性的判定(1)无重叠的归约图示：LR 和LR是规则图中SL和SR分别表示 代换S作用于L的 结果 S:T T代换S的最主要部分是把变量映射到项,29,cond(B,rest(cons s l),cons(first(l),rest(l),项 重 写 系 统,局部合流性的判定（问题二的子问题）(2)平凡的重叠 归约规则：rest(cons(x,l)l（规则LR）cons(first(l),rest(l)l（规则LR）待归约项：rest(cons(x,cons(first(l),rest(l)方式1:原式 cons(first(l),rest(l)l 方式2:原式 r

19、est(cons(x,l)l,30,项 重 写 系 统,局部合流性的判定（问题二的子问题）(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）,31,项 重 写 系 统,局部合流性的判定(2)平凡的重叠 图示：SL是SL的子项，且S把L中的某变量x用有SL构成的项代换不同的第1步归约不会影

20、响局部合流，但合流所需归约步数可能不一样,32,rest(cons(x,cons(first(l),rest(l),项 重 写 系 统,局部合流性的判定（问题二的子问题）(3)非平凡的重叠 归约规则：rest(cons(x,l)l（规则LR）cons(first(l),rest(l)l（规则LR）待归约项：rest(cons(first(l),rest(l)方式1:原式 rest(l)（用规则LR）方式2:原式 rest(l)（用规则LR）该例比较特殊，都一步归约就到范式,33,项 重 写 系 统,局部合流性的判定（问题二的子问题）(3)非平凡的重叠 归约规则：rest(cons(x,l)l（

21、规则LR）cons(first(l),rest(l)l（规则LR）待归约项：rest(cons(first(l),rest(l)特点：SL在SL的非变量位置LR 或LR的使用都可能使对方在原定位置 不能使用，故不能保证局部合流,34,项 重 写 系 统,局部合流性的判定(3)非平凡的重叠 图示：SL在SL的非变量位置LR或LR的使用都可能使对方在原定位置不能使用，故不能保证局部合流,35,rest(cons(first(l),rest(l),项 重 写 系 统,局部合流性的判定若所有含非平凡重叠的项都能局部合流,则R也能把对所有含非平凡重叠的项的检查缩小为对有限的重写规则集的检查 若由R的重写

22、规则确定的所有关键对(critical pair)都能归约到同一个项，则所有项的非平凡重叠都能局部合流（课堂上不介绍）例：重写规则rest(cons(x,l)l，和 cons(first(l),rest(l)l会形成两个关键对,36,项 重 写 系 统,第1个关键对：（课堂上不介绍）选适当的代换，使得两规则代换后绿色部分一样cons(first(l),rest(l)l rest(cons(x,l)l第1条规则中的l用cons(x,l)代换后,其左部是项：cons(first(cons(x,l),(rest(cons(x,l)用这两条规则化简上述项可得第1个关键对：cons(x,l),cons(

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

24、 系 统,局部合流性的判定定理 一个重写系统R是局部合流的，当且仅当对每个关键对M,N有M N如果一个有限的重写系统R是终止的，那么该定理就给出一个算法，可用于判定R是否局部合流,39,项 重 写 系 统,局部合流、终止和合流之间的联系定理 令R是终止的重写系统，那么R是合流的当且仅当它是局部合流的合流蕴含局部合流（这是显然的）反方向蕴含的证明需要使用良基归纳法,40,良 基 归 纳 法,良基归纳法用一个简单例子说明它比自然数归纳法更一般证明：对任何自然数的有限集合，每次删除一个元 素，最终会到达空集 1.若忽略集合中元素的个性，只关心集合中元素的个数，则可以用自然数归纳法 2.若关注元素个性

25、（虽无必要）：集合之间的归约规则:x1,xnx2,xn其中x1是左边集合的任意元素 3.良基关系：A B则A B,41,良 基 归 纳 法,良基归纳法需要证明：任何自然数的有限集合可归约到空集1.对所有的归约路径进行归纳2.良基归纳证明归纳基础：经0步归约到归纳假设：对所有的s s1,s s2,s sn,s1,s2,sn都能归约到归纳证明：证明s能归约到,42,良 基 归 纳 法,良基归纳法（课堂上不介绍）令是集合A上的一个良基关系，令P是A上的某个性质。若每当所有的P(b)(b a)为真则P(a)为真(即a.(b.(b a P(b)P(a)，那么，对所有的aA，P(a)为真证明步骤：归纳基础

26、:对任意不存在b使得b a的a，证明P(a)在不存在b使得b a的情况下，b.(b a P(b)P(a)等价于 true P(a)等价于 P(a),43,良 基 归 纳 法,良基归纳法（课堂上不介绍）令是集合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 a的b，P(b)为真，然后证明：归纳证明：证明P(a)为真,44,

27、良 基 归 纳 法,用良基归纳法证明合流性证明：若有M N和 M P，则N P若MN,则规定NM。因系统终止,故是良基的归纳基础：若不存在N使得N M，即M是范式，显然M具有要证明的性质 因为M只能0步归约到M本身，图上的N和P都只能是M,45,良 基 归 纳 法,用良基归纳法证明合流性证明：若有M N和 M P，则N P若MN,则规定NM。因系统终止,故是良基的归纳步骤：假定M N1 N并且M P1 P(1)根据局部合流性，存在Q，使得N1 Q P1,46,良 基 归 纳 法,用良基归纳法证明合流性证明：若有M N和 M P，则N P若MN,则规定NM。因系统终止,故是良基的归纳步骤：假定M

28、 N1 N并且M P1 P(1)根据局部合流性，存在Q，使得N1 Q P1,47,良 基 归 纳 法,用良基归纳法证明合流性证明：若有M N和 M P，则N P若MN,则规定NM。因系统终止,故是良基的归纳步骤：假定M N1 N并且M P1 P(2)由归纳假设，存在R，使得N R Q,48,良 基 归 纳 法,用良基归纳法证明合流性证明：若有M N和 M P，则N P若MN,则规定NM。因系统终止,故是良基的归纳步骤：假定M N1 N并且M P1 P(2)由归纳假设，存在R，使得N R Q,M,49,良 基 归 纳 法,用良基归纳法证明合流性证明：若有M N和 M P，则N P若MN,则规定N

29、M。因系统终止,故是良基的归纳步骤：假定M N1 N并且M P1 P(3)再由归纳假设，存在S，使得R S P,M,50,良 基 归 纳 法,用良基归纳法证明合流性证明：若有M N和 M P，则N P若MN,则规定NM。因系统终止,故是良基的归纳步骤：假定M N1 N并且M P1 P(3)再由归纳假设，存在S，使得R S P(4)N P得证,51,Knuth-Bendix完备化过程,问题三：完备性回顾最适合于计算机自动证明代数等式M=N的方式：把M和N分别化简,若它们的最简形式一样则相等由定向代数等式系统E来得到等价的重写系统R，需解决三个问题：终止性、合流性和完备性完备性：从E可得到R，E和

30、R确定同样的代数理论概要介绍Knuth-Bendix完备化过程 给出一个完备化过程不终止的例子。由此可知，并非对任何E都可以得到与之有同样代数理论的R,52,Knuth-Bendix完备化过程,Knuth-Bendix完备化过程的目的完备化过程的目的为一个代数等式系统E，构造一个确定同样代数理论的终止且合流的重写系统R,53,Knuth-Bendix完备化过程,Knuth-Bendix完备化过程简介1.把E定向成一个终止的重写系统R（若定向失败，则完备化过程失败）2.检查R的局部合流性并进行完备化for(R的每个关键对M,N)if(不具备M N)把MN或NM加入R（原因稍后解释）（若定向失败，

31、则完备化过程失败）(过程可能因R不断地被加入规则而不终止)3.最终的R为所求,54,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.检查局部合流性并进行完备化,55,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.检查局部合

32、流性并进行完备化(1)把两条规则左部的绿色部分进行合一，产生一个临界对 f(x+y)+z,f(x)+(f(y)+z)临界对的两个项都已最简，这个临界对不能合流,因第2条规则左部的合一结果：(f(x)f(y)+z,56,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)增加重写规则f

33、(x+y)+z f(x)+(f(y)+z),因第2条规则左部的合一结果：(f(x)f(y)+z,57,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中加规则是为了完备性,58,Knuth-Bendix完备化过程,例（续

34、）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)+z),59,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(

35、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)两条规则中的绿色部分也可以合一,60,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(

36、x+y)+z f(x)+(f(y)+z)将产生无数规则:f n(x+y)+z f n(x)+(f n(y)+z),完备化过程因不断产生新的规则而不终止,61,自 动 定 理 证 明,不同逻辑的自动定理证明方法可能不一样本讲座介绍代数等式理论的自动定理证明，并未彻底解决其他还有：命题逻辑的自动定理证明几何定理的自动证明 多种理论组合的自动定理证明其中有些已彻底解决，有些在一定约束下可以解决,62,构造性证明与传统证明对比,传统证明的一个例子证明根据 是有理数或无理数来讨论,若 是有理数，则取x=3若是无理数，则取x=这种非构造性证明不太可能由计算机自动得到,63,小 结,本讲座小结以代数等式理论

37、中的定理证明为例，介绍怎样从熟知的等式演算方法，构造自动定理证明系统不同逻辑的自动定理证明方法不同自动定理证明的应用集成电路设计程序验证程序分析相关课程数理逻辑、人工智能,64,小 结,工具交互式定理证明辅助工具Coqhttp:/coq.inria.fr/，获ACM 2013年度软件系统奖自动定理证明器Z31.http:/redmond/projects/z3/old/index.html2.http:/2015年度编程语言软件奖,65,小 结,参考文献Daniel Kroening and Ofer Strichman，Decision Procedures:An Algorithmic Point of View(Texts in Theoretical Computer Science.An EATCS Series)陈意云、张昱，程序设计语言理论（第二版），高等教育出版者，2010年2月 备注：本次课的内容取自该书前两章中有关代数数据类型的部分,66,