命题逻辑

我们课上学的基本上就是这些了,大部分就是一些 trival 的是个人都能想通的东西,就是各种箭头(?)的用法容易混淆:

  • 设有命题 $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$ 分别代表 truefalse

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 子句1

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$ 都试一遍,如果推出了冲突的结论就回溯,如果全判定完了没冲突就成了。

1

“子句” 的定义是原子公式或 “$\neg 原子公式$” 的析取。