Skip to content

命题逻辑

命题与联结词

联结词：否定词（并非）、合取词（并且）、析取词（或）、蕴涵词（如果 . . . 那么 . . . ） 和等值词（当且仅当） 其中仅否定词为一元联结词，其他都是二元。

命题语言\(\mathcal{L}^p\)

  1. 命题符号：
    • 永真命题：\(\top\)
    • 永假命题：\(\bot\)
  2. 联结符号：\(\neg, \lor, \land, \rightarrow, \leftrightarrow\)
  3. 标点符号：左、右括号

定义：命题公式

命题公式，简称公式，可定义如下： (1) 命题符号是公式，称为原子公式。 (2) 如果 𝜙 和 𝜓 是公式，那么 (¬𝜙), (𝜙 ∧ 𝜓), (𝜙 ∨ 𝜓), (𝜙 → 𝜓), (𝜙 ↔ 𝜓) 也是公式。 (3) 只有有限次使用 (1) (2) 条款所组成的符号串是公式。 或可用BNF形式表示如下： $$ \phi::=p|(\neg \phi)|(\phi\land \phi)|(\phi\lor \phi)|(\phi\rightarrow \phi)|(\phi\leftrightarrow \phi) $$

任意的命题公式有且只有如下形式之一：𝑝，(¬𝜙)，(𝜙∧𝜓)，(𝜙∨𝜓)，(𝜙 → 𝜓)，(𝜙 ↔ 𝜓)。

语义

定义：真假赋值

真假赋值是以所有命题符号的集为定义域，以真假值 \({1, 0}\) 为值域的函数。 真假赋值 \(v\) 给公式 \(p\) 记为 \(p^v\).

定义：公式的真值

真假赋值 𝑣 给公式指派的真值递归地定义如下：

  • \(p^v\in{1,0}\)

  • \((\neg \phi)^v=\begin{cases} 1, & \text{if}\phi^v=0\\ 0, & \text{otherwise} \end{cases}\)

  • \((\phi \land \psi)^v = \begin{cases} 1, & \text{if } \phi^v = \psi^v = 1 \\ 0, & \text{otherwise} \end{cases}\)

  • \((\phi \lor \psi)^v = \begin{cases} 1, & \text{if } \phi^v = 1 \text{ or } \psi^v = 1 \\ 0, & \text{otherwise} \end{cases}\)

  • \((\phi \rightarrow \psi)^v = \begin{cases} 1, & \text{if } \phi^v = 0 \text{ or } \psi^v = 1 \\ 0, & \text{otherwise} \end{cases}\)

  • \((\phi \leftrightarrow \psi)^v = \begin{cases} 1, & \text{if } \phi^v =\psi^v\\ 0, & \text{otherwise} \end{cases}\)

  • \(\top^v=1\)
  • \(\bot^v=0\)

一个命题公式在任何真假赋值下均为真，称为重言式；一个命题公式在任何真假赋值下均为假，称为矛盾式；一个命题公式在某个真假赋值为真，称为可满足式。

逻辑推论

给定一组公式集合 \(\Phi\) 作为前提，我们希望知道 \(\Phi\) 是否在逻辑上蕴涵某个结论 \(\phi\)。如果对 于任何真假赋值 \(v\), \(\Phi^v=1\) 总是蕴涵 \(\phi^v=1\)，那么我们说 \(\phi\) 是 \(\Phi\) 的逻辑推论，记作 \(\Phi\models \phi\)

则可进行如下定义： 给定一组命题公式集合 \(\Phi\) 和一个命题公式 \(\phi\)，\(\Phi\models\phi\) 当且仅当对于任意 \(v\)，如果 \(\Phi^v=1\) ，那么 \(\phi^v=1\)

定义：有效性

给定命题逻辑公式 𝜙，如果 \(\models\phi\)，我们说 𝜙 是有效的。

定理1

\({\phi_1,\phi_2,\dots,\phi_n}\models\phi\) 当且仅当 \(\models\phi_1\land\phi_2\land\cdots\phi_n\rightarrow\phi\)

定理2：有效性与可满足性

设 𝜙 是命题公式。那么，𝜙 是可满足的，当且仅当 ¬𝜙 不是有效的；𝜙 是有效的，当且仅当 ¬𝜙 不是可满足的。

定理

