Overview - 概览

已完成 · 笔记范围：全

考试范围：

  PL (命题逻辑) FOL (一阶逻辑)
Syntax
(语法)		 Alphabet (\land, \lor, \to \dots)
w.f.f. (properties)
parse tree
precedence, convention		 Alphabet (\forall, \exists \dots)
const, predicate, function
terms, atom, w.f.f.
parse tree, convention
Semantics
(语义)		 Truth table
Tautology, contradiction
Satisfiable		 free / bound var
Interpretation / environment (\mathcal{I}, \xi)
\mathcal{I} \models_\xi \alpha \quad \Sigma \models \alpha
  \Sigma \models \alpha \quad \Sigma \not\models \alpha
adequate set
\equiv CNF / DNF (principal)		 valid, satisfiable
unsatisfiable
Formal proof
system
(形式化证明系统)		 Hilbert, ND, resolution ND
Soundness &
Completeness
(可靠性与完备性)		 Both（不考证明） Both
Formalization
(形式化)		 NL \to PL NL \to FOL

预备知识/证明系统的可靠性与完备性证明/霍尔逻辑不考。