逻辑推理中的决议算法及相关理论

### 逻辑推理中的决议算法及相关理论 #### 1. 决议算法的可靠性与完备性 决议算法有两个主要问题：可靠性和完备性。可靠性指证明过程的正确性，完备性意味着使用该算法可以推导出所有可能的推理。 - **可靠性定义**：若从一组公理 $S$ 通过证明过程证明了任何推理 $\alpha$（即 $S\vdash\alpha$），那么 $\alpha$ 从 $S$ 逻辑推导得出（即 $S\vDash\alpha$），则该证明过程称为可靠的。 - **完备性定义**：对于任何从给定公理集 $S$ 逻辑推导得出的推理 $\alpha$（即 $S\vDash\alpha$），证明过程能够证明 $\alpha$（即 $S\vdash\alpha$），则该证明过程称为完备的。 下面是对决议定理可靠性和完备性的证明： - **决议定理的可靠性**：给定一组子句 $S$ 和目标 $\alpha$，假设通过决议定理从 $S$ 推导出 $\alpha$（即 $S\vdash\alpha$）。采用反证法，假设 $S\vDash\alpha$ 为假，即 $S\vDash\neg\alpha$，那么 $\neg\alpha$ 是可满足的。为满足它，为 $\alpha$ 中使用的所有命题分配真值（真/假）。可以证明，对于这样的分配，$S$ 中任意两个子句的归结将为真，即使通过归结耗尽所有子句，结果子句也不会为假，这与 $S\vdash\alpha$ 矛盾。因此，假设 $S\vDash\neg\alpha$ 为假，从而 $S\vDash\alpha$ 为真。 - **决议定理的完备性**：设 $\alpha$ 是一个公式，从给定的子句集 $S$ 有 $S\vDash\alpha$，即 $\alpha$ 可以从 $S$ 逻辑证明。采用反证法，假设 $S\vdash\alpha$ 不成立，即 $S\vdash\neg\alpha$，也就是 $\alpha$ 不能通过证明过程从 $S$ 推导得出。所以 $S_1 = S \cup \{\neg\alpha\}$（都以子句形式表示）是不可满足的。根据地面决议定理，“如果一组地面子句（无变量的子句）是不可满足的，那么这些子句的归结闭包包含‘假’子句”。由于 $S_1$ 不可满足，$S_1$ 的归结闭包产生空子句，这与 $S\vdash\neg\alpha$ 矛盾，所以假设错误，$S\vdash\alpha$ 成立。 #### 2. 谓词逻辑 谓词逻辑（也称为一阶谓词逻辑）与命题逻辑有相似的形式，但使用谓词逻辑进行推理和知识表示的能力高于命题逻辑。它包含两个额外的量词：全称量词（$\forall$）和存在量词（$\exists$）。 - **谓词逻辑的字母表**： - 常量：$a, b, c$ - 变量：$X, Y, Z$ - 函数：$f, g, h$ - 运算符：$\land, \lor, \neg, \to$ - 量词：$\forall, \exists$ - 谓词：$P, Q, R$ - **术语定义**：术语递归定义为常量、变量或函数应用于术语的结果，例如 $a, x, t(x), t(g(x))$ 都是术语。 - **函数和谓词的定义**： - 函数表示定义在域 $D$ 上的关系，将 $n$ 个元素（$n > 0$）映射到域中的单个元素，如“father - of”，“age - of”。$n$ 元函数写为 $f(t_1, t_2, \ldots, t_n)$，其中 $t_i$ 表示术语，0 元函数是常量。 - 谓词符号表示从域 $D$ 的元素到真值（真或假）的关系或函数映射，大写字母如 $P, Q, MARRIED, EQUAL$ 用于表示谓词。$P(t_1, t_2, \ldots, t_n)$ 表示 $n$ 元谓词，其中 $t_i$ 是术语，0 元谓词是命题，即常量谓词。 - **一阶逻辑的句子（合式公式，WFF）定义**： 1. 如果 $P(t_1, t_2, \ldots, t_n)$ 是 $n$ 元谓词，则 $P$ 是原子公式。 2. 原子公式是合式公式。 3. 如果 $P$ 和 $Q$ 是合式公式，则 $P \land Q, P \lor Q, \neg P, P \to Q$ 都是合式公式，$\forall X R(X)$ 也是合式公式。 4. 如果 $P$ 是合式公式且 $X$ 不是 $P$ 中的量化变量，则 $P$ 在量化后仍然是合式公式，例如 $\forall X P$ 或 $\exists X P$ 是合式公式。 **示例**：将以下句子重写为一阶逻辑： 1. Coconut - crunchy 是饼干：$Biscuit(coconut - crunchy)$ 2. Mary 是吃 Coconut - crunchy 的孩子：$Child(mary) \land Takes(mary, coconut - crunchy)$ 3. John 爱拿饼干的孩子：$\forall X ((Child(X) \land \exists Y (Takes(X, Y) \land Biscuit(Y))) \to Loves(john, X)$ 4. John 爱 Mary：$Loves(john, mary)$ #### 3. 将句子转换为子句形式 以下是将复杂句子转换为简单子句的算法步骤： |步骤|操作|示例（以 $\forall X ((Child(X) \land \exists Y (Takes(X, Y) \land Biscuit(Y))) \to Loves(john, X)$ 为例）| | ---- | ---- | ---- | |步骤 I|消除蕴含运算符：将“$\to$”运算符替换为“$\neg$”和“$\lor$”运算符|$\forall X (\neg (Child(X) \land \exists Y (Takes(X, Y) \land Biscuit(Y))) \lor Loves(john, X)$| |步骤 II|减少否定范围：根据规则替换“$\neg$”符号|$\forall X (\neg Child(X) \lor \forall Y (\neg Takes(X, Y) \lor \neg Biscuit(Y)) \lor Loves(john, X)$| |步骤 III|重命名量词范围内的变量|此例中 $X$ 和 $Y$ 不同，无需操作| |步骤 IV|将量词移到表达式前面|$\forall X \forall Y \neg Child(X) \lor \neg Takes(X,Y) \lor \neg Biscuit(Y) \lor Loves(john, X)$| |步骤 V|将存在量词替换为全称量词的 Skolem 函数|此例中 $Y$ 不是 $X$ 的子集，无需操作，去掉全称量词| |步骤 VI|将结果表达式转换为合取范式（CNF）|此例结果表达式已是 CNF，无需操作| |步骤 VII|每行写一个子句|$Child(X), Takes(X, Y), Biscuit(Y) \to Loves(john, X)$| #### 4. 谓词的合一 两个谓词 $P(t_1,t_2,\ldots, t_n)$ 和 $Q(s_1, s_2,\ldots, s_n)$ 可以合一，如果术