Φ |= 𝜙，当且仅当：Φ ∪ {¬𝜙} 是不可满足的，即 Φ ∪ {¬𝜙} |= ⊥。

定义：语义等价性

设 𝜙 和 𝜓 是命题公式。我们说 𝜙 和 𝜓 语义等价，记作 𝜙 |=| 𝜓，当且仅当 𝜙 |= 𝜓 并且𝜓 |= 𝜙。

定理：等值替换

给定 𝜙 |=| 𝜓, 且 𝜙 是 𝜑 的一部分。把 𝜑 中的 𝜙 替换成 𝜓 到 𝜑′。我们有 𝜑 |=| 𝜑′。

语义等价关系满足自反性、对称性和传递性，即命题公式的语义等价关系是一种等价关系。

范式

定义：合取范式

命题公式 𝜙 称为命题公式 𝜓 的合取范式，如果 𝜙 |=| 𝜓，且 𝜙 呈如下形式： $ D_1 \land D_2\land\cdots\land D_m$ 其中，\(D_i(i=1,2,\dots,m)\) 称为 \(\phi\) 的子句，形如 $ L_1 \lor L_2 \lor \cdots \lor L_n$。 \(L_j\) 为原子公式或原子公式否定，称 \(L_i\) 为子句的文字。

定理

任何命题公式与它的合取范式（析取范式）等价。

形式推演

目标：建立一个基于规则的推理系统，来判断一个有效推理是否成立。这样的规则为推理规则。 MP规则（肯定前件规则、蕴含消去）：由 \(\phi\) 和 \(\phi \rightarrow \psi\) 可得到 \(\psi\)。

形式可推演

给定一组前提集合 Φ = {𝜙1, 𝜙2, 𝜙3, . . . , , 𝜙𝑛} 和一个结论 𝜓, 其中 𝜙𝑖 和 𝜓 都是公式。我们说从这组前提到这个结论是形式可推演的，记作 Φ ⊢ 𝜓，如果存在一个证明：\(\psi_1, \psi_2,\cdots,\psi_m\) 使得 \(\psi_m=\psi\)。其中，每个 \(\psi_i(i=1,2,3,\dots, m)\) 要么属于 {𝜙1, 𝜙2, 𝜙3, . . . , , 𝜙𝑛}，要么依据 \({\psi_1,\dots,\psi_{i-1}}\) 中的公式通过应用一条推理规则得到。

推理系统的可靠性和完备性

设 ⊢𝑅 是由一组形式推演规则集合 𝑅 构成的推理系统，称为自然演绎系统。对于任意公式集合 Φ 和公式 𝜓, 我们说: - ⊢𝑅 是可靠的，当且仅当如果 Φ ⊢𝑅 𝜓，则 Φ \(\models\) 𝜓。 - ⊢𝑅 是完备的，当且仅当如果 Φ \(\models\) 𝜓，则 Φ ⊢𝑅 𝜓。

  • 如果一个推理系统是可靠的，那么它从一组真命题出发，通过形式推演得到的结 论也是真的。这一点确保了推理系统的正确性。
  • 如果一个推理系统是完备的，那么从一组真命题出发，可以推出这组真命题所蕴涵的所有结论。

消解原理

消解推演系统

采用子句公式表示合取范式：一个子句看出一个文字的集合，一个合取范式看成子句的集合。（不考虑重复和顺序）

子句公式

子句公式是子句的集合，可理解为子句的合取。子句是文字的集合，可理解为文字的析取。为了区分这两种集合，我们把文字的集合表示为 [𝐿1, 𝐿2, . . . , 𝐿𝑛]，等价于一个析取式𝐿1∨𝐿2∨· · ·∨𝐿𝑛，其中 𝐿𝑖 (𝑖 = 1, 2, . . . , 𝑛) 是文字；把子句的集合表示为 {𝐷1, 𝐷2, . . . , 𝐷𝑚}，等价于 𝐷1 ∧ 𝐷2 ∧ · · · ∧ 𝐷𝑚，其中 𝐷𝑖 (𝑖 = 1, 2, . . . , 𝑚) 是子句。

消解规则

