NL:松弛时序逻辑自然推理系统

由于时序逻辑的特性所在,经典逻辑的某些规则不能直接用于时序自然推理,虽然N系统给出了一个解决办法——把所有规则或推理分为两类:垂直型和水平型,但这种二维模式又为推理带来了某些困难。本文提出了NL松弛时序逻辑自然推理系统,它为以上两类推理提供了统一视角,我们可以证明:NL与N等价;有N的证明则必有长度不超过它的NL证明