Skip to main content
SpringerLink
Log in

Synchronization of Logics

  • Published:
Studia Logica Aims and scope Submit manuscript

Abstract

Motivated by applications in software engineering, we propose two forms of combination of logics: synchronization on formulae and synchronization on models. We start by reviewing satisfaction systems, consequence systems, one-step derivation systems and theory spaces, as well as their functorial relationships. We define the synchronization on formulae of two consequence systems and provide a categorial characterization of the construction. For illustration we consider the synchronization of linear temporal logic and equational logic. We define the synchronization on models of two satisfaction systems and provide a categorial characterization of the construction. We illustrate the technique in two cases: linear temporal logic versus equational logic; and linear temporal logic versus branching temporal logic. Finally, we lift the synchronization on formulae to the category of logics over consequences systems.

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

Access this article

Log in via an institution

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. M. Arrais and J. Fiadeiro , 1996, Unifying theories in different institutions, in: M. Haveraaen, O. Owe and O.-J. Dahl, (eds), Recent Trends in Data Type Specification, Springer-Verlag, LNCS 1130, 81–101

  2. J. Barwise, 1974, Axioms for abstract model theory, Annals of Mathematical Logic, 7, 221–265

    Article  Google Scholar 

  3. A. Blass, 1984, The interaction between category theory and set theory, in: J. W. Gray, (ed), Mathematical Applications of Category Theory, AMS Series in Contemporary Mathematics, 5–29

  4. P. Blackburn and M.de Rijke, 1997, Why combine logics, Studia Logica, 59,1, 5–28

    Article  Google Scholar 

  5. R. Burstall and J. Goguen, 1977, Putting theories together to make specifications, in: R. Reddy, (ed), Proc. 5th Intl. Joint Conf. on Artificial Intelligence, Cambridge, Massachusetts, 1045–1058

  6. M. Cerioli and J. Meseguer, 1993, May I Borrow Your Logic, in: A. Borzyszkowski and S. Sokolowski, (eds), Mathematical Foundations of Computer Science 1993, LNCS, Springer-Verlag, 342–351

  7. M. Finger and D. Gabbay, 1992, Adding a temporal dimension to a logic system, Journal of Logic, Language and Information, 1, 203–233

    Google Scholar 

  8. M. Finger and D. Gabbay, 1996, Combining temporal logic systems, Notre Dame Journal of Formal Logic, 37, 204–232

    Article  Google Scholar 

  9. D. Gabbay (ed), 1994, What is a logical system?, Oxford Science Publications

  10. D. Gabbay, 1996, An overview of fibred semantics and the combination of logics, in: F. Baader and K. Schulz, (eds), Frontiers of Combining Systems, Kluwer Academic Publishers, 1–55

  11. J. Goguen and R. Burstall, 1992, Institutions: Abstract model theory for specification and programming, Journal of the ACM, 39,1, 95–146

    Article  Google Scholar 

  12. R. Goldblatt, 1992, Logics of Time and Computation, CSLI. Second edition

  13. J.-L. Lassez, V. L. Nguyen and E. A. Sonenberg, 1982, Fixed point theorems and semantics: A folk tale, Information Processing Letters, 14,3, 112–116

    Article  Google Scholar 

  14. J. Fiadeiro and A. Sernadas, 1988, Structuring theories on consequence, in: D. Sannella and A. Tarlecki, (eds), Recent Trends in Data Type Specification, Springer-Verlag, 44–72

  15. M. Kracht and F. Wolter, 1991, Properties of independently axiomatizable bimodal logics, Journal of Symbolic Logic, 56,4, 1469–1485

    Google Scholar 

  16. S. Mac Lane, 1971, Categories for the Working Mathematician, Springer-Verlag

  17. M. Manzano, 1996, Extensions of First Order Logic, Cambridge University Press

  18. J. Meseguer, 1989, General logics, in: H.-D. Ebbinghaus et al, (eds), Proceedings of the Logic Colloquium, 1987, North-Holland, 275–329

  19. A. Tarlecki, 1996, Moving between logical systems, in: M. Haveraaen, O. Owe and O.-J. Dahl, (eds), Recent Trends in Data Type Specification, Springer-Verlag, LNCS 1130, 478–502

  20. A. Tarski, 1956, On the concept of logical consequence, in: J. H. Woodger, (ed), Logic, Semantics, Metamathematics, Oxford Clarendon Press, 409–420

  21. A. Tarski, 1955, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, 5, 285–309

    Google Scholar 

  22. R. Thomason, 1984, Combinations of tense and modality, in: D. Gabbay and F. Guenthner, (eds), Handbook of Philosophical Logic II, Kluwer Academic Publishers, 135–165

  23. G. Winskel and M. Nielsen, 1995, Models of concurrency, in: S. Abramsky, D. Gabbay and T. Maibaum, (eds), Handbook of Logic in Computer Science 4, Oxford Science Publications, 1–148

  24. M. Ben-Ari, Z. Manna and A. Pnueli, 1981, The temporal logic of branching time, in: 8th ACM Symposium on Principles of Programming Languages, Williamsburg, VA, 164–176. Also, Acta Informatica, 20(3):207–226, 1983

  25. W. Penczek, 1988, A temporal logic for event structures, Fundamenta Informaticae, 11,3, 297–326

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Departamento de Matemática, IST, Av. Rovisco Pais, 1096, Lisboa, Portugal

    Amílcar Sernadas, Cristina Sernadas & Carlos Caleiro

Authors
  1. Amílcar Sernadas
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Cristina Sernadas
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Carlos Caleiro
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Sernadas, A., Sernadas, C. & Caleiro, C. Synchronization of Logics. Studia Logica 59, 217–247 (1997). https://doi.org/10.1023/A:1004904401346

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1004904401346

Search

Navigation