重新开始学数学 • 数理逻辑（1）

命题逻辑

我们课上学的基本上就是这些了，大部分就是一些 trivial 的是个人都能想通的东西，就是各种箭头（？）的用法容易混淆：

• 设有命题 $A$ 和 $B$，$A \rightarrow B$ 指 “$A$ 实质蕴含 $B$” 这样一个命题，即

  if A then B
  

• 设有一堆命题 $A$ 和一个命题 $B$，$A \vdash B$ 指 “$B$ 是 $A$ 的句法后承” 这样一个 sequent。

  通过使用某些证明手段，从前提 $A$ 能证出 $B$，那么这个 sequent 就 valid，否则就不vaild。¹ $$ \require{bussproofs} \begin{prooftree} \AxiomC{A} \UnaryInfC{$\vdots$} \UnaryInfC{B} \end{prooftree} $$

• $ A \dashv \vdash B$：$A \vdash B$ 和 $ B \vdash A$ 都 valid，称为 $A$ 和 $B$ provably equivalent。

• 设有一堆命题 $A$ 和一个命题 $B$，$A \models B$：指 “$B$ 是 $A$ 的语义后承”，即如果 $A$ 中每一个命题都为真，则 $B$ 也为真。

  在自然演绎中，$A \models B$ 当且仅当 $ A \vdash B $

另外常常会使用 $\top$ 和 $\bot$ 分别代表 true 和 false。

Horn 公式和 Horn 可满足性问题

设 p 为原子公式，

$$ \displaylines { P ::= \bot | \top | p \\ A ::= P \mid P \wedge A \\ C ::= A \rightarrow P \\ H ::= C \mid C \wedge H } $$

其中 H 就是 Horn 公式，C 就是 Horn 子句²。

Horn 公式的几个例子：

$$ (p \wedge q \wedge s \rightarrow p) \wedge(q \wedge r \rightarrow p) \wedge(p \wedge s \rightarrow s) $$

$$ (p \wedge q \wedge s \rightarrow \perp) \wedge(q \wedge r \rightarrow p) \wedge(\top \rightarrow s) $$

$$ (p_{2} \wedge p_{3} \wedge p_{5} \rightarrow p_{13}) \wedge (\top \rightarrow p_{5}) \wedge (p_{5} \wedge p_{11} \rightarrow \perp) $$

Horn 公式的好处在于，和任意公式是否可满足（即 SAT 问题）是 NP 问题不同，HornSAT 是 P 问题，有这么一个判定算法：

fn horn_satisfiabe(formula: HornFormula) {
  let mut marked = HashSet::new();
  marked.add(⊤);
  while let Some(p) = 
    formula.find(|it| !it.rhs.marked && 
      it.lhs.all(|it| marked.contains(it))
    ).map(|it| it.rhs) {
    marked.add(p);
  }
  return !marked.contains(⊥);
}

Sat 求解器

感觉这里书上讲的好复杂……

其实就是自顶而下地考虑一个公式的 parse tree，对公式本身每一个子公式的值，如果能通过上层的值和算符的真值表直接判定就直接判定，比如：

$$ \top = \neg p \wedge q $$

从上层的 $\top$ 和 $\wedge$ 的性质我们就能得出 $$ \neg p = \top $$

$$ q = \top $$

不行的话（比如遇到了类似 $\top = p \vee q$ 的情况）就随便选一个子公式把 $\top$ 和 $\bot$ 都试一遍，如果推出了冲突的结论就回溯，如果全判定完了没冲突就成了。