湘潭大学人工智能课件确定性推理part6

ArtificialIntelligence(AI)

人工智能第二章：知识表示与推理ArtificialIntelligence(AI)

人内容提要第二章：知识表示与推理1.推理的基本概念2.搜索策略3.自然演绎推理4.消解演绎推理5.基于规则的演绎推理二、确定性推理内容提要第二章：知识表示与推理1.推理的基本概念2.搜索策略消解演绎推理消解演绎推理子句集及其化简鲁滨逊消解原理消解反演推理的消解策略用消解反演求取问题的答案消解演绎推理消解演绎推理鲁滨逊消解原理鲁滨逊消解原理包括命题逻辑的消解谓词逻辑的消解鲁滨逊消解原理鲁滨逊消解原理包括命题逻辑的消解命题逻辑的消解反演：在命题逻辑中，已知F，证明G为真的消解反演过程如下：①否定目标公式G，得﹁G;②把﹁G并入到公式集F中，得到{F，﹁G}；③把{F，﹁G}化为子句集S。④应用消解原理对子句集S中的子句进行消解，并把每次得到的消解式并入S中。如此反复进行，若出现空子句，则停止消解，此时就证明了G为真。命题逻辑的消解命题逻辑的消解反演：在命题逻辑中，已知F，证明鲁滨逊消解原理鲁滨逊消解原理包括命题逻辑的消解谓词逻辑的消解鲁滨逊消解原理鲁滨逊消解原理包括谓词逻辑的消解在谓词逻辑中，由于子句集中的谓词一般都含有变元，因此不能象命题逻辑那样直接消去互补文字。对于谓词逻辑，需要先用一个最一般合一对变元进行置换，然后才能进行消解。谓词逻辑的消解原理设C1和C2是两个没有公共变元的子句，L1和L2分别是C1和C2中的文字。如果σ是L1和﹁

L2存在最一般合一，则称：C12=({C1σ}-{L1σ})∪({C2σ}-{L2σ})

