量词的推理规则

全称量词实例化

---

存在量词实例化

---

简化到命题逻辑推理

---

Generalized Modus Ponens（一般化分离规则）

一般化分离规则是分离规则（Modus Ponens）的提升版本——它将分离规则从命题逻辑提高到一阶逻辑。

---

举例

GMP（一般化分离规则）可用于确定子句的知识库（也称为确定性逻辑程序）中。确定子句是一种形式化的表示方法，其中每个子句都是一个析取式，而每个析取式都是由一个或多个文字（原子命题或它们的否定）构成的。确定子句知识库中的每个子句都是形如以下形式的规则：

L1 ∧ L2 ∧ … ∧ Ln → Q

其中，L1，L2 … Ln 是原子命题或它们的否定，并且 Q 是一个原子命题。这种表示方法的优点是简洁、易于处理和推理。

GMP 在确定子句知识库中的应用如下：

1. 从前提中提取出每个原子命题和结论，形成 L1，L2 … Ln 和 Q。

2. 找到一个最一般的替换 θ，使得前提中的每个原子命题都可以用替换后的形式匹配前提中的相应原子命题。

3. 将结论实例化为 Qθ。

4. 将 Qθ 添加到确定子句知识库中。

例如，假设我们有以下确定子句知识库：

1. 父亲(x) → 男性(x)
2. 母亲(x) → 女性(x)
3. 父亲(John)
4. 母亲(Mary)

现在我们想知道 John 是男性还是女性。我们可以使用 GMP 推理出 John 是男性，因为 John 是 Mary 的父亲，而所有的父亲都是男性。

这个推理过程可以用以下步骤表示：

1. 前提：父亲(John)。
2. 根据规则1，我们知道所有的父亲都是男性。
3. 找到一个最一般的替换 θ，使得父亲(John) 可以匹配父亲(x)。在这种情况下，θ = {x/John}。
4. 使用替换 θ 将男性(x) 实例化为男性(John)。
5. 推导出结论男性(John)，并将其添加到知识库中。

因此，我们可以得出结论：John 是男性。

---

合一

---

Forward chaining 前向链接算法

示例

---

Backward chaining algorithm 反向链接算法

一般FOL的FC/BC的完整性

FC和BC对于Horn KBs是完整的，但对于一般FOL KBs是不完整的：

存在一个负文字

---

归结算法

归结推理规则

证明举例

小结

• 一阶逻辑中的逻辑推理
  • 命题化推理问题/Reducing first-order inference to propositional inference
  • 效率较低
• 合一/ Unification
  • 用于确定适当的变量置换
• 一般化分离规则/ Generalized Modus Ponens
  • 确定子句/definite clauses
  • 可靠的，完备的
  • 应用于前向链接和反向链接算法
• 前向链接，反向链接
  • 归结推理/Resolution