第五章 归结反演推理

• 反证推理方法就是证明﹁A恒为假来证明A恒为真，也叫消解法，归结反演推理
• 合取范式、前束范式、Skolem(斯科伦)标准型（消去存在量词）、子句集（合取范式，合取变逗号）
• 消去存在量词的步骤
• 公式A化为子句集的步骤（9步）
  • 例：美国人卖武器给敌对国家是犯罪的
  • 例：热爱所有动物的每个人会被某个人所爱
• 归结反演推理方法原理
  • 归结过程举例图
• H论域和H基
  • 例：𝑆1 = {𝑃(𝑎), ¬𝑃(𝑎), 𝑃(𝑓(𝑥))}, 𝑆2 = {𝑃(𝑥), 𝑄(𝑓(𝑎)), ¬𝑅(𝑔(𝑏))}

• Herbrand解释、语义树表示、规范语义树、完备语义树

  • 例：给出子句集𝑆 = {𝑃(𝑥), 𝑄(𝑥), 𝑅(𝑥)} 的H解释对应的语义树

• 基例、否节点、封闭语义树

  • 例：试给出子句集𝑆 = {¬𝑃(𝑥), 𝑄(𝑥), 𝑃(𝑓(𝑥)), ¬𝑄(𝑓(𝑥))}的封闭语义树

• 求二元消解式

  • 例：
• 常见的消解策略，删除策略、禁止策略、支持集消解
  • 例：
• 动态支持集策略：线性消解、输入消解、单元消解
  • 输入消解和单元消解对于Horn子句集都是完备的
  • 例：试分别采用线性消解、输入消解、单元消解3种策略对子句集进行消解否证

• 例：“快乐的小张”问题

  • 设有以下句子：任何通过计算机考试并获奖的人都是快乐的， 任何肯学习或幸运的人都可以通过所有考试；小张不肯学习但 他是幸运的，任何幸运的人都能获奖。求证：小张是快乐的