为C1和C2的二元消解式，L1和L2为消解式上的文字。谓词逻辑的消解在谓词逻辑中，由于子句集中的谓词一般都含有变元谓词逻辑的消解例：设C1=P(a)∨R(x)，C2=﹁P(y)∨Q(b)，求C12解：取L1=P(a),L2=﹁P(y)，则L1和﹁L2的最一般合一是σ={a/y}。因此：C12=({C1σ}-{L1σ})∪({C2σ}-{L2σ})=({P(a),R(x)}-{P(a)})∪({﹁P(a),Q(b)}-{﹁P(a)})=({R(x)})∪({Q(b)})={R(x),Q(b)}=R(x)∨Q(b)谓词逻辑的消解例：设C1=P(a)∨R(x)，C2=﹁P(y谓词逻辑的消解例：设C1=P(x)∨Q(a)，C2=﹁P(b)∨R(x)，求C12解：由于C1和C2有相同的变元x，不符合定义的要求。为了进行消解，需要修改C2中变元的名字。令C2=﹁P(b)∨R(y)，此时L1=P(x),L2=﹁P(b)，L1和﹁L2的最一般合一是σ={b/x}。则有:

C12=({C1σ}-{L1σ})∪({C2σ}-{L2σ})=({P(b),Q(a)}-{P(b)})∪({﹁P(b),R(y)}-{﹁P(b)})=({Q(a)})∪({R(y)})={Q(a),R(y)}=Q(a)∨R(y)谓词逻辑的消解例：设C1=P(x)∨Q(a)，C2=﹁P(b谓词逻辑的消解例：设C1=P(a)∨﹁Q(x)∨R(x)

C2=﹁P(y)∨Q(b)求C12对C1和C2通过最一般合一（σ={b/x,a/y}）的作用，可以得到两个互补对。注意：求消解式不能同时消去两个互补对，这样的结果不是二元消解式。如在σ={b/x,a/y}下，若同时消去两个互补对，所得的R(b)不是C1和C2的二元消解式。谓词逻辑的消解例：设C1=P(a)∨﹁Q(x)∨R(x)谓词逻辑的消解例：设C1=P(a)∨﹁Q(x)∨R(x)

C2=﹁P(y)∨Q(b)求C12解1：取L1=P(a),L2=﹁P(y)，则σ={a/y}是L1与﹁L2的最一般合一。此时：

C12=﹁Q(x)∨R(x)∨Q(b)解2：取L1=﹁Q(x)，L2=Q(b)，则σ={b/x}是L1与﹁L2的最一般合一。此时：

C12=P(a)∨R(b)∨﹁P(y)谓词逻辑的消解例：设C1=P(a)∨﹁Q(x)∨R(x)谓词逻辑的消解例：设

C1=P(x)∨P(f(a))∨Q(x)，C2=﹁P(y)∨R(b)求C12解：对参加消解的某个子句，若其内部有可合一的文字，则在进行消解之前应先对这些文字进行合一。本例的C1中有可合一的文字P(x)与P(f(a))，若用它们的最一般合一σ={f(a)/x}进行代换，可得到：C1σ=P(f(a))∨Q(f(a))此时对C1σ与C2进行消解。选L1=P(f(a)),L2=﹁P(y)，L1和L2的最一般合一是σ={f(a)/y}，则可得到C1和C2的二元消解式为：

C12=R(b)∨Q(f(a))谓词逻辑的消解例：设C1=P(x)∨P(f(a))∨Q(x谓词逻辑的消解例：设C1=P(y)∨P(f(x))∨Q(g(x))

C2=﹁P(f(g(a)))∨Q(b)求C12解：对C1

，取最一般合一σ={f(x)/y}，得C1的因子

C1σ=P(f(x))∨Q(g(x))

对C1的因子和C2消解（σ={g(a)/x}），可得：

C12=Q(g(g(a)))∨Q(b)谓词逻辑的消解例：设C1=P(y)∨P(f(x))∨Q(g谓词逻辑的消解我们把C1σ称为C1的因子。一般来说，若子句C中有两个或两个以上的文字具有最一般合一σ，则称Cσ为子句C的因子。如果Cσ是一个单文字，则称它为C的单元因子。应用因子概念，可对谓词逻辑中的消解原理给出如下定义：若C1和C2是无公共变元的子句，则子句C1和C2的消解式是下列二元消解式之一：①C1和C2的二元消解式;②C1的因子C1σ1和C2的二元消解式；③C1和C2的因子C2σ2的二元消解式；④C1的因子C1σ1和C2的因子C2σ的二元消解式。谓词逻辑的消解我们把C1σ称为C1的因子。一般来说，若子句C命题逻辑的消解反演：在命题逻辑中，已知F，证明G为真的消解反演过程如下：①否定目标公式G，得﹁G;②把﹁G并入到公式集F中，得到{F，﹁G}；③把{F，﹁G}化为子句集S。④应用消解原理对子句集S中的子句进行消解，并把每次得到的消解式并入S中。如此反复进行，若出现空子句，则停止消解，此时就证明了G为真。谓词逻辑的消解命题逻辑的消解反演：在命题逻辑中，已知F，证明G为真的消解反谓词逻辑的消解谓词逻辑的消解反演谓词逻辑的消解反演过程与命题逻辑的消解反演过程相比，其步骤基本相同，但每步的处理对象不同。在步骤(3)化简子句集时，谓词逻辑需要把由谓词构成的公式集化为子句集。在步骤(4)按消解原理进行消解时，谓词逻辑的消解原理需要考虑两个亲本子句的最一般合一。谓词逻辑的消解谓词逻辑的消解反演谓词逻辑的消解例：已知F:(∀x)((∃y)(A(x,y)∧B(y))→(∃y)(C(y)∧D(x,y)))G:﹁(∃x)C(x)→(∀x)(∀y)(A(x,y)→﹁B(y))求证G是F的逻辑结论。证明：先把G否定，并放入F中，得到的{F,﹁G}：{(∀x)((∃y)(A(x,y)∧B(y))→(∃y)(C(y)∧D(x,y))),

﹁(﹁(∃x)C(x)→(∀x)(∀y)(A(x,y)→﹁B(y)))}再把{F,﹁G}化成子句集，得到谓词逻辑的消解例：已知谓词逻辑的消解

(1)﹁A(x,y)∨﹁B(y)∨C(f(x))(2)﹁A(u,v)∨﹁B(v)∨D(u,f(u))(3)﹁C(z)(4)A(m,n)(5)B(k)最后应用谓词逻辑的消解原理对上述子句集进行消解，其过程为：(6)﹁A(x,y)∨﹁B(y)

(7)﹁B(n)(8)NILF﹁G(1)和(3)消解，取σ={f(x)/z}(4)和(6)消解，取σ={m/x,n/y}(5)和(7)消解，取σ={n/k}谓词逻辑的消解(1)﹁A(x,y)∨﹁B(y)∨C(谓词逻辑的消解因此，G是F的逻辑结论。上述消解过程可用如下消解树来表示﹁A(x,y)∨﹁B(y)∨C(f(x))﹁C(z)﹁A(x,y)∨﹁B(y)A(m,n)﹁B(n)B(k)NIL{f(x)/z}{m/x,n/y}{n/k}谓词逻辑的消解因此，G是F的逻辑结论。﹁A(x,y)∨﹁谓词逻辑的消解例：“快乐学生”问题假设：任何通过计算机考试并获奖的人都是快乐的，任何肯学习或幸运的人都可以通过所有考试，张不肯学习但他是幸运的，任何幸运的人都能获奖。求证：张是快乐的。解：先定义谓词：Pass(x,y)：x可以通过y考试

Win(x,prize)：x能获得奖励

Study(x)：x肯学习

Happy(x)：x是快乐的

Lucky(x)：x是幸运的谓词逻辑的消解例：“快乐学生”问题谓词逻辑的消解再将问题用谓词表示如下：“任何通过计算机考试并奖的人都是快乐的”(∀x)(Pass(x,computer)∧Win(x,prize)→Happy(x))“任何肯学习或幸运的人都可以通过所有考试”

(∀x)(∀y)(Study(x)∨Lucky(x)→Pass(x,y))“张不肯学习但他是幸运的”

﹁Study(zhang)∧Lucky(zhang)“任何幸运的人都能获奖”

(∀x)(Lucky(x)→Win(x,prize))结论“张是快乐的”的否定

﹁Happy(zhang)谓词逻辑的消解再将问题用谓词表示如下：谓词逻辑的消解将上述谓词公式转化为子句集如下：(1)﹁Pass(x,computer)∨﹁Win(x,prize)∨Happy(x)(2)﹁Study(y)∨Pass(y,z)(3)﹁Lucky(u)∨Pass(u,v)(4)﹁Study(zhang)(5)Lucky(zhang)(6)﹁Lucky(w)∨Win(w,prize)(7)﹁Happy(zhang)(结论的否定)按消解原理进行消解，消解树如下：谓词逻辑的消解将上述谓词公式转化为子句集如下：谓词逻辑的消解﹁Pass(x,computer)∨﹁Win(x,prize)∨Happy(x)﹁Lucky(w)∨Win(w,prize)﹁Pass(w,Computer)∨Happy(w)∨﹁Lucky(w)﹁Happy(zhang)Lucky(zhang)﹁Pass(zhang,Computer)∨﹁Lucky(zhang)﹁Pass(zhang,Computer)﹁Lucky(u)∨Pass(u,v)﹁Lucky(zhang)Lucky(zhang)

NIL{w/x}{zhang/w}{zhang/u,computer/v}谓词逻辑的消解﹁Pass(x,computer)∨﹁Win消解演绎推理消解演绎推理子句集及其化简鲁滨逊消解原理消解反演推理的消解策略用消解反演求取问题的答案消解演绎推理消解演绎推理消解反演推理的消解策略在消解演绎推理中，由于事先并不知道哪些子句对可进行消解，更不知道通过对哪些子句对的消解能尽快得到空子句，因此就需要对子句集中的所有子句逐对进行比较，直到得出空子句为止。这种盲目的全面进行消解的方法，不仅会产生许多无用的消解式，更严重的是会产生组核爆炸问题。因此，需要研究有效的消解策略来解决这些问题。常用的消解策略可分为两大类：限制策略：通过限制参加消解的子句减少盲目性删除策略：通过删除某些无用的子句缩小消解范围消解反演推理的消解策略在消解演绎推理中，由于事先并不知道哪些消解演绎推理消解演绎推理子句集及其化简鲁滨逊消解原理消解反演推理的消解策略用消解反演求取问题的答案消解演绎推理消解演绎推理用消解反演求取问题的答案消解原理出了可用于定理证明外，还可用来求取问题答案，其思想与定理证明相似。其一般步骤为：(1)把问题的已知条件用谓词公式表示出来，并化为子句集；(2)把问题的目标的否定用谓词公式表示出来，并化为子句集；(3)对目标否定子句集中的每个子句，构造该子句的重言式（即把该目标否定子句和此目标否定子句的否定之间再进行析取所得到的子句），用这些重言式代替相应的目标否定子句式，并把这些重言式加入到前提子句集中，得到一个新的子句集；(4)对这个新的子句集，应用消解原理求出其证明树，这时证明树的根子句不为空，称这个证明树为修改的证明树；(5)用修改证明树的根子句作为回答语句，则答案就在此根子句中。用消解反演求取问题的答案消解原理出了可用于定理证明外，还可用用消解反演求取问题的答案例1：已知：“张和李是同班同学，如果x和y是同班同学，则x的教室也是y的教室，现在张在302教室上课。”问：“现在李在哪个教室上课？”解：首先定义谓词C(x,y)：x和y是同班同学At(x,u)：x在u教室上课。把已知前提用谓词公式表示如下：C(zhang,li)(∀x)(∀y)(∀u)(C(x,y)∧At(x,u)→At(y,u))At(zhang,302)用消解反演求取问题的答案例1：用消解反演求取问题的答案把目标的否定用谓词公式表示如下：

﹁(∃v)At(li,v)把上述公式化为子句集：

把目标的否定化成子句式，并用下面的重言式代替：

﹁At(li,v)∨At(li,v)把此重言式加入前提子句集中，得到一个新的子句集，对这个新的子句集，应用消解原理求出其证明树。C(zhang,li)﹁C(x,y)∨﹁At(x,u)∨At(y,u)At(zhang,302)用消解反演求取问题的答案把目标用消解反演求取问题的答案求解过程如下图所示。该证明树的根子句就是所求的答案，即“李明在302教室”。﹁At(li,v)∨At(li,v)﹁C(x,y)∨﹁At(x,u)∨At(y,u)At(li,v)∨﹁

C(x,li)∨﹁At(x,v)C(zhang,li)﹁At(zhang,v)∨At(li,v)At(zhang,302)At(li,302){li/y,v/u}{Zhang/x}{302/v}用消解反演求取问题的答案求解过程如下图所示。该证明树的根子句用消解反演求取问题的答案例2：已知：A,B,C三人中有人从不说真话，也有人从不说假话。某人向这三人分别提出同一个问题：谁是说谎者？A答：“B和C都是说谎者”；B答：“A和C都是说谎者”；C答：“A和B中至少有一个是说谎者”。问：求谁是老实人，谁是说谎者？解：首先定义谓词T(x)：表示x说真话用消解反演求取问题的答案例2：用消解反演求取问题的答案把已知前提用谓词公式表示如下：有人从不说真话：¬T(C)∨¬T(A)∨¬T(B)有人从不说假话：T(C)∨T(A)∨T(B)根据“A答：B和C都是说谎者”，则若A说真话：T(A)→¬T(B)∧¬T(C)

若A说假话：

¬T(A)→T(B)∨T(C)同理：根据“B答：A和C都是说谎者”，则T(B)→¬T(A)∧¬T(C)¬T(B)→T(A)∨T(C)

根据“C答：A和B中至少有一个是说谎者”，则T(C)→¬T(A)∨¬T(B)¬T(C)→T(A)∧T(B)用消解反演求取问题的答案把已知前提用谓词公式表示如下：用消解反演求取问题的答案把上述公式化成子句集，得到前提子句集S：¬T(A)∨¬T(B)¬T(A)∨¬T(C)T(C)∨T(A)∨T(B)¬T(B)∨¬T(C)¬T(C)∨¬T(A)∨¬T(B)T(A)∨T(C)T(B)∨T(C)先求谁是老实人，结论的否定为：¬(∃x)T(x)用消解反演求取问题的答案把上述公式化成子句集，得到前提子句集用消解反演求取问题的答案把目标的否定化成子句式，并用下面的重言式代替：

¬T(x)∨T(x)把此重言式加入前提子句集S，得到一个新子句集，对这个新的子句集，应用消解原理求出其证明树。¬T(A)∨¬T(B)T(B)∨T(C)¬T(A)∨T(C)T(A)∨T(C)T(C)¬T(x)∨T(x)T(C){C/x}C是老实人用消解反演求取问题的答案把目标的否定化成子句式，并用下面的重用消解反演求取问题的答案下面证明A不是老实人，结论的否定为：¬T(A)将结论的否定¬

(¬T(A))加入并入前提子句集S中，应用消解原理对新的子句集进行消解：¬T(A)∨¬T(B)T(B)∨T(C)¬T(A)∨T(C)¬T(A)∨¬T(C)¬T(A)T(A)NIL得证。A不是是老实人同理可证B不是老实人用消解反演求取问题的答案下面证明A不是老实人，结论的否定为：消解演绎推理消解演绎推理的优点：简单，便于在计算机上实现。消解演绎推理的不足：必须把逻辑公式化成子句集。不便于阅读与理解：¬P(x)∨Q(x)没有P(x)→Q(x)直观。可能丢失控制信息，如下列逻辑公式：(¬A∧¬B)→C ¬A→(B∨C)(¬A∧¬C)→B ¬B→(A∨C)(¬C∧¬B)→A ¬C→(B∨A)化成子句后都是:A∨B∨C消解演绎推理消解演绎推理的优点：问题？问题？ArtificialIntelligence(AI)

人工智能第二章：知识表示与推理ArtificialIntelligence(AI)

人内容提要第二章：知识表示与推理1.推理的基本概念2.搜索策略3.自然演绎推理4.消解演绎推理5.基于规则的演绎推理二、确定性推理内容提要第二章：知识表示与推理1.推理的基本概念2.搜索策略消解演绎推理消解演绎推理子句集及其化简鲁滨逊消解原理消解反演推理的消解策略用消解反演求取问题的答案消解演绎推理消解演绎推理鲁滨逊消解原理鲁滨逊消解原理包括命题逻辑的消解谓词逻辑的消解鲁滨逊消解原理鲁滨逊消解原理包括命题逻辑的消解命题逻辑的消解反演：在命题逻辑中，已知F，证明G为真的消解反演过程如下：①否定目标公式G，得﹁G;②把﹁G并入到公式集F中，得到{F，﹁G}；③把{F，﹁G}化为子句集S。④应用消解原理对子句集S中的子句进行消解，并把每次得到的消解式并入S中。如此反复进行，若出现空子句，则停止消解，此时就证明了G为真。命题逻辑的消解命题逻辑的消解反演：在命题逻辑中，已知F，证明鲁滨逊消解原理鲁滨逊消解原理包括命题逻辑的消解谓词逻辑的消解鲁滨逊消解原理鲁滨逊消解原理包括谓词逻辑的消解在谓词逻辑中，由于子句集中的谓词一般都含有变元，因此不能象命题逻辑那样直接消去互补文字。对于谓词逻辑，需要先用一个最一般合一对变元进行置换，然后才能进行消解。谓词逻辑的消解原理设C1和C2是两个没有公共变元的子句，L1和L2分别是C1和C2中的文字。如果σ是L1和﹁

L2存在最一般合一，则称：C12=({C1σ}-{L1σ})∪({C2σ}-{L2σ})

为C1和C2的二元消解式，L1和L2为消解式上的文字。谓词逻辑的消解在谓词逻辑中，由于子句集中的谓词一般都含有变元谓词逻辑的消解例：设C1=P(a)∨R(x)，C2=﹁P(y)∨Q(b)，求C12解：取L1=P(a),L2=﹁P(y)，则L1和﹁L2的最一般合一是σ={a/y}。因此：C12=({C1σ}-{L1σ})∪({C2σ}-{L2σ})=({P(a),R(x)}-{P(a)})∪({﹁P(a),Q(b)}-{﹁P(a)})=({R(x)})∪({Q(b)})={R(x),Q(b)}=R(x)∨Q(b)谓词逻辑的消解例：设C1=P(a)∨R(x)，C2=﹁P(y谓词逻辑的消解例：设C1=P(x)∨Q(a)，C2=﹁P(b)∨R(x)，求C12解：由于C1和C2有相同的变元x，不符合定义的要求。为了进行消解，需要修改C2中变元的名字。令C2=﹁P(b)∨R(y)，此时L1=P(x),L2=﹁P(b)，L1和﹁L2的最一般合一是σ={b/x}。则有:

C12=({C1σ}-{L1σ})∪({C2σ}-{L2σ})=({P(b),Q(a)}-{P(b)})∪({﹁P(b),R(y)}-{﹁P(b)})=({Q(a)})∪({R(y)})={Q(a),R(y)}=Q(a)∨R(y)谓词逻辑的消解例：设C1=P(x)∨Q(a)，C2=﹁P(b谓词逻辑的消解例：设C1=P(a)∨﹁Q(x)∨R(x)

C2=﹁P(y)∨Q(b)求C12对C1和C2通过最一般合一（σ={b/x,a/y}）的作用，可以得到两个互补对。注意：求消解式不能同时消去两个互补对，这样的结果不是二元消解式。如在σ={b/x,a/y}下，若同时消去两个互补对，所得的R(b)不是C1和C2的二元消解式。谓词逻辑的消解例：设C1=P(a)∨﹁Q(x)∨R(x)谓词逻辑的消解例：设C1=P(a)∨﹁Q(x)∨R(x)

C2=﹁P(y)∨Q(b)求C12解1：取L1=P(a),L2=﹁P(y)，则σ={a/y}是L1与﹁L2的最一般合一。此时：

C12=﹁Q(x)∨R(x)∨Q(b)解2：取L1=﹁Q(x)，L2=Q(b)，则σ={b/x}是L1与﹁L2的最一般合一。此时：

C12=P(a)∨R(b)∨﹁P(y)谓词逻辑的消解例：设C1=P(a)∨﹁Q(x)∨R(x)谓词逻辑的消解例：设

C1=P(x)∨P(f(a))∨Q(x)，C2=﹁P(y)∨R(b)求C12解：对参加消解的某个子句，若其内部有可合一的文字，则在进行消解之前应先对这些文字进行合一。本例的C1中有可合一的文字P(x)与P(f(a))，若用它们的最一般合一σ={f(a)/x}进行代换，可得到：C1σ=P(f(a))∨Q(f(a))此时对C1σ与C2进行消解。选L1=P(f(a)),L2=﹁P(y)，L1和L2的最一般合一是σ={f(a)/y}，则可得到C1和C2的二元消解式为：

C12=R(b)∨Q(f(a))谓词逻辑的消解例：设C1=P(x)∨P(f(a))∨Q(x谓词逻辑的消解例：设C1=P(y)∨P(f(x))∨Q(g(x))

C2=﹁P(f(g(a)))∨Q(b)求C12解：对C1

，取最一般合一σ={f(x)/y}，得C1的因子

C1σ=P(f(x))∨Q(g(x))

对C1的因子和C2消解（σ={g(a)/x}），可得：

C12=Q(g(g(a)))∨Q(b)谓词逻辑的消解例：设C1=P(y)∨P(f(x))∨Q(g谓词逻辑的消解我们把C1σ称为C1的因子。一般来说，若子句C中有两个或两个以上的文字具有最一般合一σ，则称Cσ为子句C的因子。如果Cσ是一个单文字，则称它为C的单元因子。应用因子概念，可对谓词逻辑中的消解原理给出如下定义：若C1和C2是无公共变元的子句，则子句C1和C2的消解式是下列二元消解式之一：①C1和C2的二元消解式;②C1的因子C1σ1和C2的二元消解式；③C1和C2的因子C2σ2的二元消解式；④C1的因子C1σ1和C2的因子C2σ的二元消解式。谓词逻辑的消解我们把C1σ称为C1的因子。一般来说，若子句C命题逻辑的消解反演：在命题逻辑中，已知F，证明G为真的消解反演过程如下：①否定目标公式G，得﹁G;②把﹁G并入到公式集F中，得到{F，﹁G}；③把{F，﹁G}化为子句集S。④应用消解原理对子句集S中的子句进行消解，并把每次得到的消解式并入S中。如此反复进行，若出现空子句，则停止消解，此时就证明了G为真。谓词逻辑的消解命题逻辑的消解反演：在命题逻辑中，已知F，证明G为真的消解反谓词逻辑的消解谓词逻辑的消解反演谓词逻辑的消解反演过程与命题逻辑的消解反演过程相比，其步骤基本相同，但每步的处理对象不同。在步骤(3)化简子句集时，谓词逻辑需要把由谓词构成的公式集化为子句集。在步骤(4)按消解原理进行消解时，谓词逻辑的消解原理需要考虑两个亲本子句的最一般合一。谓词逻辑的消解谓词逻辑的消解反演谓词逻辑的消解例：已知F:(∀x)((∃y)(A(x,y)∧B(y))→(∃y)(C(y)∧D(x,y)))G:﹁(∃x)C(x)→(∀x)(∀y)(A(x,y)→﹁B(y))求证G是F的逻辑结论。证明：先把G否定，并放入F中，得到的{F,﹁G}：{(∀x)((∃y)(A(x,y)∧B(y))→(∃y)(C(y)∧D(x,y))),

﹁(﹁(∃x)C(x)→(∀x)(∀y)(A(x,y)→﹁B(y)))}再把{F,﹁G}化成子句集，得到谓词逻辑的消解例：已知谓词逻辑的消解

(1)﹁A(x,y)∨﹁B(y)∨C(f(x))(2)﹁A(u,v)∨﹁B(v)∨D(u,f(u))(3)﹁C(z)(4)A(m,n)(5)B(k)最后应用谓词逻辑的消解原理对上述子句集进行消解，其过程为：(6)﹁A(x,y)∨﹁B(y)

(7)﹁B(n)(8)NILF﹁G(1)和(3)消解，取σ={f(x)/z}(4)和(6)消解，取σ={m/x,n/y}(5)和(7)消解，取σ={n/k}谓词逻辑的消解(1)﹁A(x,y)∨﹁B(y)∨C(谓词逻辑的消解因此，G是F的逻辑结论。上述消解过程可用如下消解树来表示﹁A(x,y)∨﹁B(y)∨C(f(x))﹁C(z)﹁A(x,y)∨﹁B(y)A(m,n)﹁B(n)B(k)NIL{f(x)/z}{m/x,n/y}{n/k}谓词逻辑的消解因此，G是F的逻辑结论。﹁A(x,y)∨﹁谓词逻辑的消解例：“快乐学生”问题假设：任何通过计算机考试并获奖的人都是快乐的，任何肯学习或幸运的人都可以通过所有考试，张不肯学习但他是幸运的，任何幸运的人都能获奖。求证：张是快乐的。解：先定义谓词：Pass(x,y)：x可以通过y考试

Win(x,prize)：x能获得奖励

Study(x)：x肯学习

Happy(x)：x是快乐的

Lucky(x)：x是幸运的谓词逻辑的消解例：“快乐学生”问题谓词逻辑的消解再将问题用谓词表示如下：“任何通过计算机考试并奖的人都是快乐的”(∀x)(Pass(x,computer)∧Win(x,prize)→Happy(x))“任何肯学习或幸运的人都可以通过所有考试”

(∀x)(∀y)(Study(x)∨Lucky(x)→Pass(x,y))“张不肯学习但他是幸运的”

﹁Study(zhang)∧Lucky(zhang)“任何幸运的人都能获奖”

(∀x)(Lucky(x)→Win(x,prize))结论“张是快乐的”的否定

﹁Happy(zhang)谓词逻辑的消解再将问题用谓词表示如下：谓词逻辑的消解将上述谓词公式转化为子句集如下：(1)﹁Pass(x,computer)∨﹁Win(x,prize)∨Happy(x)(2)﹁Study(y)∨Pass(y,z)(3)﹁Lucky(u)∨Pass(u,v)(4)﹁Study(zhang)(5)Lucky(zhang)(6)﹁Lucky(w)∨Win(w,prize)(7)﹁Happy(zhang)(结论的否定)按消解原理进行消解，消解树如下：谓词逻辑的消解将上述谓词公式转化为子句集如下：谓词逻辑的消解﹁Pass(x,computer)∨﹁Win(x,prize)∨Happy(x)﹁Lucky(w)∨Win(w,prize)﹁Pass(w,Computer)∨Happy(w)∨﹁Lucky(w)﹁Happy(zhang)Lucky(zhang)﹁Pass(zhang,Computer)∨﹁Lucky(zhang)﹁Pass(zhang,Computer)﹁Lucky(u)∨Pass(u,v)﹁Lucky(zhang)Lucky(zhang)

NIL{w/x}{zhang/w}{zhang/u,computer/v}谓词逻辑的消解﹁Pass(x,computer)∨﹁Win消解演绎推理消解演绎推理子句集及其化简鲁滨逊消解原理消解反演推理的消解策略用消解反演求取问题的答案消解演绎推理消解演绎推理消解反演推理的消解策略在消解演绎推理中，由于事先并不知道哪些子句对可进行消解，更不知道通过对哪些子句对的消解能尽快得到空子句，因此就需要对子句集中的所有子句逐对进行比较，直到得出空子句为止。这种盲目的全面进行消解的方法，不仅会产生许多无用的消解式，更严重的是会产生组核爆炸问题。因此，需要研究有效的消解策略来解决这些问题。常用的消解策略可分为两大类：限制策略：通过限制参加消解的子句减少盲目性删除策略：通过删除某些无用的子句缩小消解范围消解反演推理的消解策略在消解演绎推理中，由于事先并不知道哪些消解演绎推理消解演绎推理子句集及其化简鲁滨逊消解原理消解反演推理的消解策略用消解反演求取问题的答案消解演绎推理消解演绎推理用消解反演求取问题的答案消解原理出了可用于定理证明外，还可用来求取问题答案，其思想与定理证明相似。其一般步骤为：(1)把问题的已知条件用谓词公式表示出来，并化为子句集；(2)把问题的目标的否定用谓词公式表示出来，并化为子句集；(3)对目标否定子句集中的每个子句，构造该子句的重言式（即把该目标否定子句和此目标否定子句的否定之间再进行析取所得到的子句），用这些重言式代替相应的目标否定子句式，并把这些重言式加入到前提子句集中，得到一个新的子句集；(4)对这个新的子句集，应用消解原理求出其证明树，这时证明树的根子句不为空，称这个证明树为修改的证明树；(5)用修改证明树的根子句作为回答语句，则答案就在此根子句中。用消解反演求取问题的答案消解原理出了可用于定理证明外，还可用用消解反演求取问题的答案例1：已知：“张和李是同班同学，如果x和y是同班同学，则x的教室也是y的教室，现在张在302教室上课。”问：“现在李在哪个教室上课？”解：首先定义谓词C(x,y)：x和y是同班同学At(x,u)：x在u教室上课。把已知前提用谓词公式表示如下：C(zhang,li)(∀x)(∀y)(∀u)(C(x,y)∧At(x,u)→At(y,u))At(zhang,302)用消解反演求取问题的答案例1：用消解反演求取问题的答案把目标的否定用谓词公式表示如下：

﹁(∃v)At(li,v)把上述公式化为子句集：

把目标的否定化成子句式，并用下面的重言式代替：

﹁At(li,v)∨At(li,v)把此重言式加入前提子句集中，得到一个新的子句集，对这个新的子句集，应用消解原理求出其证明树。C(zhang,li)﹁C(x,y)∨﹁At(x,u)∨At(y,u)At(zhang,302)用消解反演求取问题的答案把目标用消解反演求取问题的答案