离散件谓词逻辑.ppt

例如：(?x) (?y)[A(x) ? B(y)]是前束范式， 而(?x)A(x) ? (?y)B(y)则不是前束范式。 2。定义：如果前束范式的母式A是析取范式， 则称该前束范式为前束析取范式；如果母 式A是合取范式，则称该前束范式为前束 合取范式。 例如：(?x)(?y)[A(x) ? B(y)]是前束析取 范式， (?x)(?y)[A(x,y) ? (B(x) ? C(y))] 是前束合取范式。 3。定理：每个谓词合适公式都存在前束合 取范式和前束析取范式。 例：求公式 (?x)[A(x)?(?y)B(y)]?(?y)[?B(y)?C(y)] 的前束合取范式。 解： (?x)[A(x)?(?y)B(y)]?(?y)[?B(y)?C(y)] ? (?x)[(?A(x)?(?y)B(y)) ? (?B(x)?C(x))] ? (?x)(?y)[(?A(x)?B(y))?(?B(x)?C(x))] 由此很容易得到它的前束析取范式 (对母式利用分配律即可)。 五、Skolem范式 划去了存在量词的前束范式（改进）。例： (?x1) (? x2)(? x3)(? x4)[A(x1, x2) ?B(x1, x3, x4)] 划去?x1 , 将x1代以常元a: (? x2)(? x3)(? x4)[A(a, x2) ?B(a, x3, x4)] 划去?x4 ,将x4代以f(x2, x3): (? x2)(? x3)[A(a, x2) ?B(a, x3, f(x2, x3))] 定义 设谓词公式A的等价前束合取范式是（Q1x1）（Q2x2）…（Qnxn）G, １）从左到右扫描量词，设Qi是第一个遇到的存在量词, ①如i=1,则选择一个在G中未使用过的常量标识符代替G中的全部x1,然后删去Q1x1; ②如果i1,则Q１,Q2,…Qi-1都是全称量词,这时选择一个在G中未使用过的函数标识符(如g)，并用g(x1,x2,..,xi-1)去代替G中的全部xi,然后删去Qixi; 2）重复这一过程,直到公式中不含存在量词为止。 这样得到的公式称为Skolem范式,而取代存在量词时使用的常量标识符或函数,称为Skolem函数。 Skolem范式是一种重要的范式形式，机器定理证明和逻辑程序设计中的消解(或称归结)原理就建立在这种范式的基础上。 作业：习题2。3 1, 2 （吴子华） or 习题二 9, 10 （冯伟森） 第四节 谓词公式的蕴含 一、定义：设A(x)和B(x)是论域? 上的两个 WFF，如果对论域上的任何解释，A(x)取值 1 时，B(x)也取值 1， 就说A(x)在论域上蕴含B(x)。 如果论域是全总个体域，就说A(x)蕴含B(x)。 A(x)蕴含B(x)记为A(x) ? B(x)。 二、定理： A(x)? B(x)当且仅当A(x)?B(x) 是永真式。 证明要点：同命题公式蕴含情形相似， 对于任何论域，当A(x) ? B(x)时，在任 何解释下A(x)取值 1时, B(x) 必取值 1， 因而A(x)? B(x)恒取值 1 ，即为永真式。 反之也对。 三、基本蕴含式 在命题逻辑中导出的蕴含式依然有效。 (?x)A(x) ? (?x)B(x) ? (?x)[A(x) ? B(x)] 证明要点：当左端取值 1时，则A(x)或 B(x)对任何客体 x都取值 1，从而右端也取值 1。 (?x)[A(x) ? B(x)] ? (?x)A(x)? (?x) B(x) 证明要点：当左端取值 1时，则至少存在 一个客体 c 使A(c)和 B(c)都取值 1，从而 右端也取值 1。 (?x)(?y)A(x, y) ? ( ?y) (?x)A(x, y) (?y)(?x) A(x, y) ? (?x) (?y)A(x, y) (?x)(?y) A(x, y) ? (? x) (? y) A(x, y) 以上三式可以同样类似证明。 两个量词的等价式和蕴含式 ?x ?yP(x,y) ? ?y?xP(x,y) ?y?x ? ?x?y ?y?x ?x?y ?x?y ?y?x ? ? ?