Comp520MLCourse-5.1-GentzenSystem

语义树与金琛系统

一个文字(Literal)是一个原子命题或者一个原子命题的否。原子命题称为正文字, 原子命题的否称为负文字 $p$ $\{p,\lnot{p}\}$ 称为一对互补文字。

定理: 一组文字是可满足的, 当且仅当这组文字中不包含互补文字。

$S=\{p,q,{\lnot}q,{\lnot}r\}$ $p$ $q$ ${\lnot}q$ ${\lnot}r$ $q$ ${\lnot}q$ $S$ $S$ 是不可满足的。

通过语义树(Sematic Tableaux)分析公式的可满足性。open分支是可满足的; close分支是不可满足的。

$\{\alpha,\beta\}$ -公式建立语义树。

$\alpha$ -公式

\begin{matrix} (1) & \begin{array}{ccc} α & α_{1} & α_{2} \\ \neg \neg A_{1} & A_{1} \\ A_{1} \land A_{2} & A_{1} & A_{2} \\ \neg (A_{1} \lor A_{2}) & \neg A_{1} & \neg A_{2} \\ \neg (A_{1} \to A_{2}) & A_{1} & \neg A_{2} \\ \neg (A_{1} ↑ A_{2}) & A_{1} & A_{2} \\ A_{1} ↓ A_{2} & \neg A_{1} & \neg A_{2} \\ A_{1} \leftrightarrow A_{2} & A_{1} \to A_{2} & A_{2} \to A_{1} \\ \neg (A_{1} \oplus A_{2}) & A_{1} \to A_{2} & A_{2} \to A_{1} \end{array} \end{matrix}

$\beta$ -公式

\begin{matrix} (2) & \begin{array}{ccc} β & β_{1} & β_{2} \\ \neg (B_{1} \land B_{2}) & \neg B_{1} & \neg B_{2} \\ B_{1} \lor B_{2} & B_{1} & B_{2} \\ B_{1} \to B_{2} & \neg B_{1} & B_{2} \\ B_{1} ↑ B_{2} & \neg B_{1} & \neg B_{2} \\ \neg (B_{1} ↓ B_{2}) & B_{1} & B_{2} \\ \neg (B_{1} \leftrightarrow B_{2}) & \neg (B_{1} \to B_{2}) & \neg (B_{2} \to B_{1}) \\ B_{1} \oplus B_{2} & \neg (B_{1} \to B_{2}) & \neg (B_{2} \to B_{1}) \end{array} \end{matrix}

用语义树分析可满足性的两个实例

语义树不唯一

如果一个语义树的所有分支都是不可满足的,称该语义树是不可满足的。否则, 称该语义树是可满足的。

$X$ ${\lnot}X$ 的语义树是不可满足的。

$X$ ${\lnot}X$ $X$ 是永真的。

$X$ ${\lnot}X$ 的语义树是不可满足的。

$\mathcal{G}$ $\alpha$ $\beta$ 规则逐步推导, 最终证明命题。

$\mathcal{G}$ ${\vdash}(r{\vee}s){\rightarrow}(s{\vee}r)$ .

\begin{matrix} (3) & \begin{array}{lll} 1. & ⊢ \neg r, s, r & A x i o m \\ 2. & ⊢ \neg s, s, r & A x i o m \\ 3. & ⊢ \neg (r \lor s), s, r & β, 1, 2 \\ 4. & ⊢ \neg (r \lor s), s \lor r & α, 3 \\ 5. & ⊢ (r \lor s) \to (s \lor r) & α, 4 \end{array} \end{matrix}

${\vdash}p{\vee}(q{\wedge}r)\rightarrow(p{\vee}q)\wedge(p{\vee}r)$ .

\begin{matrix} (4) & \begin{array}{lll} 1. & ⊢ \neg p, p, q & A x i o m \\ 2. & ⊢ \neg p, p \lor q & α, 1 \\ 3. & ⊢ \neg p, p, r & A x i o m \\ 4. & ⊢ \neg p, p \lor r & α, 3 \\ 5. & ⊢ \neg p, (p \lor q) \land (p \lor r) & β, 2, 4 \\ 6. & ⊢ \neg q, \neg r, p, q & A x i o m \\ 7. & ⊢ \neg q, \neg r, p \lor q & α, 6 \\ 8. & ⊢ \neg q, \neg r, p, r & A x i o m \\ 9. & ⊢ \neg q, \neg r, p \lor r & α, 8 \\ 10. & ⊢ \neg q, \neg r, (p \lor q) \land (p \lor r) & β, 7, 9 \\ 11. & ⊢ \neg (q \land r), (p \lor q) \land (p \lor r) & α, 10 \\ 12. & ⊢ (p \lor \neg (q \land r)), (p \lor q) \land (p \lor r) & β, 5, 11 \\ 13. & ⊢ p \lor (q \land r) \to (p \lor q) \land (p \lor r) & α, 12 \end{array} \end{matrix}

金琛系统与语义树之间的联系