Journal of Computer Science and Technology

, Volume 3, Issue 3, pp 173–185 | Cite as

A natural deduction system of temporal logic

  • Li Renwei 
Regular Papers


This paper will present a natural deduction system of temporal logic, which includes two collections of inference rules called “horizontal inference rules” and “vertical inference rules” respectively. It is also proved that the system is both sound and complete under an appropriate interpretation. Very natural and generally short, each proof in the system can be represented by a matrix whose entries serve to record the inference process.


Temporal Logic Inference Rule Axiomatic System Concurrent Program Completeness Theorem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    M. Abadi, Z. Manna, Nonclausal Temporal Deduction, LNCS 193, Springer-Verlag, 1985.Google Scholar
  2. [2]
    H. Barringer, R. Kuiper, A. Pnueli, Now You May Compose Temporal Logic Specification, Proc. 16th ACM Symposium on the Theory of Computing, Washington, 1984.Google Scholar
  3. [3]
    M. Ben-Ari, Z. Manna, A. Pnuell, The Temporal logic of branching time,Acta Informatica,20(1983), 207–226.MATHCrossRefMathSciNetGoogle Scholar
  4. [4]
    E.M. Clarke, E.A. Emerson, A.P. Sistla, Automatic verification of finite-ctate concurrent system using temporal logic specification,ACM Trans. Programming Languages and Systems,8:2 (1986).Google Scholar
  5. [5]
    E.A. Emerson, J. Y. Halpern, “Sometimes” and “Not Never” revisited: on branching versus linear time temporal logic,J. ACM,33:1(1986).Google Scholar
  6. [6]
    G. E. Hughes, M. J. Gresswell, An Introduction To Modal Logic, Methuen and co. Ltd. 1968.Google Scholar
  7. [7]
    C. H. Kung, A Temporal Framework for Database Specification and Verification, Proc. of 10th International Conf. on VLDB, Singapore, 1984.Google Scholar
  8. [8]
    F. Kroger, On temporal program verification rules,Theoretical Informatics,19:3(1985).Google Scholar
  9. [9]
    F. Kroger, Temporal Logic of Programs, Springer-Verlag, 1987.Google Scholar
  10. [10]
    L. Lamport, “Sometimes” is sometimes “Not Never”—on the Temporal Logic of Programs, Proc. 7th ACM Symp. Principles of Programming Languages, 1980.Google Scholar
  11. [11]
    Z. Manna, Verification of sequential programs: Temporal axiomatization, in Theoretical Foundation of Programming Methodology, 1982.Google Scholar
  12. [12]
    Z. Manna, A. Pnueli, Verification of concurrent programs: the temporal framework, in Correctness Problem in Computer Science (R. S. Boyer & J. S. Moore, eds), International Lecture Series in Computer Science, Academic Press, London, 1981.Google Scholar
  13. [13]
    Z. Manna, A. Pnueli, Verification of concurrent programs: Temporal proof principles, in Logic of Programs, LNCS 131, Springer-Verlag, 1982.Google Scholar
  14. [14]
    R. P. McArthur, Tense Logic, D. Reidel Publishing Company, 1976.Google Scholar
  15. [15]
    S. Owicki, L. Lamport, Proving liveness properties of concurrent programs,ACM TOPLAS,4:3 (1982).Google Scholar
  16. [16]
    A. Pnueli, The Temporal Logic of Programs, 18th IEEE Symposium on Foundation of Computer Science, 1977.Google Scholar
  17. [17]
    A. Pnueli, The temporal semantics of concurrent programs,Theoretical Computer Science,13 (1981), 45–60.MATHCrossRefMathSciNetGoogle Scholar
  18. [18]
    N. Reacher, A. Urquart, Temporal Logic, Springer-Verlag, 1971.Google Scholar
  19. [19]
    A. Szalas, Concerning the semantic consequence relation in first-order temporal logic,Theoretic Computer Science,47:3(1987).Google Scholar
  20. [20]
    C. S. Tang, XYZ: A program development environment based on temporal logic, Programming Languages and System Design (ed. J. Bormann), 1983.Google Scholar
  21. [21]
    P. Wolper, Temporal logic can be more expressive, 22nd Annual Symposium on Foundation of Computer Science, 1981.Google Scholar

Copyright information

© Science Press, Beijing China and Allerton Press Inc. 1988

Authors and Affiliations

  • Li Renwei 
    • 1
  1. 1.Institute of SoftwareAcademia SinicaBeijing

Personalised recommendations