给定两个子句，推出一个新子句：从子句 𝐷1 ∪ {𝐿} 和 𝐷2 ∪ {𝐿} 推出子句 𝐷1 ∪ 𝐷2。其中，𝐷1 和 𝐷2 可为空集。𝐷1 ∪ 𝐷2 称为输入子句关于 𝐿 的消解式。其中，𝐿 称为 𝐿 的补。对于任意原子命题 𝑝：𝑝 = ¬𝑝，¬𝑝 = 𝑝。

消解推理

从一个集合 Φ 推出一个子句 𝐷 的推演，记作 Φ ⊢Res 𝐷，是一个子句序列 𝐷1, 𝐷2, . . . , 𝐷𝑛，其中 𝐷𝑛 = 𝐷, 并且对于每个 𝐷𝑖，要么 𝐷𝑖 ∈ Φ，要么 𝐷𝑖 是该推导中前面两个子句的消解式。

可靠性、完全性、计算复杂性

定理

  1. 设有两个子句 𝐷1 ∪ {𝐿} 和 𝐷2 ∪ {\(\bar{L}\)}，则 𝐷1 ∪ {𝐿}, 𝐷2 ∪ {\(\bar{L}\)} |= 𝐷1 ∪ 𝐷2。
  2. 如果 Φ ⊢Res 𝐷 则 Φ |= 𝐷（可靠性）；反之（完备性），不成立。
  3. 消解系统是一个完备的否证系统，即：从一组有穷的前提集 Φ 出发，如果不存在 ⊥ 的证明，那么 Φ 是可满足的。

定理2 表明消解推理系统是可靠的，但是不完备。但是，当 \(D\) 为空子句时，消解推演及时可靠的又是完备的。

我们说一个证明系统 𝑅 是完备的，如果每个逻辑推论都有一个证明，即如果Φ |= 𝜙 则Φ ⊢𝑅 𝜙。对于消解系统来说，它是否证完备的，即：从一组有穷的前提集 Φ 出发，如果没有⊥ 的证明，那么 Φ 是可满足的。反之，如果 Φ 是不可满足的，那么就有从 Φ 到 ⊥ 的证明，即Φ ⊢Res ⊥。这是定理3。

消解算法复杂性

存在一个数字 𝑐 > 1 使得对于每个 𝑛，存在一个不可满足的公式，该公式包括 𝑛 个命题符号，其最小的消解否证包含至少 \(c^n\) 个步骤。

霍恩子句逻辑

霍恩子句

子句 𝐿1 ∨ · · · ∨ 𝐿𝑛 中如果至多包含一个正文字，那么该子句称为霍恩子句。

霍恩字句有如下四种形式：

  1. \(p\leftarrow q_1,\dots,q_m(m\neq 0)\)
  2. \(p\leftarrow\)(上式中 \(m=0\) )
  3. \(\leftarrow q_1,\dots,q_m(m\neq 0)\)
  4. \(\square\)(空语句，上式m=0)

其中 \(\leftarrow\) 为逻辑编程惯例写法，约定蕴涵前件的文字之间恒为合取，而蕴涵后件（箭头尖端）的文字之间恒为析取。

我们把一个形如 𝑝 ← 𝑞1, . . . , 𝑞𝑚 的霍恩子句称为一个过程，把 𝑝 称为过程名，把 {𝑞1, . . . ,𝑞𝑚} 称为过程体，各个 𝑞𝑖 可解释为过程调用。把形如 𝑝 ← 的霍恩子句看作一个事实，而把形如 ← 𝑞1, . . . , 𝑞𝑚 看作一个目标。目标全部由过程调用所组成，常用来表示一个询问。□ 可称 为停机语句，表示程序执行（成功）终止。

霍恩子句逻辑就是由这种子句组成的系统。它是命题演算系统的子系统。霍恩子句逻辑程序就是指这样一些被称为过程、目标和事实的霍恩子句的集合。

当一个霍恩子句刚好包含一个肯定文字时，我们称之为肯定的（或确定的）霍恩子句。当没有肯定文字时，该子句被称为否定霍恩子句。

例如，子句 [¬𝑝1, ¬𝑝2, . . . , ¬𝑝𝑛, 𝑞] 表示的是 ¬𝑝1 ∨ ¬𝑝2 ∨ · · · ∨ ¬𝑝𝑛 ∨ 𝑞。可以读作：如果 𝑝1 而且 𝑝2 而且 . . . 而且 𝑝𝑛 那么 𝑞。

SAT

Comments