人工智能 搜索推理技术消解原理

人工智能ArtificialIntelligence(AI)第3章搜索推理技术3.1图的搜索策略3.2盲目搜索3.3启发式搜索3.4与或树搜索（补充）3.5博弈树搜索（补充）3.6消解原理3.6消解原理3.6.1子句集的求取3.6.2消解原理（补充）3.6.3消解推理规则3.6.4含有变量的消解式3.6.5消解反演求解过程3.6.6Horn子句集消解（补充）3.6.7Prolog语言简介（补充）3.6消解原理第2章中介绍：谓词逻辑的基本知识合一算法（求最一般的一致置换或合一者mgu）本节：消解原理（或者归结原理）3.6.1子句集的求取如何将谓词公式转化为子句集，作为合一算法的输入（公式集）3.6.1.1若干基本概念3.6.1.2子句集的求取3.6.1.1若干基本概念1自由变元与约束变元2前束范式与前束合取范式3斯科伦（Skolem）范式4子句集设α，β是一个谓词公式，将量词记作θ（即或）1自由变元与约束变元如果α中包含部分公式(θx)β，则β中变元x的一切出现都称为x在α中的约束出现，相应地称x为约束变元（哑元、虚构变量、约束变量）约束变元α中不在任何量词作用域内的变元x，称为变元x在α中的自由出现，相应地称x为自由变元（自由变量）自由变元：量词的作用域（辖域）是直接跟在它后面的公式如果有括号，则是括号里的公式如果没有括号，则是最短的完整公式说明：例1：x(P(x)y(R(x,y)))x,y都是约束变元例2：x(P(x)(R(x,y)))x是约束变量，y是自由变元改名：将谓词公式中一个变元名改成另一个变元名，但是要求改名后的公式与原公式意义相同（真假值相同）原则：改成的新的变元名一定是量词作用域中没有出现过的变元名（包括约束变元和自由变元）约束变元的改名或变量的标准化例3：x(P(x)(R(x,y)))除了y外，可以将x改成任何变元名例4：xP(x)∧Q(y)可以改成任何变元名，包括y（建议不要用）2前束范式与前束合取范式定义：设谓词公式α具有形式：α＝(θ1x1)…(θnxn)M其中：θi(i=1,…,n)是或M是不包含量词的谓词公式则，称α是前束范式称(θ1x1)…(θnxn)为前束称M为母式定义：设谓词公式α是一个前束范式，如果α的母式具有形式：（M11∨M12…∨M1n1）∧（M21∨M22…∨M2n2）∧……(Mm1∨Mm2…∨Mmnm）其中，Mij是原子公式或其非，则称α是前束合取范式。相应地有前束析取范式前束范式：(x)(y)(z)((～P(x)∧～Q(y))∨R(z))前束合取范式（交换律、分配律）(x)(y)(z)((R(z)∨～P(x))∧(R(z)∨～Q(y)))例：3斯柯伦范式定义：前束中不含存在量词的前束范式称为斯柯伦范式①若xk(1≤k≤n)左边没有全称量词，则取不在母式中出现的常量替代母式中的所有xk，并删除前束中的xk消去存在量词的规则或前束范式化成斯柯伦的步骤是：②若xk(1k≤n)左边有全称量词(xs1)(xs2)…(xsr)(1≤r，1≤s1s2…srk)则，取不在母式中出现的r阶函数fr(xs1,xs2,…xsr)替代母式中的所有xk，并删除前束中的xk③反复使用上述两条规则，消除前束中的所有存在量词，即得到斯柯伦范式其中，引入的函数称为斯柯伦函数xyzuvwA(x,y,z,u,v,w)(用a替代x，删除x)=yzuvwA(a,y,z,u,v,w)（用f(y,z)代替u，删除u）=yzvwA(a,y,z,f(y,z),v,w)（用h(y,z,v)代替w，删除w）=yzvA(a,y,z,f(y,z),v,h(y,z,v))例：求斯柯伦范式说明：一个谓词公式的斯科伦范式不是唯一的，尽可能将斯科伦函数取得简单一点化成前束范式化成前束合取范式化成斯科伦范式（斯科伦函数的变元较多）对于谓词公式：α=α1∧α2正常的做法：将α1、α2分别化成前束范式对α1、α2分别求出斯柯伦范式β1、β2将β1∧β2的量词左移得到α的斯柯伦范式（即前束范式）简化的做法：好处：简化斯科伦函数α=α1∧α2α=y1x1P(x1,y1)∧x2y2Q(x2,y2)=y1x1x2y2(P(x1,y1)∧Q(x2,y2))（前束合取范式）=x1x2(P(x1,a1)∧Q(x2,f(x1,x2)))例：正常化法α=y1x1P(x1,y1)∧x2y2Q(x2,y2)=x1P(x1,a1)∧x2Q(x2,f(x2))（先分别化成斯科伦范式）=x1x2(P(x1,a1)∧Q(x2,f(x2)))(前束合取范式）简化化法4子句集①原子命题是原子公式②如果t1,…,tn(n≥1)是项，P是谓词，则P(t1,…,tn)是原子公式③其它表达式都不是原子公式原子公式的定义：①文字（或基本式）：“原子公式”或者“原子公式的非”②子句：一个或多个基本式的析取子句的定义：一个谓词公式α具有形式：α＝(x1)…(xn)(c1∧c2∧…∧cm)其中，ci(i=1,…,m)为子句x1,…,xn是子句中出现的约束变元则，称谓词公式α具有子句形式子句形式的定义：闭公式：不含自由变量的谓词公式谓词公式的子句形式是闭公式母式为子句的合取范式前束中只有全称量词，无存在量词说明：若谓词公式α具有子句形式，记S=(c1,c2,…,cm)则，称S为谓词公式的子句集α＝(x1)…(xn)(c1∧c2∧…∧cm)子句集的定义：为了便于消解推理，要通过改名使得一个变量符号不出现在一个以上的子句中，即每一个子句具有不同的变量说明：子句形式：(x)(y)(z)((R(z)∨～P(x))∧(R(z)∨～Q(y)))子句集：{R(z)∨～P(x),R(z)∨～Q(y)}{R(z1)∨～P(x1),R(z2)∨～Q(y1)}（改名）例：3.6.1.2子句集的求取子句集的求取（将谓词公式化成子句集）有两种方法，其形式上会有差别，但是其逻辑意义是相同1、将谓词合适公式转化为前束合取范式①消去“蕴含”和“等价”连结词②将“～”连结词直接作用到原子公式前③约束变元改名，使所有的约束变元名都不相同④将量词移到谓词公式的左边，得到前束范式⑤将前束范式化成前束合取范式方法1（离散数学、数理逻辑采用的方法）：2、将前束范式转化为斯柯伦（Skolem）范式⑥得到斯科伦范式3、将斯柯伦范式转化为子句集⑦消去前束（全称量词）⑧消去合取连词⑨变量改名，得到子句集为了使斯科伦函数更简单一些，可以将合取关系的各个谓词公式分别先分成前束范式、斯科伦范式，再综合起来化成前束范式、前束合取范式（后面的定理证明部分就采用了这一种化法）说明：①消去“蕴含”和“等价”连结词②减少“非”连结词的辖域（将“～”连结词直接作用到原子公式前）③对变量标准化（约束变元改名）方法2（教材采用的方法）：④消去存在量词（引入斯科伦函数）⑤化成前束范式⑥将母式化成合取范式⑦消去全称量词⑧消去合取连结词⑨更改变量名，得到子句集两者的差别：在于④⑤⑥三步方法1是先得到前束合取范式，再化成斯科伦范式方法2是先引入斯科伦函数消去存在量词，再化成前束合取范式三步的结果：得到不含存在量词的前束合取范式谓词公式=全称量词串+合取范式的母式注：母式中的斯科伦函数变元个数可能不相同求取子句集的步骤：使用的公式：AB=～A∨BAB=(AB)∧(BA)①消去“蕴含”和“等价”连结词将“～”连结词直接作用到原子公式前，使得每一个“非”联结词最多只能作用于一个原子公式（谓词符号）②减少“非”连结词的辖域～(～A)＝A～(A∨B)=～A∧～B～(A∧B)=～A∨～B～(x)A(x)=(x)(～A(x))～(x)A(x)=(x)(～A(x))使用的公式是：说明：到现在为止，谓词公式只包含三种连结词“合取”：∧“析取”∨“非”~对约束变元改名，使得所有的约束变元名都不相同，保证每一个量词都有自己唯一的约束变元③对变量标准化以一个斯科伦函数代替每一个带存在量词的约束变元，斯科伦函数的变元是（左边）带全称量词的约束变元，而且这些全称量词的辖域必须包括被消去的存在量词的辖域④消去存在量词消去存在量词的规则：如果要消去的存在量词不在任何一个全称量词的辖域内，则用常量来代替斯科伦函数和常量的符号必须是未在谓词公式出现过的符号α=y1x1P(x1,y1)∧x2y2Q(x2,y2)=x1P(x1,a1)∧x2Q(x2,f(x2))（引入斯科伦函数，消去存在量词，x1的辖域不包含y2的辖域）例：将全称量词移到谓词公式的左边，使得每一个量词的辖域包括该量词后面的整个谓词公式⑤化成前束范式(θx)A(x)∨R=(θx)(A(x)∨R)(θx)A(x)∧R=(θx)(A(x)∧R)(θ1x)A(x)∨(θ2z)B(z)=(θ1x)(θ2z)(A(x)∨B(z))(θ1x)A(x)∧(θ2z)B(z)=(θ1x)(θ2z)(A(x)∧B(z))说明：A(x),B(z),R中允许含有与x，z不同的自由变量使用的规则：前束范式＝（前束）（母式）全称量词串无量词公式⑥将母式化成合取范式利用分配律将前束范式化成前束合取范式：P∨(Q∧R)=(P∨Q)∧(P∨R)（析取合取）谓词公式已经化成了前束合取范式，且只包含全称量词，此时全称量词的次序也不重要了，所以可以消去全部量词（即前束、前缀）⑦消去全称量词⑧消去合取连结词∧母式为合取范式：A1∧A2∧…∧An消去合取连结词∧，得到子句集：{A1,A2,…,An}子句：基本式（文字）的析取（只含∨）更改变元名，使得一个变量符号不出现在一个以上的子句中，即不同的子句包含不同的约束变元名⑨更换变元名(x)A(x)(x)B(x)=～(x)A(x)∨(x)B(x)（消去“蕴含”）=(x)(～A(x))∨(x)B(x)（“非”直接作用谓词符号）=(x)(～A(x))∨(z)B(z)(改名)=～A(a)∨B(b)（消去存在量词）子句集={～A(a)∨B(b)}注：两种方法的结果相同例1：仔细分析量词的辖域(x)(y)((z)(A(x,z)∧A(y,z))(u)B(x,y,u))=(x)(y)(～((z)(A(x,z)∧A(y,z)))∨(u)B(x,y,u))=(x)(y)((z)(～A(x,z)∨～A(y,z))∨(u)B(x,y,u))=(x)(y)((z)(～A(x,z)∨～A(y,z))∨B(x,y,f(x,y))=(x)(y)(z)(～A(x,z)∨～A(y,z)∨B(x,y,f(x,y)))使用方法1，函数将为f(x,y,z)子句例2：((x)P(x)∨(y)Q(y))(x)R(x)=～((x)P(x)∨(y)Q(y))∨(x)R(x)=(～(x)P(x)∧～(y)Q(y))∨(x)R(x)=((x)(～P(x))∧(y)(～Q(y)))∨(x)R(x)=((x)(～P(x))∧(y)(～Q(y)))∨(z)R(z)(改名)例3：＝((～P(a))∧(y)(～Q(y)))∨(z)R(z)（消去存在量词）＝(y)(z)((～P(a)∧～Q(y))∨R(z))（化成前束范式）＝(y)(z)((～P(a)∨R(z))∧(～Q(y)∨R(z)))(化成前束合取范式)子句集={～P(a)∨R(z),～Q(y)∨R(x)}两者化法结果相同=((x)(～P(x))∧(y)(～Q(y)))∨(z)R(z)例4：将谓词公式化成子句集①消去“蕴含”符号②“非”直接作用到谓词符号③约束变量改名后面的y改成w④引入斯科伦函数消去存在量词斯科伦函数w=g(x)⑤化成前束范式⑥化成前束合取范式分配律：P∨(Q∧R)=(P∨Q)∧(P∨R)注：使用分配律两次⑦消去全称量词或者前束⑧消去合取符号，得到子句⑨变量改名，使得变量不相同，得到子句集如果使用方