主要内容
- 归结演绎推理
- 范式
- 子句与子句集
- 将谓词公式转化为子句集
- 命题逻辑鲁宾逊归结原理
归结演绎推理
- 定理证明的实质是对前提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 ∨ A 2 ) ∧ ( A 3 ∨ A 4 ) (A_{1}∨A_2)∧(A_3∨A_4 ) (A1∨A2)∧(A3∨A4)的形式，被称为 “ 合取范式”。
析取范式
设 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的亲本子句。
