资源描述：
《人工智能-谓词逻辑43.ppt》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、谓词逻辑基础一阶逻辑基本概念个体词：表示主语的词谓词：刻画个体性质或个体之间关系的词量词：表示数量的词小王是个工程师。8是个自然数。我去买花。小丽和小华是朋友。其中，“小王”、“工程师”、“我”、“花”、“8”、“小丽”、“小华”都是个体词，而“是个工程师”、“是个自然数”、“去买”、“是朋友”都是谓词。显然前两个谓词表示的是事物的性质，第三个谓词“去买”表示的一个动作也表示了主、宾两个个体词的关系，最后一个谓词“是朋友”表示两个个体词之间的关系。谓词逻辑基础谓词逻辑基础例如：（1）所有的人都是要死的。（2）有的人活到一百岁
2、以上。在个体域D为人类集合时，可符号化为：（1）xP(x)，其中P(x)表示x是要死的。（2）xQ(x),其中Q(x)表示x活到一百岁以上。在个体域D是全总个体域时，引入特殊谓词R(x)表示x是人，可符号化为：（1）x（R(x)→P(x)）,其中，R(x)表示x是人；P(x)表示x是要死的。（2）x（R(x)∧Q(x)），其中，R(x)表示x是人；Q(x)表示x活到一百岁以上。一阶逻辑公式及其解释个体常量：a,b,c个体变量：x,y,z谓词符号：P,Q,R量词符号：,谓词逻辑基础量词否定等值式：～(x）P（x）
3、<=>（y）～P（y）～(x）P（x）<=>（y）～P（y）量词分配等值式：(x）(P（x）∧Q（x）)<=>(x）P（x）∧(x）Q（x）(x）(P（x）∨Q（x）)<=>(x）P（x）∨(x）Q（x）消去量词等值式：设个体域为有穷集合（a1,a2,…an）(x）P（x）<=>P（a1）∧P（a2）∧…∧P（an）(x）P（x）<=>P（a1）∨P（a2）∨…∨P（an）谓词逻辑基础量词辖域收缩与扩张等值式：(x）(P（x）∨Q)<=>(x）P（x）∨Q(x）(P（x）∧Q)<=>(x）P（x
4、）∧Q(x）(P（x）→Q)<=>(x）P（x）→Q(x）(Q→P（x）)<=>Q→(x）P（x）(x）(P（x）∨Q)<=>(x）P（x）∨Q(x）(P（x）∧Q)<=>(x）P（x）∧Q(x）(P（x）→Q)<=>(x）P（x）→Q(x）(Q→P（x）)<=>Q→(x）P（x）谓词逻辑基础谓词逻辑基础SKOLEM标准形前束范式定义：说公式A是一个前束范式，如果A中的一切量词都位于该公式的最左边（不含否定词），且这些量词的辖域都延伸到公式的末端。谓词逻辑归结原理即：把所有的量词都提到前面去，然后消掉
5、所有量词(Q1x1)(Q2x2)…(Qnxn)M(x1,x2,…,xn)约束变项换名规则：(Qx）M（x）<=>（Qy）M（y）(Qx）M（x,z）<=>（Qy）M（y,z）谓词逻辑归结原理量词消去原则：消去存在量词“”，略去全程量词“”。注意：左边有全程量词的存在量词，消去时该变量改写成为全程量词的函数；如没有，改写成为常量。谓词逻辑归结原理Skolem定理：谓词逻辑的任意公式都可以化为与之等价的前束范式，但其前束范式不唯一。SKOLEM标准形定义：消去量词后的谓词公
6、式。注意：谓词公式G的SKOLEM标准形同G并不等值。谓词逻辑归结原理例：将下式化为Skolem标准形：～(x)(y)P(a,x,y)→(x)(～(y)Q(y,b)→R(x))解：第一步，消去→号，得：～(～(x)(y)P(a,x,y))∨(x)(～～(y)Q(y,b)∨R(x))第二步，～深入到量词内部，得：(x)(y)P(a,x,y)∨(x)((y)Q(y,b)∨R(x))第三步，变元易名，得(x)(y)P(a,x,y)∨(u)(v)(Q(v,b)∨R(u))第四步，存在量词左移，直至所有
7、的量词移到前面，(x)(y)(u)(v)(P(a,x,y)∨(Q(v,b)∨R(u))由此得到前述范式第五步，消去“”（存在量词），略去“”全称量词消去(y)，因为它左边只有(x)，所以使用x的函数f(x)代替之，这样得到：(x)(u)(v)(P(a,x,f(x))∨Q(v,b)∨R(u))消去(u)，同理使用g(x)代替之，这样得到：(x)(v)(P(a,x,f(x))∨Q(v,b)∨R(g(x)))则，略去全称变量，原式的Skolem标准形为：P(a,x,f(x))∨Q(v,b)∨R(g(x)
8、)子句与子句集文字：不含任何连接词的谓词公式。子句：一些文字的析取（谓词的和）。子句集S的求取：G→SKOLEM标准形→消去存在变量→以“，”取代“∧”，并表示为集合形式。谓词逻辑归结原理G是不可满足的<=>S是不可满足的G与S不等价，但在不可满足得意义下是一致的。定理：若G是给定的公式，
