NL:A LOOSE NATURAL DEDUCTION SYSTEM OF TEMPORAL LOGIC
Affiliation:

  • Article
  • | |
  • Metrics
  • |
  • Reference [1]
  • |
  • Related [20]
  • | | |
  • Comments
    Abstract:

    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.

    Reference
    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.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

何锫,唐稚松. NL:松弛时序逻辑自然推理系统.软件学报,1993,4(4):51-55

Copy
Share
Article Metrics
  • Abstract:2139
  • PDF: 3808
  • HTML: 0
  • Cited by: 0
History
  • Received:December 01,1990
  • Revised:March 18,1991
You are the first2038716Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063