第5章-基于谓词逻辑的机器推理课件

第第5 5章章 基于谓词逻辑的机器推理基于谓词逻辑的机器推理7/12/20241目录目录5.0 5.0 机器推理概述机器推理概述5.1 5.1 一阶谓词逻辑一阶谓词逻辑5.2 5.2 归结演绎推理归结演绎推理5.3 5.3 应用归结原理求取问题答案应用归结原理求取问题答案5.4 5.4 归结策略归结策略5.5 5.5 归结反演程序举例归结反演程序举例*5.6 5.6 HornHorn子句归结与逻辑程序子句归结与逻辑程序5.7 5.7 非归结演绎推理非归结演绎推理7/12/202425.0 5.0 机器推理概述（机器推理概述（1 1）n机器推理：机器推理：就是计算机推理，也称自动推理。它是人工智能的核就是计算机推理，也称自动推理。它是人工智能的核心课题之一。推理是人脑的一个基本功能和重要功能。几心课题之一。推理是人脑的一个基本功能和重要功能。几乎所有的人工智能领域都与推理有关。因此，要实现人工乎所有的人工智能领域都与推理有关。因此，要实现人工智能，就必须将推理的功能赋予机器，实现机器推理。智能，就必须将推理的功能赋予机器，实现机器推理。n自动定理证明：自动定理证明：是机器推理的一种重要应用，它是利用计算机证明非是机器推理的一种重要应用，它是利用计算机证明非数值性的结果，很多非数值领域的任务如医疗诊断、信息数值性的结果，很多非数值领域的任务如医疗诊断、信息检索、规划制定和难题求解等方法都可以转化一个定理证检索、规划制定和难题求解等方法都可以转化一个定理证明问题明问题。7/12/20243n自动定理证明的基本方法：自动定理证明的基本方法：5.0 5.0 机器推理概述（机器推理概述（2 2）定理证明器定理证明器：它是研究一切可判定问题的证明方法。：它是研究一切可判定问题的证明方法。鲁滨逊的归结原理。鲁滨逊的归结原理。人机交互进行定理证明人机交互进行定理证明：计算机作为数学家的辅助工具，：计算机作为数学家的辅助工具，用计算机帮助人完成手工证明中的难以完成的烦杂的大用计算机帮助人完成手工证明中的难以完成的烦杂的大量计算推理和穷举。四色定理。量计算推理和穷举。四色定理。判定法判定法：该方法是对一类问题找出统一的计算机上可实：该方法是对一类问题找出统一的计算机上可实现的算法。数学家吴文俊教授现的算法。数学家吴文俊教授吴氏方法。吴氏方法。自然演绎法自然演绎法：该方法依据推理规则从前提和公理中可以：该方法依据推理规则从前提和公理中可以推出许多定理，如果待证明的定理在其中则定理得证。推出许多定理，如果待证明的定理在其中则定理得证。LTLT程序、证明平面几何的程序。程序、证明平面几何的程序。7/12/20244n基于归结原理的自动定理证明过程：基于归结原理的自动定理证明过程：5.0 5.0 机器推理概述（机器推理概述（3 3）定理的自然语言描述定理的自然语言描述定理的谓词公式描述定理的谓词公式描述子句集子句集生成子句集生成子句集定理得证定理得证应用归结规则归结策略应用归结规则归结策略自然语言处理生成谓词公式自然语言处理生成谓词公式已知前提：已知前提：F1F1：自然数都是大于零的整数。：自然数都是大于零的整数。F2F2：所有整数不是偶数就是奇数。：所有整数不是偶数就是奇数。F3F3：偶数除以：偶数除以2 2是整数。是整数。结论结论G G：所有自然数不是奇数就是一：所有自然数不是奇数就是一半为整数的数。半为整数的数。定理的谓词公式描述：定理的谓词公式描述：F1:F1:x(x(N(x)N(x)GZ(xGZ(x)I(xI(x)F2:F2:x(x(I(x)I(x)(E(x(E(x)O(xO(x)F3:F3:x(x(E(xE(x)I(s(xI(s(x)G:G:x(x(N(x)N(x)(I(s(x(I(s(x)O(xO(x)7/12/202455.15.1一阶谓词逻辑一阶谓词逻辑5.1.1 5.1.1 谓词、函数、量词谓词、函数、量词5.1.2 5.1.2 谓词公式谓词公式5.1.3 5.1.3 谓词逻辑中的形式演绎推理谓词逻辑中的形式演绎推理7/12/202465.1.15.1.1谓词、函数、量词（谓词、函数、量词（1 1）命题（命题（proposition）：）：是具有真假意义的语句。命题代表人是具有真假意义的语句。命题代表人们进行思维时的一种判断，或者是否定，或者是肯定。们进行思维时的一种判断，或者是否定，或者是肯定。命题可以用命题符号表示。命题可以用命题符号表示。用命题符号可以表示简单的逻辑关系和推理。用命题符号可以表示简单的逻辑关系和推理。P:P:今天天气好今天天气好 Q:Q:去旅游去旅游 S1S1：我有名字我有名字 S2S2：你有名字你有名字P PQ Q表示：如果今天天气好，就去旅游。表示：如果今天天气好，就去旅游。此时，如果此时，如果P P（今天天气好）今天天气好）成立，则可以得到结论成立，则可以得到结论Q Q（去旅游去旅游）7/12/202475.1.15.1.1谓词、函数、量词（谓词、函数、量词（2 2）n对于复杂的知识，命题符号能力不够。对于复杂的知识，命题符号能力不够。n无法把所描述的客观事物的结构及逻辑特征无法把所描述的客观事物的结构及逻辑特征反映出来。反映出来。n无法把不同事物间的共同特征表达出来。无法把不同事物间的共同特征表达出来。F：老李是小李的父亲。老李是小李的父亲。S1：我有名字我有名字 S2：你有名字你有名字所有的人都有名字：所有的人都有名字：SI S2 S3 7/12/202485.1.15.1.1谓词、函数、量词（谓词、函数、量词（3 3）谓词谓词(predicate)：一般形式为一般形式为P（x1,x2,xn）P为为谓词名，谓词名，用于刻画个体的性质、状态用于刻画个体的性质、状态 或个体间的关系。或个体间的关系。x1，x2，xn是是个体，个体，表示某个独立存表示某个独立存 在的事物或者某个抽象的概念。在的事物或者某个抽象的概念。S(x):x是学生；是学生；P(x,y):x是是y的父亲。的父亲。个体变元的变化范围称为个体变元的变化范围称为个体域个体域。包揽一切事物的集合称为包揽一切事物的集合称为全总个体域全总个体域。7/12/202495.1.15.1.1谓词、函数、量词（谓词、函数、量词（4 4）n函数：函数：为了表达个体之间的对应关系，引入数为了表达个体之间的对应关系，引入数学中函数概念和记法。用形如学中函数概念和记法。用形如f(xf(x1 1，x x2 2，x xn n)来表示个体变元对应的个体来表示个体变元对应的个体y y，并称之为并称之为n元元个体函数个体函数，简称函数。，简称函数。函数函数 father(x):值为值为x x的父亲。的父亲。谓词谓词D(D(father(Li):):表示表示x x的父亲是医生，值为真或假。的父亲是医生，值为真或假。符号约定：符号约定：谓词大写字母；谓词大写字母；P(x,y)P(x,y)函数小写字母；函数小写字母；f(x)f(x)变量变量 x x、y y、z z、u u、v v；常量常量a a、b b、c c.。P(a,yP(a,y)7/12/2024105.1.15.1.1谓词、函数、量词（谓词、函数、量词（5 5）表示表示“对个体域中所有的（或任一个）个体对个体域中所有的（或任一个）个体”。记为。记为 x x全称量词全称量词 表示表示“在个体域中存在个体在个体域中存在个体”。记为。记为 x x存在量词存在量词 如：如：“凡是人都有名字凡是人都有名字”用用M M（x x）表示表示“x x是人是人”，N N（x x）表示表示“x x有名字有名字”x x（M M（x x）N N（x x）如：如：“存在不是偶数的整数存在不是偶数的整数”用用G G（x x）表示）表示“x x是整数是整数”，E E（x x）表示）表示“x x是偶数是偶数”x x（G G（x x）E E（x x）7/12/2024115.1.15.1.1谓词、函数、量词（谓词、函数、量词（6 6）用谓词表示命题时，一般取全总个体域，再采用使用用谓词表示命题时，一般取全总个体域，再采用使用限定谓词的方法来指出每个个体变元的个体域。限定谓词的方法来指出每个个体变元的个体域。(2)(2)对存在量词，把限定词作为一个合取项加入。即对存在量词，把限定词作为一个合取项加入。即 x(P(x)x(P(x)例例5.25.2：对于所有的自然数，均有：对于所有的自然数，均有x+yx+yxx x x y y（N N（x x）N N（y y）S(x,y,x)S(x,y,x)）例例5.35.3：某些人对某些食物过敏：某些人对某些食物过敏 x x y(M(x)y(M(x)N(y)N(y)G G（x x，y y）(1)(1)对全称量词，把限定词作为蕴含式之前件加入。对全称量词，把限定词作为蕴含式之前件加入。即即 x x（P P（x x）例例5.25.2：对于所有的自然数，均有：对于所有的自然数，均有x+yx+yxx 也可以用函数也可以用函数h h（x x，y y）来表示）来表示x x与与y y的和的和 x x y y（N N（x x）N N（y y）G(G(h(x,yh(x,y),x),x)）7/12/2024125.1.15.1.1谓词、函数、量词（谓词、函数、量词（7 7）例例5.15.1：不存在最大的整数，我们可以把它表示为：不存在最大的整数，我们可以把它表示为：x(G(x)y（G（y）D（x，y）x(G(x)y（G（y）D（y，x）用谓词表示命题时，形式并不是固定的。用谓词表示命题时，形式并不是固定的。7/12/2024135.1.15.1.1谓词、函数、量词（谓词、函数、量词（8 8）练习：用谓词公式表示下述命题。练习：用谓词公式表示下述命题。已知前提：已知前提：（1）自然数自然数都是都是大于零大于零的的整数整数。（2）所有整数不是）所有整数不是偶数偶数就是就是奇数奇数。（3）偶数）偶数除以除以2是整数。是整数。结论：所有自然数不是奇数就是一半为整数的数。结论：所有自然数不是奇数就是一半为整数的数。首先定义如下谓词：首先定义如下谓词：N(x):x是自然数。是自然数。I(x):x是整数。是整数。E(x):x是偶数。是偶数。O(x):x是奇数。是奇数。GZ(x):x大于零。大于零。s(x):x除以除以2。7/12/2024145.1.15.1.1谓词、函数、量词（谓词、函数、量词（9 9）将上述各语句翻译成谓词公式：将上述各语句翻译成谓词公式：（1）自然数自然数都是都是大于零大于零的的整数整数。F1:F1:x(N(x)x(N(x)GZ(x)GZ(x)I(x)I(x)（2）所有整数不是所有整数不是偶数偶数就是就是奇数奇数。F2:F2:x(I(x)x(I(x)(E(x)(E(x)O(x)O(x)（3）偶数偶数除以除以2是整数。是整数。F3:F3:x(E(x)x(E(x)I(s(x)I(s(x)所有自然数不是奇数就是一半为整数的数。所有自然数不是奇数就是一半为整数的数。G:G:x(N(x)x(N(x)(I(s(x)(I(s(x)O(x)O(x)7/12/2024155.1.25.1.2谓词公式（谓词公式（1 1）定义定义1 1：项：项（1 1）个体常元和变元都是项。个体常元和变元都是项。（2 2）f f是是n n元函数符号，若元函数符号，若t t1 1，t t2 2，t tn n是项，则是项，则 f f（t t1 1，t t2 2，t tn n ）是项。是项。（3 3）只有有限次使用（）只有有限次使用（1 1），（），（2 2）得到的符号串才是项。）得到的符号串才是项。用谓词、量词及真值连结词可以表达相当复杂的命题，用谓词、量词及真值连结词可以表达相当复杂的命题，我们把命题的这种符号表达式称为我们把命题的这种符号表达式称为谓词公式谓词公式。7/12/2024165.1.25.1.2谓词公式（谓词公式（2 2）定义定义2 2：原子公式：原子公式 设设P P为为n n元谓词符号，元谓词符号，t t1 1，t t2 2，t tn n为项，为项，P P（t t1 1，t t2 2，t tn n）称为原子谓词公式，简称原子或原）称为原子谓词公式，简称原子或原子公式。子公式。7/12/2024175.1.25.1.2谓词公式（谓词公式（3 3）定义定义3 3：谓词公式：谓词公式（1 1）原子公式是谓词公式。）原子公式是谓词公式。（2 2）若）若A A、B B是谓词公式，则是谓词公式，则 A A，A A B B，A A B B，A A B B，A AB B，xAxA，xAxA也是谓词公式。也是谓词公式。（3 3）只有有限步应用（）只有有限步应用（1 1）（）（2 2）生成的公式才是谓词公式。）生成的公式才是谓词公式。谓词公式亦称为谓词逻辑中的合适（式）公式，记为谓词公式亦称为谓词逻辑中的合适（式）公式，记为WffWff。由项的定义，当由项的定义，当t t1 1，t t2 2，t tn n全为个体常元时，所得全为个体常元时，所得的原子谓词公式就是原子命题公式（命题符号）。所以的原子谓词公式就是原子命题公式（命题符号）。所以全体命题公式也是谓词公式。全体命题公式也是谓词公式。7/12/2024185.1.25.1.2谓词公式（谓词公式（4 4）n辖域辖域：紧接于量词之后被量词作用（即说明）：紧接于量词之后被量词作用（即说明）的谓词公式称为该量词的辖域。的谓词公式称为该量词的辖域。n指导变元指导变元：量词后的变元为指导变元。：量词后的变元为指导变元。n约束变元约束变元：在一个量词辖域中与该量词的指导：在一个量词辖域中与该量词的指导变元相同的变元称为约束变元。变元相同的变元称为约束变元。n自由变元自由变元：谓词公式中除了约束变元之外的变：谓词公式中除了约束变元之外的变元。元。（1）x P（x）（2）y（G（y）D（x，y）（3）x G(x)P（x）指导指导变元变元约束约束变元变元约束约束变元变元约束约束变元变元自由自由变元变元自由自由变元变元7/12/2024195.1.25.1.2谓词公式（谓词公式（5 5）n一个变元在一个公式中既可以约束出现，一个变元在一个公式中既可以约束出现，也可以自由出现，为了避免混淆，通过也可以自由出现，为了避免混淆，通过改名规则改名规则改名：改名：n对需要改名的变元，应对需要改名的变元，应同时更改同时更改该变元在量该变元在量词及其辖域中的词及其辖域中的所有出现所有出现。n新变元符号必须是量词辖域内新变元符号必须是量词辖域内原先没有原先没有的，的，最好是最好是公式中公式中也也未出现未出现过的。过的。x G(x)x G(x)P P（x x）x G(x)x G(x)P P（y y）7/12/2024205.1.25.1.2谓词公式（谓词公式（6 6）n谓词公式与命题的区别与联系谓词公式与命题的区别与联系n谓词公式是谓词公式是命题函数命题函数。n一个谓词公式中所有个体变元被量化，谓词一个谓词公式中所有个体变元被量化，谓词公式就变成了一个命题。公式就变成了一个命题。n从谓词公式得到命题的两种方法：给谓词中从谓词公式得到命题的两种方法：给谓词中的个体变元代入个体常元；把谓词中的个体的个体变元代入个体常元；把谓词中的个体变元全部量化。变元全部量化。例：例：P P（x x）表示表示“x x是素数是素数”x P（x），），x P（x），），P P（a a）都是命题都是命题7/12/2024215.1.25.1.2谓词公式（谓词公式（7 7）n一阶谓词一阶谓词：仅个体变元被量化的谓词。：仅个体变元被量化的谓词。n二阶谓词二阶谓词：个体变元被量化，函数符号和谓词：个体变元被量化，函数符号和谓词符号也被量化。符号也被量化。P x P（x）n全称命题：全称命题：x P(x)x P(x)等价于等价于P P(a(a1 1)P P(a(a2 2)P P(a(an n)n特称命题特称命题 x G(x)x G(x)等价于等价于P P(a(a1 1)P P(a(a2 2)P P(a(an n)7/12/2024225.1.25.1.2谓词公式（谓词公式（8 8）定义定义4 4：合取范式（：合取范式（Conjunctive Normal FormConjunctive Normal Form）设设A A为如下形式的谓词公式：为如下形式的谓词公式：B B1 1 B B2 2 B Bn n其中其中B Bi i（i=1,2,i=1,2,，n n）形如形如L L1 1 L L2 2 L Lm m，L Lj j（j=1j=1，2,2,，m m）为原子公式或其否定，则为原子公式或其否定，则A A称为合取范式。称为合取范式。例例 (P(x)Q(y)(P(x)Q(y)R(x,y)(Q(x)R(x,y)就是一个合取范式就是一个合取范式7/12/2024235.1.25.1.2谓词公式（谓词公式（9 9）定义定义5 5：析取范式：析取范式（Disjunctive Normal FormDisjunctive Normal Form）设设A A为如下形式的谓词公式：为如下形式的谓词公式：B B1 1 B B2 2 B Bn n其中其中B Bi i（i=1,2,i=1,2,，n n）形如形如L L1 1 L L2 2 L Lm m，L Lj j（j=1j=1，2,2,，m m）为原子公式或其否定，则为原子公式或其否定，则A A称为析取范式称为析取范式。例例 (P(x)P(x)Q(y)Q(y)R(x,y)R(x,y)(P(x)P(x)Q(y)Q(y)(P(x)P(x)R(x,yR(x,y)就是一个析取范式就是一个析取范式7/12/2024245.1.25.1.2谓词公式（谓词公式（1010）*谓词公式的解释谓词公式的解释 设设D D为谓词公式为谓词公式P P的个体域，若对的个体域，若对P P中的个体常量、函数中的个体常量、函数和谓词按如下规定赋值：和谓词按如下规定赋值：（1 1）为）为每个个体常量每个个体常量指派指派D D中的一个元素；中的一个元素；（2 2）为）为每个每个n n元函数元函数指派一个从指派一个从D Dn n到到D D的映射，其中的映射，其中 D Dn n(x(x1 1,x,x2 2,x,xn n)/x)/x1 1,x,x2 2,x,xn n DD （3 3）为为每个每个n n元谓词元谓词指派一个从指派一个从D Dn n到到F,TF,T的映射。的映射。则称这些指派为公式则称这些指派为公式P P在在D D上的一个解释。上的一个解释。7/12/2024255.1.25.1.2谓词公式（谓词公式（1111）*例：设个体域例：设个体域D D1,2,1,2,求公式求公式A A x x yPyP（x x，y y）在）在D D上的解释，并指出在每一种解释下公式上的解释，并指出在每一种解释下公式A A的真值。的真值。解：公式里没有个体常量和函数，所以直接为解：公式里没有个体常量和函数，所以直接为谓词指派谓词指派真值真值，设为，设为 P（1，1）T P（1，2）F P（2，1）T P（2，2）F 这就是这就是A A在在D D上的一个解释。上的一个解释。在此解释下：在此解释下：当当x x1 1时有时有y y1 1使使P P（x x，y y）的真值为的真值为T T；当当x x2 2时有时有y y1 1使使P P（x x，y y）的真值为的真值为T T；即对于即对于D D中的所有中的所有X X都有都有y y1 1使使P P（x x，y y）的真值为的真值为T T，所以在此解释下公式所以在此解释下公式A A的真值为的真值为T T。7/12/2024265.1.25.1.2谓词公式（谓词公式（1212）*例：设个体域例：设个体域D D1,2,1,2,求公式求公式A A x x P P（x x）Q Q（f(x),bf(x),b）在在D D上的解释，上的解释，并指出在每一种解释下公式并指出在每一种解释下公式A A的真值。的真值。解：解：为为个体常量个体常量b b指派指派D D中的值：中的值：b=1 b=1 为为函数函数f(x)f(x)指派指派D D中的值中的值 f(1)=2,f(2)=1f(1)=2,f(2)=1 对对谓词谓词指派真值为：指派真值为：P(1)=F,P(2)=T,Q(1,1)=T,Q(2,1)=FP(1)=F,P(2)=T,Q(1,1)=T,Q(2,1)=F 7/12/2024275.1.25.1.2谓词公式（谓词公式（1313）*在此解释下，在此解释下，当当x1时有：时有：P(1)=F,Q(f(1),1)=Q(2,1)=FP(1)=F,Q(f(1),1)=Q(2,1)=F 所以所以P P（x x）Q Q（f(x),bf(x),b）为）为T T。当当x2时有时有 P(2)=T,Q(f(2),1)=Q(1,1)=TP(2)=T,Q(f(2),1)=Q(1,1)=T 所以所以P P（x x）Q Q（f(x),bf(x),b）为）为T T。即对个体域即对个体域D D中的所有中的所有x x均有均有P P（x x）Q Q（f(x),bf(x),b），），所所以公式以公式B B在此解释下的真值为在此解释下的真值为T T。7/12/2024285.1.25.1.2谓词公式（谓词公式（1414）定义定义6 6：谓词公式在个体域上的永真、永假、可满足：谓词公式在个体域上的永真、永假、可满足设设P P为谓词公式，为谓词公式，D D为其个体域，对于为其个体域，对于D D中的任一解释中的任一解释I I：（1 1）若）若P P恒为真，则称恒为真，则称P P在在D D上永真或是上永真或是D D上的永真式。上的永真式。（2 2）若）若P P恒为假，则称恒为假，则称P P在在D D上永假或是上永假或是D D上的永假式。上的永假式。（3 3）若至少有一个解释，可是）若至少有一个解释，可是P P为真，则称为真，则称P P在在D D上是上是可满足式可满足式。7/12/2024295.1.25.1.2谓词公式（谓词公式（1515）定义定义7 7：谓词公式全个体域上的永真、永假、可满足：谓词公式全个体域上的永真、永假、可满足设设P P为谓词公式，对于任何个体域：为谓词公式，对于任何个体域：（1 1）若）若P P都永真，则称都永真，则称P P为永真式。为永真式。（2 2）若）若P P都永假，则称都永假，则称P P为永假式。为永假式。（3 3）若）若P P都可满足，则称都可满足，则称P P为可满足式。为可满足式。谓词公式的真值与个体域及真值有关，考虑到个体域的谓词公式的真值与个体域及真值有关，考虑到个体域的数目和个体域中元素数目无限的情形，所以要通过算法数目和个体域中元素数目无限的情形，所以要通过算法判断一个谓词公式永真是不可能的，所以称一阶谓词逻判断一个谓词公式永真是不可能的，所以称一阶谓词逻辑是不可判定的（但它是半可判定的）。辑是不可判定的（但它是半可判定的）。7/12/2024305.1.35.1.3谓词逻辑中的形式演绎推理（谓词逻辑中的形式演绎推理（1 1）n自然演绎推理自然演绎推理 利用一阶谓词推理规则的符号表示形式，可以把关利用一阶谓词推理规则的符号表示形式，可以把关于自然语言的逻辑推理问题，转化为符号表达式的推于自然语言的逻辑推理问题，转化为符号表达式的推演变换。这种推理十分类似于人们用自然语言推理的演变换。这种推理十分类似于人们用自然语言推理的思维过程，因而称为自然演绎推理。思维过程，因而称为自然演绎推理。n常用逻辑等价式常用逻辑等价式n常用逻辑蕴含式常用逻辑蕴含式 7/12/202431常用逻辑等价式（常用逻辑等价式（1 1）7/12/202432常用逻辑等价式（常用逻辑等价式（2 2）7/12/202433常用逻辑等价式（常用逻辑等价式（3 3）7/12/202434常用逻辑等价式（常用逻辑等价式（4 4）7/12/202435常用逻辑蕴含式（常用逻辑蕴含式（1)1)7/12/202436常用逻辑蕴含式常用逻辑蕴含式(2)(2)7/12/2024375.1.35.1.3谓词逻辑中的形式演绎推理（谓词逻辑中的形式演绎推理（2 2）例例5.4 5.4 设有前提：设有前提：（1 1）凡是大学生都学过计算机；）凡是大学生都学过计算机；（2 2）小王是大学生。）小王是大学生。试问：小王学过计算机吗？试问：小王学过计算机吗？解：令解：令S S（x x）：x x是大学生是大学生M M（x x）：x x学过计算机；学过计算机；a a：小王小王上面命题用谓词公式表示为：上面命题用谓词公式表示为：前提前提(1),US前提前提(2),(3),I3我们进行形式推理：我们进行形式推理：M(a)，即，即小王学过计算机。小王学过计算机。xA(x)=A(y)y是个体域中任一确定元素是个体域中任一确定元素(A B)A=B7/12/2024385.1.35.1.3谓词逻辑中的形式演绎推理（谓词逻辑中的形式演绎推理（3 3）例例5.5 证明证明 是是 和和 逻辑逻辑 结果。结果。证：证：前提前提(1),US(2),US前提前提(3),(4),I4(A B)B=A 拒取式拒取式7/12/2024395.1.35.1.3谓词逻辑中的形式演绎推理（谓词逻辑中的形式演绎推理（4 4）例例5.6 证明证明 证：证：前提前提(1),US(2),E24(3),(5),I6前提前提(4),US(6),UGAB=B A 逆反律逆反律(AB)(BC)=A B 假言三段论假言三段论A(y)=xA(x)全称推广规则全称推广规则7/12/2024405.25.2归结演绎推理归结演绎推理5.2.1 5.2.1 子句集子句集5.2.2 5.2.2 命题逻辑中的归结原理命题逻辑中的归结原理5.2.3 5.2.3 替换与合一替换与合一5.2.4 5.2.4 谓词逻辑中的归结原理谓词逻辑中的归结原理7/12/2024415.2.15.2.1子句集子句集(1)(1)定义定义1 1：原子谓词公式及其否定称为：原子谓词公式及其否定称为文字文字 若干个文字的一个析取式称为一个若干个文字的一个析取式称为一个子句子句 由由r r个文字组成的子句叫个文字组成的子句叫r-r-文字子句文字子句 1-1-文字子句叫文字子句叫单元子句单元子句 不含任何文字的子句称为不含任何文字的子句称为空子句空子句，记为，记为或或NILNIL。例如：例如：D(y)D(y)I(aI(a)P P Q Q R R I(z)I(z)R(z)R(z)7/12/2024425.2.15.2.1子句集子句集(2)(2)n谓词公式例谓词公式例 xx yP(x,yyP(x,y)yQ(x,y)yQ(x,y)R(x,yR(x,y)n子句集例子句集例 P(x,f(xP(x,f(x)Q(x,g(xQ(x,g(x),),P(y,f(yP(y,f(y)R(y,g(yR(y,g(y)谓词公式与子句集有哪些区别？谓词公式与子句集有哪些区别？“”作用原子谓词作用原子谓词没有量词没有量词(、)合取范式合取范式元素之间变元不同元素之间变元不同定义定义2 2：对一个谓词公式：对一个谓词公式G G，通过以下步骤所得的子句集通过以下步骤所得的子句集 S S，称为称为G G的的子句集（子句集（clausesclauses）。集合形式集合形式没有蕴含词、等值词没有蕴含词、等值词7/12/2024435.2.15.2.1子句子句集集(3)(3)例例5.7：x y P(x，y)yQ(x,y)R(x,y)由由第一步可得：第一步可得：x y P(x，y)y Q(x,y)R(x,y)1 1、消蕴含词和等值词消蕴含词和等值词理论根据理论根据：AB A B A B (A B)(B A)蕴含等价式蕴含等价式问题问题:蕴含式蕴含式 y y P(xP(x，y)y)yQ(x,y)yQ(x,y)R(x,yR(x,y)的前件是？的前件是？1 1：y y P(xP(x，y)y)2 2：P(xP(x，y)y)7/12/2024445.2.15.2.1子句集子句集(4)(4)n子句集的特征子句集的特征“”作用原子谓词作用原子谓词没有量词没有量词(、)合取范式合取范式元素之间变元不同元素之间变元不同集合形式集合形式没有蕴含词、等值词没有蕴含词、等值词7/12/2024455.2.15.2.1子句集子句集(5)(5)x x y P(x y P(x，y)y)yy Q(x,y)Q(x,y)R(x,y)R(x,y)2、移动否定词作用范围，使其仅作用于原子公式移动否定词作用范围，使其仅作用于原子公式理论根据：理论根据：(A)A (A B)A B (A B)A B xP(x)xP(x)xP(x)xP(x)双重否定律双重否定律摩根定律摩根定律量词转换定律量词转换定律=x x y y P(x P(x，y)y)y y Q(x,yQ(x,y)R(x,yR(x,y)=x x y y P(x P(x，y)y)y y(Q(x,yQ(x,y)R(x,y)R(x,y)=x x y y P(x P(x，y)y)y Q(x,y)y Q(x,y)R(x,y)R(x,y)7/12/2024465.2.15.2.1子句集子句集(6)(6)n子句集的特征子句集的特征“”作用原子谓词作用原子谓词没有量词没有量词(、)合取范式合取范式元素之间变元不同元素之间变元不同集合形式集合形式没有蕴含词、等值词没有蕴含词、等值词7/12/2024475.2.15.2.1子句子句集集(7)(7)=x x y y P(x P(x，y)y)z zQ(x,Q(x,z z)R(x,R(x,z z)3、适当改名，使变量标准化适当改名，使变量标准化即：对于不同的约束，对应于不同的变量即：对于不同的约束，对应于不同的变量 x x y y P(x P(x，y)y)y Q(x,y)y Q(x,y)R(x,y)R(x,y)问题问题:不同辖域的相同变元对应的约束相同吗不同辖域的相同变元对应的约束相同吗?7/12/2024485.2.15.2.1子句集子句集(8)(8)4 4、消去存在量词消去存在量词(SkolemSkolem化）化）,同时进行变元替换同时进行变元替换 原则：原则：若该存在量词若该存在量词不在任何不在任何全称量词全称量词的辖域内，的辖域内，则则用一用一 个个常量符号常量符号代替该存在量词辖域内的相应约束变元，代替该存在量词辖域内的相应约束变元，这个常量叫这个常量叫SkolemSkolem常量常量；若该存在量词若该存在量词在在全称量词全称量词的辖域内，的辖域内，则则用这些全用这些全 称量词指导变元的一个称量词指导变元的一个函数函数代替该存在量词辖域代替该存在量词辖域 内的相应约束变元，这样的函数称为内的相应约束变元，这样的函数称为SkolemSkolem函数函数。理论依据：理论依据：xA（x）=A（y）y y是个体域中某一确定的元素。是个体域中某一确定的元素。存在指定规则存在指定规则 7/12/2024495.2.15.2.1子句集子句集(9)(9)问题问题:为什么受全称量词约束的要用为什么受全称量词约束的要用SkolemSkolem函数替换函数替换?而不能用常量替换？而不能用常量替换？x x yMyM（y y，x x）：）：对任意一个人对任意一个人x x，都存在一个，都存在一个y y，y y是是x x的妈妈。的妈妈。若去掉存在量词用常量若去掉存在量词用常量a a代替代替y y，则变为：，则变为：x Mx M（a a，x x）：）：a a是所有人的妈妈。是所有人的妈妈。实际上，引入实际上，引入SkolemSkolem函数，是由于存在量词在全称量词函数，是由于存在量词在全称量词的辖域之内，其约束变元的取值完全依赖于全称变量的的辖域之内，其约束变元的取值完全依赖于全称变量的取值。而取值。而SkolemSkolem函数反映了这种依赖关系。函数反映了这种依赖关系。7/12/2024505.2.15.2.1子句集子句集(10)(10)x x y y P(x P(x，y)y)zQ(x,z)zQ(x,z)R(x,zR(x,z)=x P(x，f(x)Q(x，g(x)R(x，g(x)=P(x P(x，f(x)f(x)Q(x,g(x)Q(x,g(x)R(x,g(x)R(x,g(x)5、消去所有全称量词。消去所有全称量词。理论依据：理论依据：xA（x）=A（y）y y是个体域中任一确定的元素。是个体域中任一确定的元素。全称指定规则全称指定规则 7/12/2024515.2.15.2.1子句集子句集(11)(11)n子句集的特征子句集的特征“”作用原子谓词作用原子谓词没有量词没有量词(、)合取范式合取范式元素之间变元不同元素之间变元不同集合形式集合形式没有蕴含词、等值词没有蕴含词、等值词7/12/2024525.2.15.2.1子句集子句集(12)(12)=P(x，f(x)Q(x,g(x)P(x，f(x)R(x,g(x)6 6、化公式为合取范式、化公式为合取范式 理论依据：理论依据：A（B C）（A B）（A C）（A B）C （A C）（B C）P(x，f(x)Q(x,g(x)R(x,g(x)分配律分配律 7/12/2024535.2.15.2.1子句集子句集(13)(13)n子句集的特征子句集的特征“”作用原子谓词作用原子谓词没有量词没有量词(、)合取范式合取范式元素之间变元不同元素之间变元不同集合形式集合形式没有蕴含词、等值词没有蕴含词、等值词7/12/2024545.2.15.2.1子句集子句集(14)(14)=P(x，f(x)Q(x,g(x)P(y，f(y)R(y,g(y)7、适当改名，使子句间无同名变元适当改名，使子句间无同名变元=P(x，f(x)Q(x,g(x),P(y，f(y)R(y,g(y)8、消去合取词，以子句为元素组成一个集合消去合取词，以子句为元素组成一个集合S S=P(x P(x，f(x)f(x)Q(x,g(x)Q(x,g(x)R(x,g(x)R(x,g(x)7/12/2024555.2.15.2.1子句集子句集(15)(15)消去蕴含词和等值词消去蕴含词和等值词使否定词仅作用于原子公式使否定词仅作用于原子公式使量词间不含同名指导变元使量词间不含同名指导变元消去存在量词消去存在量词消去全称量词消去全称量词化公式为合取范式化公式为合取范式子句间无同名变元子句间无同名变元组成一个集合组成一个集合“”作用原子谓词作用原子谓词没有量词没有量词(、)合取范式合取范式元素之间变元不同元素之间变元不同集合形式集合形式没有蕴含词、等值词没有蕴含词、等值词蕴含等价式蕴含等价式双重否定律、双重否定律、摩根定律、摩根定律、量词转换律量词转换律存在指定、存在指定、依赖关系依赖关系全称指定全称指定分配律分配律7/12/2024565.2.15.2.1子句集子句集(16)(16)练习：用谓词公式表示下述命题。练习：用谓词公式表示下述命题。已知前提：已知前提：（1）自然数都是大于零的整数。）自然数都是大于零的整数。（2）所有整数不是偶数就是奇数。）所有整数不是偶数就是奇数。（3）偶数除以）偶数除以2是整数。是整数。结论：所有自然数不是奇数就是一半为整数的数。结论：所有自然数不是奇数就是一半为整数的数。化化F1 F1 F2 F2 F3 F3 G G的的子句集。子句集。F1:F1:x(N(x)x(N(x)GZ(x)GZ(x)I(x)I(x)F2:F2:x(I(x)x(I(x)(E(x)(E(x)O(x)O(x)F3:F3:x(E(x)x(E(x)I(s(x)I(s(x)G:G:x(N(x)x(N(x)(I(s(x)(I(s(x)O(x)O(x)7/12/2024575.2.15.2.1子句集子句集(17)(17)解：解：F1 F1 F2 F2 F3 F3 G G的子句集为的子句集为（1 1）N(x)N(x)GZ(x)GZ(x)（2 2）N(y)N(y)I(y)I(y)（3 3）I(z)I(z)E(z)E(z)O(z)O(z)（4 4）E(u)E(u)I(s(u)I(s(u)（5 5）N(a)N(a)（6 6）O(a)O(a)（7 7）I(s(a)I(s(a)7/12/2024585.2.15.2.1子句集子句集(18)(18)SkolemSkolem标准型标准型 在求子句集的过程中，消去存在量词在求子句集的过程中，消去存在量词之后，把所有之后，把所有全称量词全称量词都依次移到式子的最左边（或者都依次移到式子的最左边（或者把所有的量词都依次移到式子最左边，再消去存在量把所有的量词都依次移到式子最左边，再消去存在量词），再将右部的式子化为合取范式，这样得到的式词），再将右部的式子化为合取范式，这样得到的式子就是子就是SkolemSkolem标准型。标准型。x y P(x，y)zQ(x,z)R(x,z)=x P(x，f(x)Q(x,g(x)R(x,g(x)=x P(x，f(x)Q(x,g(x)P(x，f(x)R(x,g(x)P(x，f(x)Q(x,g(x),P(y，f(y)R(y,g(y)消去合取词和全称量词，就得到了原公式的子句集消去合取词和全称量词，就得到了原公式的子句集7/12/2024595.2.15.2.1子句集子句集(19)(19)例例5.8设设消去存在量词消去存在量词 用用a a代替代替x x 用用f f（y y，z z）代替代替u u 用用g g（y y，z z，v v）代替代替w w得到得到G G的的SkolemSkolem标准型标准型进而得进而得G G的子句集为：的子句集为：7/12/2024605.2.15.2.1子句集子句集(20)(20)引入引入SkolemSkolem函数，是由于存在量词在全称量词的辖函数，是由于存在量词在全称量词的辖域内，其约束变元的取值完全依赖于全称量词的取值。域内，其约束变元的取值完全依赖于全称量词的取值。SkolemSkolem反映了这种依赖关系。反映了这种依赖关系。但但SkolemSkolem标准型与原公式一般并不等价。标准型与原公式一般并不等价。有公式：有公式：G G xP(x)xP(x)它的它的SkolemSkolem标准型是标准型是 G G P(a)P(a)我们给出如下的解释我们给出如下的解释I I：D D0,1,a/0,P(0)/F,P(1)/T0,1,a/0,P(0)/F,P(1)/T 在此解释下，在此解释下，G GT,GT,G F F7/12/2024615.2.15.2.1子句集子句集(21)(21)定理定理1：谓词公式：谓词公式G不可满足当且仅当其子句集不可满足当且仅当其子句集S不可满不可满 足。足。定义定义3：子句：子句集集S是不可满足的，当且仅当其全部子句的是不可满足的，当且仅当其全部子句的 合取式是不可满足的。合取式是不可满足的。7/12/2024625.2.25.2.2命题逻辑中的归结原理命题逻辑中的归结原理(1)(1)n归结原理的提出归结原理的提出 归结原理归结原理(principle of resolution)(principle of resolution)又称消解原又称消解原理理,1965,1965年鲁滨逊（年鲁滨逊（J.A.RobinsonJ.A.Robinson）提出，从理论上提出，从理论上解决了定理证明问题。归结原理提出的是一种证明子解决了定理证明问题。归结原理提出的是一种证明子句集不可满足性，从而实现定理证明的一种理论及方句集不可满足性，从而实现定理证明的一种理论及方法。法。7/12/2024635.2.25.2.2命题逻辑中的归结原理命题逻辑中的归结原理(2)(2)定义定义4 4 设设L L为一个文字，则为一个文字，则L L与与L L为为互补文字互补文字。定义定义5 5 设设C C1 1，C C2 2是是命题逻辑中的两个子句，命题逻辑中的两个子句，C C1 1中有中有文字文字L L1 1 ，C C2 2中有文字中有文字L L2 2 ，且，且L L1 1与与L L2 2互补，互补，从从C C1 1、C C2 2中分别删除中分别删除L L1 1、L L2 2，再再将将剩余部分析取起来，剩余部分析取起来，构成的新子句为构成的新子句为C C1 21 2，则，则C C1 21 2为为C C1 1、C C2 2的的归结式归结式，C C1 1、C C2 2称为其归结式的称为其归结式的亲本子句亲本子句，称称L L1 1、L L2 2 为为消解基消解基。例例5.9 设设 ，则，则C1、C2的归结式为：的归结式为：7/12/2024645.2.25.2.2命题逻辑中的归结原理命题逻辑中的归结原理(3)(3)定理定理2 归结式是其亲本子句的逻辑结果。归结式是其亲本子句的逻辑结果。证明：设证明：设C C1 1=L=L C C1 1，C C2 2=L L C C2 2 其中其中C C1 1 、C C2 2 都是文字的析取式。都是文字的析取式。C C1 1 C C2 2的归结式为的归结式为C C1 1 C C2 2 C C1 1 C C2 2的逻辑结果为：的逻辑结果为：C C1 1=C=C1 1 L=L=C C1 1 L L C2=C2=L L C C2 2=L L C C2 2 由假言三段论可得：由假言三段论可得：C C1 1 C C2 2=（C C1 1 L L）（L LC C2 2）=C C1 1 C C2 2=C=C1 1 C C2 2命题逻辑中的归结原理：命题逻辑中的归结原理：7/12/2024655.2.25.2.2命题逻辑中的归结原理命题逻辑中的归结原理(4)(4)例例5.10 用归结原理验证分离规则和拒取式用归结原理验证分离规则和拒取式 A(AB)B (AB)B A 解解 A(AB)A(AB)B (AB)B (AB)(B)A 7/12/2024665.2.25.2.2命题逻辑中的归结原理命题逻辑中的归结原理(5)(5)n类似的可以验证其他推理规则。这说明，归结原理可类似的可以验证其他推理规则。这说明，归结原理可以代替其他所有的推理规则，而且推理步骤比较机械，以代替其他所有的推理规则，而且推理步骤比较机械，为机器推理提供了方便。为机器推理提供了方便。n由归结原理可知由归结原理可知 ：L L L L NILNIL 另外我们知道：另外我们知道：L L L L F F（假），假），也就是也就是 NIL FNIL F7/12/202467补充：补充：n定理定理1 G G为为F F1 1,F,F2 2,，F Fn n的逻辑结论，当且仅当的逻辑结论，当且仅当 （F F1 1 F F2 2 F Fn n）=G=Gn定理定理2 G G为为F F1 1,F,F2 2,，F Fn n的逻辑结论，当且仅当的逻辑结论，当且仅当 (F(F1 1 F F2 2 F Fn n)G G 是不可满足的。是不可满足的。7/12/2024685.2.25.2.2命题逻辑中的归结原理命题逻辑中的归结原理(6)(6)n利用归结原理证明命题公式的思路利用归结原理证明命题公式的思路n先求出要证明的命题公式的否定式的子句集先求出要证明的命题公式的否定式的子句集S S；n然后对子句集然后对子句集S S（一次或者多次）使用归结原理；一次或者多次）使用归结原理；n若在某一步推出了空子句，即推出了矛盾，则说明若在某一步推出了空子句，即推出了矛盾，则说明子句集子句集S S是不可满足的，从而原否定式也是不可满是不可满足的，从而原否定式也是不可满足的，进而说明原公式是永真的。足的，进而说明原公式是永真的。7/12/2024695.2.25.2.2命题逻辑中的归结原理命题逻辑中的归结原理(7)(7)n推出空子句就说明子句集不可满足，原因是：推出空子句就说明子句集不可满足，原因是：n空子句就是空子句就是F，推出空子句就是推出了推出空子句就是推出了F。n归结原理是正确的推理形式，由正确的推理形式推归结原理是正确的推理形式，由正确的推理形式推出了出了F，则说明前提不真，即归结出空子句的两个则说明前提不真，即归结出空子句的两个亲本子句至少有一个为假。亲本子句至少有一个为假。n而这两个亲本子句如果都是原子句集而这两个亲本子句如果都是原子句集S中的子句则中的子句则S不可满足。不可满足。n如果这两个亲本子句不是或不全是如果这两个亲本子句不是或不全是S中的子句，那中的子句，那么它们必定是某次归结的结果。么它们必定是某次归结的结果。n同样的道理向上回溯，一定会推出原子句集中至少同样的道理向上回溯，一定会推出原子句集中至少有一个子句为假，从而说明有一个子句为假，从而说明S不可满足。不可满足。7/12/2024705.2.25.2.2命题逻辑中的归结原理命题逻辑中的归结原理(8)(8)推论推论 设设C C1 1，C C2 2是是子句集子句集S S的两个子句，的两个子句，C C1 21 2是是 它们的归结式，则它们的归结式，则（1 1）若用）若用C C1 21 2来来代替代替C C1 1，C C2 2 ，得到新的子句集得到新的子句集S S1 1，则由则由S S1 1不可满不可满足性可以推出原子句集足性可以推出原子句集S S的不可满足性。即的不可满足性。即 （2 2）若用）若用C C1 21 2加入到加入到S S中，得到新的子句集中，得到新的子句集S S2 2 ，则，则S S2 2与原与原S S的同不的同不可满足。即可满足。即S1的不可满足性的不可满足性=S不可满足不可满足S2的不可满足性的不可满足性 S不可满足不可满足7/12/2024715.2.25.2.2命题逻辑中的归结原理命题逻辑中的归结原理(9)(9)例例5.12 设公理集：设公理集：P,(P Q)R,(S T)Q,T求证：求证：R 化子句集：化子句集：(P(P Q)Q)R R=(P(P Q)Q)R R=P P Q Q R R(S(S T)T)Q Q=(S(S T)T)Q Q=(=(S S T)T)Q Q=(=(S S Q)Q)(T T Q)Q)=S S Q,Q,T T QQ子句集：子句集：(1)P(1)P(2)P(2)P QQ R R(3)S(3)S Q Q(4)T(4)T Q Q(5)T(5)T(6)R(6)R（目标求反）目标求反）7/12/2024725.2.25.2.2命题逻辑中的归结原理命题逻辑中的归结原理(10)(10)子句集：子句集：(1)P(1)P(2)(2)P P Q Q R R(3)(3)S S Q Q(4)(4)T T Q Q(5)T(5)T(6)(6)R R（目标求反）目标求反）归结：归结：(7)(7)P P Q (2,6)Q (2,6)(8)(8)Q Q (1,7)(1,7)(9)(9)T (4,8)T (4,8)(10)NIL (5,9)(10)NIL (5,9)P Q RRP QPQT QTTNIL7/12/2024735.2.25.2.2命题逻辑中的归结原理命题逻辑中的归结原理(11)(11)例例5.11 5.11 证明子句集证明子句集 P P Q,Q,P,P,Q Q 是不可满足。是不可满足。7/12/2024745.2.35.2.3替换与合一替换与合一(1)(1)n问题问题 在一阶谓词中应用消解原理，无法直接找到互否文字在一阶谓词中应用消解原理，无法直接找到互否文字的子句对的子句对 例如：例如：P(P(x x)Q(zQ(z),P(P(f(y)f(y)R(yR(y)P(P(x x)Q(yQ(y),P(P(a a)R(zR(z)n解决方法解决方法 对个体变元做适当替换对个体变元做适当替换 例如：例如：P(P(f(y)f(y)Q(z)Q(z),P(f(y)P(f(y)R(y)R(y)P(P(a a)Q(yQ(y),P(a)P(a)R(zR(z)7/12/2024755.2.35.2.3替换与合一替换与合一(2)(2)定义定义6 6 一个一个替换（替换（SubstitutionSubstitution）是形如是形如 tt1 1/x/x1 1,t,t2 2/x/x2 2,t tn n/x/xn n 的有限集合，的有限集合，其中其中t t1 1,t,t2 2,t,tn n是是项项，称为，称为替换的分子替换的分子；x x1 1,x,x2 2,x,xn n是是互不相同的互不相同的个体变元个体变元，称为，称为替换的分母替换的分母；t ti i,x,xi i不同，不