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 NL 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 NLis equivalent to N and that for every Ndeduction or proof there must exist an NL deduction shorter in length than the former.
参考文献
1 黎仁蔚,N系统:一个自然时序演绎系统,《科学通报》,1988年第6期.
2 黎仁蔚,INCAPS:一个交互式计算机辅助定理证明系统,《计算机学报》,1989年第12期.
3 Kroger,Temporal Logic of Programs,Springer—Verlag,1987.
4 Manna,Z.,Verification of Sequential Programs:Temporal Axiomatization,in Theoretical Foundation of Programming Methodology,1982.