《Herbrand定理》由会员分享，可在线阅读，更多相关《Herbrand定理（28页珍藏版）》请在金锄头文库上搜索。
1、第3.4节 Herbrand定理,王庆江计算机科学与技术系,2007-2008学年第1学期,Herbrand定理,0. 引子,“没有一般的方法可在有限步内判定一阶逻辑的公式是永真的（或永假的）。但是，如果公式的确是永真的（或永假的），则能在有限步内判定。” Turing和Church（1936）,2007-2008学年第1学期,Herbrand定理,0. 引子,“如果公式是永真（或永假）的，1965年提出的归结法（即归结原理）能否在有限步内判定？” “对于一个公理体系，归结法能否对其所有定理在有限步内判定这些定理的成立？即归结法是否具有完备性？” 根据1929（1930）年提出的Herbran
2、d定理，上述问题的回答是肯定的。,2007-2008学年第1学期,Herbrand定理,在NS大学，他对数学的基础开始有了兴趣，并阅读Whitehead和Russell写的数学原理，立志建立法国的数学逻辑学派，以和Gttingen数学逻辑学派抗衡；他选择“数学逻辑”为博士论文研究内容，而“数学逻辑”在那时法国人不是很感兴趣。然而，作为本科生时，他就在此领域取得了突破，因而他很快在此领域取得了成功。,Jacques Herbrand(1908-1931)17岁，在法国年度“concours general”竞赛第1名（top place），并以第1名考入cole Normale Suprieur
3、e大学（07年世界大学排名83）；,2007-2008学年第1学期,Herbrand定理,1929年4月，博士论文核准提交，30年(22岁)获博士学位。同年10月，他到军队服役。在服役后，Herbrand获得Rockefeller（洛克菲勒）fellowship，允许他在欧洲各处做研究。,他首先去了柏林大学，和John von Neumann(1903年生)一起工作，呆到31年5月。从柏林又去了汉堡呆了一个月，7月去了Gttingen。离开Gttingen，在回巴黎前去阿尔卑斯山度假时，登山遇难，享年23岁。他的死是数学的悲剧性损失。Herbrand在短时间里取得大量成果，在数学逻辑领域的贡献
4、是Herbrand定理（证明于1930年）。Herbrand定理在今天机器定理证明的软件开发中有重要意义。Herbrand在代数领域还做了阿贝尔扩展的研究，在短短数月里，发表了10篇论文；,2007-2008学年第1学期,Herbrand定理,2. 概述,要证明一个公式永假，需要证明公式的每个解释都是假。如果公式的解释有无限多个，且不可列，要判定每个解释都是假，这是困难的。如果将公式在原论域D上的任一个为“真”的解释，都可表示为该公式在另一个论域上的一个为“真”的解释，且该论域上公式的解释可以无限多但可列，则公式的不可满足性证明就变得简单些了。这个论域就是H域（Herbrand univers
5、e），只要H域上该公式不可满足，则可推得公式在D域上不可满足。,2007-2008学年第1学期,Herbrand定理,3. H域,对于定义在个体域D上的谓词公式G，可找到子句集S；H0= S中的常量集；当没有常量时，由任意单个常量a组成；Hi+1=Hifm(t1, t2, , tn)，tiHi-1，fm是S中所有函数符号的集合；H称为公式G的H域；H域直接依赖G，且元素个数可列。,变量符号都应为斜体，本节课件不做修改了。,2007-2008学年第1学期,Herbrand定理,例：S = P(x), Q(y)R(z)，求H域。 解：H0 = a, H1 = H0 = a H = a。例：S =
6、P(c), Q(x)R(f(x)，求H域。 解：H0 = c, H1 = H0 f(c) = c, f(c) H2 = H1 f(c), f(f(c) = c, f(c), f(f(c) H = c, f(c), f(f(c), ,2007-2008学年第1学期,Herbrand定理,例：S = P(c), Q(f(x), R(g(x)，求H域。 解：H0 = cH1 = H0 f(c), g(c) = c, f(c), g(c)H2 = H1 f(c), g(c), f(f(c), g(f(c), f(g(c), g(g(c) = c, f(c), g(c), f(f(c), g(f(c),
7、 f(g(c), g(g(c) H = H0 H1 H2 ,二阶谓词,2007-2008学年第1学期,Herbrand定理,原子集A子句集S中各谓词取个体域中的元素值，组成的集合。A = 所有形如P(t1, t2, , tn)的元素，P(t1, t2, , tn)代表任一谓词。在H域上，ti为H域中元素，只能是常量或函数，ti称为基项（ground项），A则称为基原子集。例：S = P(c), Q(x)R(f(x)，H=c, f(c), f(f(c), 那么，A = P(c), Q(c), R(c), P(f(c), Q(f(c), R(f(c), P(f(f(c), Q(f(f(c), R(
8、f(f(c), 注意：每个谓词的个体值要取遍H域。,2007-2008学年第1学期,Herbrand定理,例：S=P(x), Q(y, f(z, b), R(a)H=a, b, f(a, a), f(b, a), f(a, b), f(b, b), f(a, f(a, a), f(a, f(b, a), f(a, f(a, b), f(a, f(b, b), f(b, f(a, a), f(b, f(b, a), f(b, f(a, b), f(b, f(b, b), f(f(a, a), a), f(f(a, a), b), f(f(a, a), f(b, a), f(f(a, a), f(
9、a, b), f(f(a, a), f(b, b), f(f(b, a), a), f(f(b, a), b), f(f(b, a), f(a, a), f(f(b, a), f(a, b), f(f(b, a), f(b, b), f(f(a, b), a), f(f(a, b), b), f(f(a, b), f(a, a), f(f(a, b), f(b, a), f(f(a, b), f(b, b), f(f(b, b), a), f(f(b, b), b), f(f(b, b), f(a, a), f(f(b, b), f(b, a), f(f(b, b), f(a, b), A=P
10、(a), Q(a, a), R(a), P(b), Q(b, a), Q(a, b), Q(b, b), R(b), P(f(a,a), Q(a, f(a, a), Q(a, f(b,a), Q(a, f(a, b), Q(a, f(b, b), ,2007-2008学年第1学期,Herbrand定理,公式G在D域上的解释在D上，对G的每个原子指定真值，则得到G相应的真值，称为G在D上的一个解释。记为I。公式G在H域上的解释在H域上，对G的每个原子指定真值，则得到G相应的真值，称为G在H上的一个解释。记为I*。,2007-2008学年第1学期,Herbrand定理,例3.24：S = P(x)
11、Q(x), R(f(y)，则H = a, f(a), f(f(a), A = P(a), Q(a), R(a), P(f(a), Q(f(a), R(f(a), P(f(f(a), Q(f(f(a), R(f(f(a), 若“P(a)”表示P(a)真值为F，则 I1*和I2*是S的H域解释。 I1* = P(a), Q(a), R(a), P(f(a), Q(f(a), R(f(a), P(f(f(a), Q(f(f(a), R(f(f(a), I2* = P(a), Q(a), R(a), P(f(a), Q(f(a), R(f(a), P(f(f(a), Q(f(f(a), R(f(f(a
12、), H一般是无限可列的，故S的H域解释也是无限可列的。,2007-2008学年第1学期,Herbrand定理,例3.24(续)： S = P(x)Q(x), R(f(y)的逻辑含义是xy(P(x)Q(x)R(f(y) 若H=t1, t2, ，则S有效，当且仅当 (P(t1)Q(t1)(P(t2)Q(t2)R(t1)R(t2) 对于I1* = P(a), Q(a), R(a), P(f(a), Q(f(a), R(f(a), P(f(f(a), Q(f(f(a), R(f(f(a), ，S| I1*=T 对于I2* = P(a), Q(a), R(a), P(f(a), Q(f(a), R(f
13、(a), P(f(f(a), Q(f(f(a), R(f(f(a), ，S| I2*=F,2007-2008学年第1学期,Herbrand定理,基例（ground instance）子句中的所有个体变量都用H元素代替，得到该子句的一个基例。S = P(x)Q(x), R(f(y)，H = a, f(a), f(f(a), 基例集是P(a)Q(a), R(a) P(f(a)Q(f(a), R(f(a), P(f(f(a)Q(f(f(a), R(f(f(a), S的一个H解释为真，当且仅当该H解释下S的所有基例都为真。S的一个H解释为假，当且仅当该H解释下S的至少一个基例为假。S在H域不可满足，当
14、且仅当S在每个H解释下为假。S在H域不可满足，当且仅当每个H解释下S至少一个子句的基例为假。问题：S在H上的不可满足性和在D上的不可满足性有什么关系呢？,2007-2008学年第1学期,Herbrand定理,定理3.2：对于论域D上的任意解释I，都存在对应I的H域解释I*，使得S|I=T，则S|I*=T。（证明略）推论： S|I*=F S|I=F这样，S在D上的不可满足性证明，转为在H上的不可满足性证明。问题：H可列但仍是无穷的，怎么在无穷个体域上证明S的不可满足性呢？,2007-2008学年第1学期,Herbrand定理,4. 语义树（Semantic tree）,语义树将H域上原子集A的元素值（即基原子值）逐层添加在一棵二叉树的边上。左分支代表基原子值为真，右分支代表基原子值为假。,2007-2008学年第1学期,Herbrand定理,例：S = P(x) Q(x), P(f(y), Q(f(y)，请画出相应的语义树。 解：H域为a, f(a), f(f(a), 原子集A为P(a), Q(a), P(f(a), Q(f(a), ,所有原子值有序地布置在二叉树上。,深度一般无限大,无穷可列的所有H域解释都被包含在语义树上。,
