归结原理 人工智能-智能人工黑箱法则

6.1子句集的Herbrand域Herbrand域与Herbrand解释定义（Herbrand域）H0是出现于子句集S的常量符号集。如果S中无常量符号出现，则H0由一个常量符号a组成。Hi-1｛所有形如f(t1，…，tn)的项的集合｝其中f(t1，…，tn)是出现在S中的所有n元函数符号，tjHi-1归结原理 人工智能，j＝1，…，n．基：把对象中的变量用常量代替后得到的无变量符号出现的对象。基项、基项集、基原子、基原子集合、基文字、基子句、基子句集定义(原子集、Herbrand底))的基原子集合，称为S的Herbrand底或S的原子集．其中P(x定义（基例）设S是子句集，C是S中的一个子句．用S的H域中元素代替C中所有变量所得到的基子句称为子句C的基例。是S的原子集。于是S的一个H解释I可方便地表示为如下一个集合：S的普通解释不一定是S的H解释：普通解释不是必须定义在H域上，即使定义在H域上，也不一定是一个H解释。任取普通解释I，依照I，可以按如下方法构造S的一个H解释I*，使得若令S的一个解释I如下：D＝{1，2}指定a对应1得H解释：指定a对应2得H解释：定义（对应于I的H解释I*）设I是子句集S在区域D上的解释。

是出现在S中所有常量符号的集合。对任意aH对应于I的H解释I*是如下的一个H解释：任取S中n元谓词符号P(x7/8/201410引理如果某区域D上的解释I满足子句集S，定理子句集S恒假当且仅当S被其所有H解释弄证明:必要性显然。充分性。假设S被其所有H解释弄假，而S又是可满足的。设解释I满足S，于是由引理知，对应于I的H解释I*也满足7/8/201411l）子句2）子句C被解释I满足，当且仅当C的每一个基例都被I满足．3）子句C被解释至少有一个C的基例C’被I弄假。4）子句集S不可满足，当且仅当对每个解释I，至少有一个S中某个子句C的基例C’被I弄假。7/8/2014127/8/2014136.2HerbrandHerbrand定理是符号逻辑中一个很重要的定理．Herbrand定理就是使用语义树的方法，把需要考虑无穷个H解释的问题，变成只考虑有限个解释的问题．7/8/201414一、语义树A是原子，两个文字A和～A都是另一个的补，集合｛A，～A｝称为一个互定义(Tautology,重言式)含有互补对的子句．7/8/201415定义（语义树）设S是子句集，A是S的原子集．关于S的语义树是一棵向下生长的树T．在树的每一节上都以如下方式附着A中有限个原子或原子否定的集合：1）对于树中每一个节点N，只能向下引出有限的直接的节是一个恒真的命题公式．2）对树中每一个节点并包含N的一个分枝的所有节上附着文字的并集，则I（N）不含有任意的互补对．语义树7/8/201416定义（部分解释）对于子句集S的语义树中的每一个节点N归结原理 人工智能，I(N)是S的某个解释的子集，称I(N)为S的部分解释。

7/8/201417完全语义树定义（完全语义树）,…｝是子句集S的原子集．S的一个语义树是完全的，当且仅当对于语义树中每一个尖端节点N（即从N不再生出节的那种节点），都有7/8/201418S的完全语义树的每一个分枝都对应着S的一个解释；S的任意解释都对应着S的完全语义树中的一条分枝？结论：子句集S的一棵完全语义树对应着S的所有解释。7/8/201419若不然，设T中节点N向下生出的n个节L1，…，Ln的每个Qn是恒真公式,其中Qi表示Li上所有文字的合取，Qn化为合取范式，于是Qn＝（A1A2引理设T是子句集S的完全语义树，I是S的一个解释。于是T中任意节点向下生出的直接节中，必有一节，其上所有文字都在I中。7/8/201420定义（失效点）称语义树T中的节点N为失效点，如果(1)I(N)弄假S中某个子句的某个基例；(2)I(N’)不弄假任意子句的任意基例，其中N’是N的任意祖先节点。定义（封闭语义树）语义树T是封闭的，当且仅当T的每—个分枝的终点都是失效点。定义（推理点）称封闭语义树的节点N为推理点，如果N的所有直接下降节点都是失效点．7/8/201421HerbrandHerbrand定理I．子句集S是不可满足的，当且仅当对应于S的每一个完全语义树都存在一个有限的封闭语义证明:必要性：若S是不可满足的，设T是S的完全语义树．对T的每一个分枝B,令I弄假S中某子句C的某个基例C’．由于C’是有限的，所以B上存在一个节点N）弄假C’，于是分枝B上有一个失效点．因此，对T中每一分枝都存在一个失效点，于是从T得到S的一个封闭语义树T’。

7/8/201422Herbrand定理I．子句集S是不可满足的，当且仅当对应于S的每一个完全语义树都存在一个有限的封闭语义树．(有限性)因为T’中每一个节点只能向下生长有限个节，故T’必有有限个节点．否则，由Konig无限性引理，T’中必有一条无穷的分枝,此无穷分枝上当然没有失效点,矛盾。充分性：若S的每一个完全语义树T都对应着一个有限封闭语义树T’，则T的每条分枝上都有一个失效点。因为S的任一解释都对应T的某一条分枝，所以每一个解释都弄假S，故S是不可满足的。7/8/201423Herbrand定理II子句集S是不可满足的，当且仅当存在S的一个有限不可满足的S的基例集S’。证明:必要性：若S恒假，设T是S的完全语义树，由Herbrand定理I知，有一个有限封闭语义树T’对应着T。T’中所有失效点弄假的所有基例（S中某些子句的基例）的集合。因为T’中失效点的个数有限，所以S’是有限集合。任取S’的一解释I’，则I’是S的某个解释I的子集，而解释I是T中一个分枝，又因S恒假，所以，I弄假S，即I弄假S中某子句的某个基例，亦即I弄假S’中子句C’，故I弄假S’。因为I’I,且I’是S’的解释,故I’弄假S’．由I’的任意性知S’不可满足。

7/8/201424Herbrand定理II子句集S是不可满足的，当且仅当存在S的一个有限不可满足的S的基例集S’。充分性：假设S有一个有限的不可满足的基例集S’。因为S的每一个解释I都包含着S’的一个解释I’，而S’是不可满足的，所以S的任一解释I都弄假S’，故I弄假S’中至少一个子句，即I弄假S中至少一个子句的基例，亦即I弄假S。由I的任意性，知S是不可满足的。7/8/201425使用Herbrand定理的机器证明过程