Sequent Calculus

一阶逻辑的LK系统详见软件分析与验证课件

相继式

相继式演算的推导式称为“相继式”。相继式是一种条件重言式，形如

$$\Gamma ⊢\Sigma$$

其中$\Gamma$是前件 antecedent，$\Sigma$为后件 consequent

推导规则

推导规则形如：

$$\frac{{\Gamma }_1⊢{\Sigma }_1{\Gamma }_n⊢{\Sigma }_n}{{\Gamma }_{n+1}⊢{\Sigma }_{n+1}}$$

其中横线上的部分为前提 Premise，下方为结论 Conclusion

前提为空的推导规则即为公理 Axiom

Related

• First-Order Logic 经典逻辑的相继式演算系统为LK（甘岑，1934）