自然推理系统

P 规则: 前提在推导过程中任何时候都可以引用或使用. T 规则: 在推导中, 若有一个或多个公式重言蕴含中公式 $S$, 则 $S$ 课引入推导中.