Skip to main content
Log in

Axiomatising first-order temporal logic: Until and since over linear time

  • Published:
Studia Logica Aims and scope Submit manuscript

Abstract

We present an axiomatisation for the first-order temporal logic with connectives Until and Since over the class of all linear flows of time. Completeness of the axiom system is proved.

We also add a few axioms to find a sound and complete axiomatisation for the first order temporal logic of Until and Since over rational numbers time.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Andréka, H., V. Goranko, S. Mikulás, I. Németi, and I. Sain, 1995, ‘Effective temporal logics of programs’, In [3].

    Google Scholar 

  2. Bell, J., and M. Machover, 1977, A course in Mathematical Logic, North-Holland.

  3. Bolc, L., and A. Szalas, 1995, editors. Time and Logic, UCL Press, London.

    Google Scholar 

  4. Burgess, J. P., 1982, ‘Axioms for tense logic I: ‘since’ and ‘until” Notre Dame J. Formal Logic, 23, 367–374.

    Google Scholar 

  5. Gabbay, D., I. Hodkinson, and M. Reynolds, 1994, Temporal Logic: Mathematical Foundations and Computational Aspects, Vol. 1, Oxford University Press.

  6. Gabbay, D. M., 1975, ‘Model theory for tense logics’, Ann. Math. Logic 8, 185–235.

    Google Scholar 

  7. Gabbay, D. M., and I. M. Hodkinson, 1990, ‘An axiomatisation of the temporal logic with until and since over the real numbers’, Journal of Logic and Computation 1, 229–260.

    Google Scholar 

  8. Gabbay, D. M., A. Pnueli, S. Shelah, and J. Stavi, 1980, ‘On the temporal analysis of fairness’, In 7th ACM Symposium on Principles of Programming Languages, Las Vegas, 163–173.

  9. Garson, J. W., 1984, ‘Quantification in modal logic’, In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, D. Reidel, Dordrecht.

    Google Scholar 

  10. Hodges, W., 1984, ‘Elementary predicate logic’, In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, D. Reidel, Dordrecht.

    Google Scholar 

  11. Manna, Z., and A. Pnueli, 1992, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, New York.

    Google Scholar 

  12. Reynolds, M., 1992, ‘An axiomatization for Until and Since over the reals without the IRR rule’, Studia Logica 51, 165–194.

    Google Scholar 

  13. Szalas, A., 1987, ‘Arithmetical axiomatization of first-order temporal logic’, Information Processing Letters 26.

  14. Szalas, A., 1987, ‘A complete axiomatic characterization of first-order temporal logic of linear time’, Theoretical Computer Science 54, 199–214.

    Google Scholar 

  15. van Benthem, J. F. g200A. K., 1982, The logic of time, Reidel, Dordrecht.

    Google Scholar 

  16. Venema, Y., 1991, ‘Completeness via completeness’, In M. de Rijke, editor, Colloquium on Modal Logic, 1991, ITLI-Network Publication, Instit. for Lang., Logic and Information, University of Amsterdam.

  17. Xu, M., 1988, ‘On some U, S-tense logics’, J. of Philosophical Logic 17, 181–202.

    Google Scholar 

  18. Zanardo, A., 1991, ‘A complete deductive system for since-until branching time logic’, J. Philosophical Logic.

Download references

Author information

Authors and Affiliations

Authors

Additional information

The author would like to thank Dov Gabbay and Ian Hodkinson for helpful discussions on this material. The work was supported by the U.K. Science and Engineering Research Council under the Metatem project (GR/F/28526).

Rights and permissions

Reprints and permissions

About this article

Cite this article

Reynolds, M. Axiomatising first-order temporal logic: Until and since over linear time. Stud Logica 57, 279–302 (1996). https://doi.org/10.1007/BF00370836

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF00370836

Key words

Navigation