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

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

NL:A LOOSE NATURAL DEDUCTION SYSTEM OF TEMPORAL LOGIC

Owing to the characteristic of temporal logic,some rules of classical logic can't be used directly when doing temporal natural deduction. Though the N system shows us a solution of this problem in which all rules or deductions are divided into two types-verticality and horizontality, the two-dimensional mode also gives rise to some difficulties in deduction. This paper presents an N_L system (a loose natural deduction system of temporal logic) that provides us with a unified view of all rules and-deductions.In fact,we can prove as well that N_Lis equivalent to N and that for every Ndeduction or proof there must exist an N_L deduction shorter in length than the former.