May I borrow your logic?

  • Maura Cerioli
  • José Meseguer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 711)


It can be very advantageous to borrow key components of a logic for use in another logic. The advantages may be not only conceptual; due to the existence of software systems supporting mechanized reasoning in a given logic, it may be possible to reuse a system developed for one logic—for example, a theorem-prover—to obtain a new system for another. Translations between logics by appropriate mappings provide a first way of reusing tools of one logic in another. This paper generalizes this idea to the case where entire components—for example, the proof theory—of one of the logics involved may be completely missing, so that the appropriate mapping could not even be defined. The idea then is to borrow the missing components (as well as their associated tools if they exist) from a logic that has them in order to create the full-fledged logic and tools that we desire. The relevant structure is transported using maps that only involve a limited aspect of the two logics in question—for example, their model theory. The constructions accomplishing this kind of borrowing of logical structure are very general and simple. They only depend upon a few abstract properties that hold under very general conditions given a pair of categories linked by adjoint functors.


Natural Transformation Logical System Proof Theory Forgetful Functor Logical Component 
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.
    E. Astesiano and M. Cerioli. Partial higher-order specifications. Fundamenta Informaticae, 16(2):101–126, 1992.Google Scholar
  2. 2.
    E. Astesiano and M. Cerioli. Relationships between logical frames. In M. Bidoit and C. Choppy, editors, Recent Trends in Data Type Specification, number 655 in LNCS, pages 126–143, Berlin, 1993. Springer Verlag.Google Scholar
  3. 3.
    R.M. Burstall and J.A. Goguen. The semantics of Clear, a specification language. In D. Bjørner, editor, Proceedings of the 1979 Copenhagen Winter School on Abstract Software Specification, number 86 in LNCS, pages 292–332, Berlin, 1980. Springer Verlag.Google Scholar
  4. 4.
    M. Cerioli and J. Meseguer. May I borrow your logic? Technical report, SRI International, Computer Science Laboratory, 1993. To appear.Google Scholar
  5. 5.
    H. Ehrig, M. Baldamus, and F. Cornelius. Theory of algebraic module specification including behavioural semantics, constraints and aspects of generalized morphisms. In Proceedings of 2nd International Conference on Algebraic Methodology and Software Technology, pages 101–125, Iowa City, Iowa, USA, 1991.Google Scholar
  6. 6.
    H. Ehrig and B. Mahr. Fundamentals of Algebraic Specifications 1: Equations and Initial semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer Verlag, Berlin, 1985.Google Scholar
  7. 7.
    J. Fiadeiro and A. Sernadas. Structuring theories on consequence. In D. Sannella and A. Tarlecki, editors, Recent Trends in Data Type Specification, number 332 in LNCS, pages 44–72, Berlin, 1987. Springer Verlag.Google Scholar
  8. 8.
    J.A. Goguen and R.M. Burstall. Introducing institutions. In E. Clarke and D. Kozen, editors, Logics of Programming Workshop, number 164 in LNCS, pages 221–255, Berlin, 1984. Springer Verlag.Google Scholar
  9. 9.
    J.A. Goguen and R.M. Burstall. A study in the foundations of programming methodology: Specifications, institutions, charters and parchments. In D. Pitt, S. Abramsky, A. Poigné, and D. Rydehard, editors, Proceedings of Summer Workshop on Category Theory and Computer Programming, number 240 in LNCS, pages 313–333, Berlin, 1986. Springer Verlag.Google Scholar
  10. 10.
    J.A. Goguen and R.M. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the ACM, 39(1):95–146, 1992.Google Scholar
  11. 11.
    J.A. Goguen and J. Meseguer. Eqlog: Equality, types, and generic modules for logic programming. In D. DeGroot and G. Lindstrom, editors, Logic Programming: Functions, Relations and Equations, pages 295–363. Prentice-Hall, 1986.Google Scholar
  12. 12.
    J.A. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J.-P. Jouannaud. Introducing OBJ. Technical Report SRI-CSL-92-03, SRI International, Computer Science Laboratory, 1992. To appear in J.A. Goguen, editor, Applications of Algebraic Specification Using OBJ, Cambridge University Press.Google Scholar
  13. 13.
    R. Harper, D. Sannella, and A. Tarlecki. Logic representation in LF. In D.H. Pitt et al., editor, Category Theory and Computer Science, number 389 in LNCS, pages 250–272. Springer Verlag, 1989.Google Scholar
  14. 14.
    S. MacLane. Categories for the Working Mathematician. Springer Verlag, 1971.Google Scholar
  15. 15.
    B. Mayoh. Galleries and institutions. Technical Report DAIMI PB — 191, Aarhus University, 1985.Google Scholar
  16. 16.
    J. Meseguer. General logics. In Logic Colloquium '87, pages 275–329, Amsterdam, 1989. North Holland.Google Scholar
  17. 17.
    J. Meseguer. A logical theory of concurrent objects and its realization in the Maude language. SRI Technical Report SRI-CSL-92-08, July 1992. To appear in G. Agha, P. Wegner, and A. Yonezawa, editors, Research Directions in Object-Based Concurrency, MIT Press, 1993.Google Scholar
  18. 18.
    P. Padawitz and M. Wirsing. Completeness of many-sorted equational logic revisited. Bulletin EATCS, (24), 1984.Google Scholar
  19. 19.
    A. Poigné. Foundations are rich institutions, but institutions are poor foundations. In H. Ehrig, H. Herrlich, Kreowski H.-J., and G. Preuß, editors, Categorical Methods in Computer Science, number 393 in LNCS, pages 82–101, Berlin, 1989. Springer Verlag.Google Scholar
  20. 20.
    A. Salibra and G. Scollo. A soft stairway to institutions. In Recent Trends in Data Type Specification, number 655 in LNCS, pages 310–329, Berlin, 1992. Springer Verlag.Google Scholar
  21. 21.
    D. Sannella and A. Tarlecki. On observational equivalence and specifications. Journal of Comp. and Sys. Sciences, 34:150–178, 1987.Google Scholar
  22. 22.
    A. Tarlecki. Free constructions in algebraic institutions. In M.P. Chytil and V. Koubek, editors, Proceedings of Mathematical Foundation of Computer Science '84, number 176 in LNCS, pages 526–534, Berlin, 1984. Springer Verlag.Google Scholar
  23. 23.
    A. Tarlecki. On the existence of free models in abstract algebraic institutions. Theoretical Computer Science, 37(3):269–304, 1985.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Maura Cerioli
    • 1
  • José Meseguer
    • 2
    • 3
  1. 1.DISI-Dipartimento di Informatica e Scienze dell'InformazioneUniversità di GenovaGenovaItaly
  2. 2.SRI InternationalMenlo Park
  3. 3.Center for the Study of Language and InformationStanford UniversityStanford

Personalised recommendations