图灵机TM及可计算性

下推自动机PDA及上下文无关语言CFL

有穷自动机FA及正则语言RL

FC(一阶谓词演算系统)及其相关定理

ND(自然演绎推理系统)及其相关定理

PC(命题逻辑演算形式系统)及其相关定理