归结原理、归结演绎推理

主要内容

• 归结演绎推理
• 范式
• 子句与子句集
• 将谓词公式转化为子句集
• 命题逻辑鲁宾逊归结原理

归结演绎推理

• 定理证明的实质是对前提P和结论Q证明P →Q的永真性
• 应用反证法，欲证明P →Q，只要证明 P∧~Q 等价于 F
• 鲁宾逊归结原理对机械化推理有重大突破
• 鲁宾逊归结原理是以子句为背景开展研究的

范式

什么是范式：“范式” 是一个用于表示、简化或标准化特定类型数据或表达式的术语。它通常用于不同领域，如布尔代数、关系数据库、逻辑表达式等。范式的目标通常是将复杂的数据或表达式变成更简单、更易于处理的形式。

合取范式

合取（Conjunction）是逻辑中的一种基本操作，它表示在多个条件都为真时，整个条件为真。合取通常用符号 “∧” 表示。
例如，如果有两个条件 A 和 B，A ∧ B 表示只有当 A 和 B 都为真时，整个条件才为真。

设  A=B1 ∧ B2 ∧ … ∧ Bn

其中，Bi =L1 ∨ L2 ∨… ∨ Lmi ,而Lj为原子公式或其否定。则称A为合取范式。

如：P(x) ∧ (P(x)∨Q(y)∨～ R(x,y))
任何命题公式，最终都能够化成 $(A_1\vee A_2)\wedge (A_3\vee A_4)$的形式，被称为 “ 合取范式”。

析取范式

设 A=B1 ∨ B2 ∨ … ∨ Bn
其中，Bi =L1 ∧ L2 ∧ … ∧Lmi , 而Lj为原子公式或其否定。则称A为析取范式。
如：P(x)∨(P(x)∧Q(y)∧～R(x,y))

谓词演算中的两种范式

• 谓词公式：数学或逻辑表达式，用于描述各种属性、关系和条件，以便在形式化逻辑和数学中进行推理和分析。谓词公式通常包含变量、谓词和逻辑运算符。
  • 变量：变量代表一个范围内的值，它们允许我们在公式中引入未知的对象或条件。通常使用字母，如 x、y、z 等来表示变量。
  • 谓词：谓词是描述性质、关系或条件的符号或符号组合。谓词可以是单一的，也可以包含参数。
    • 参数是用于与特定对象或变量相关联的项。例如，P(x) 可以表示一个关于 x 的属性或条件。
  • 常量：常量是不变的值，它们可以代表特定的对象、数字或元素。例如，数字 1 或特定的对象名可以是常量。
  • 逻辑运算符：逻辑运算符用于组合、连接或否定不同的谓词和条件，以构建更复杂的公式。常见的逻辑运算符包括合取 (∧)，析取 (∨)，否定 (¬)，蕴含 (→)，双蕴含 (↔) 等。
  • 量词：量词用于引入变量的范围，以明确说明公式的含义。常见的量词包括全称量词 (∀，表示 “对于所有”）和存在量词 (∃，表示 “存在一个”）。

前束形范式

一个谓词公式的所有量词均非否定地出现在公式的最前面,且它的辖域一直延伸到公式之末,同时公式中不出现连接词→及 ↔ 。
例:($\forall$x)($\exists$y)($\forall$z)(P(x)∧F(y, z)∧Q(y,z))

斯克林范式(Skolem标准式)

在前束范式的首标中不出现存在量词，即从前束范式中消去全部存在量词所得的公式。
其一般形式为：
(∀x1)(∀x2)…(∀x3)M(x1, x2 ,….x3)
其中M(x1, x2 ,….x3)是一个合取范式，称为Skolem标准型的母式

子句

• 文字
  • 原子谓词公式及其否定称为文字。
• 子句
  • 任何文字的析取式称为子句，由子句构成的集合称为子句集。
• 空子句
  • 不包含任何文字的子句称为空子句，由于它不能被任何解释满足，所以空子句是永假的。

将谓词公式转化为子句集

• 在谓词逻辑中，任何一个谓词公式都可通过等价关系和推理规则化为子句集。
• 例、求公式的子句：
  A= (∀x) ((∀ y)P(x,y) → ~(∀)(Q(x,y)→R(x,y)) )

化句集的九个步骤

1、利用连接词化归律消去谓词公式中的条件和双条件连接词。

连接词化归律：P →Q 等价于 ~P ∨Q
由
A= (∀x) ((∀y)P(x,y)→~(∀y)(Q(x,y)→R(x,y)) )
化为
A= (∀x)(_{(∀y)P(x,y)∨}(∀y)(~Q(x,y)∨R(x,y)))

2、利用等价关系把“~”移到紧靠谓词的位置上。

₍P) = P 双重否定律
~(P ∧ Q) = ~P ∨ ~Q 摩根定律
~(P ∨ Q) = ~P ∧ ~Q
~ (∀x)P = ($\exists$x)(~P) 量词转换律
~ ($\exists$x)P = (∀x)(~P)

3、重新命名，使不同量词的约束变元名字不同

4、消去存在量词

存在量词未出现在全称量词的辖域内时，用一个个体常量替换其所有约束变元。
否则，用skolem函数替换其所有其约束变元。

5、把全称量词移到公式最左边

6、利用等价关系（如：分配律）

7、去掉全称量词

8、对变元更名，使不同子句的变元不同名 。

9、消去合取词，即得子句集

鲁宾逊归结原理

• 由谓词公式转化为子句集的过程可以看出，在子句集中子句之间是合取关系，其中只要一个子句不可满足，则子句集不可满足
• 因此若一个子句集中包含空子句，则这个子句集一定不可满足

其基本思想：
检查子句集S中是否包含空子句，若包含，则S不可满足，不包含，就在子句集中选择合适的子句进行归结，归结出空子句，则S不可满足

命题逻辑鲁宾逊归结原理

• 互补文字
  • 若P是原子谓词公式，则称P和～P为互补文字。
• 归结式
  • 设C1与C2是子句集中的任意两个子句，且C1中的文字L1与C2中的文字L2互补，令：C12={C1-L1} ∨ {C2-L2}
  • 则称C12为C1与C2的归结式，C1、C2 为C12的亲本子句。