Combining Specification Formalisms in the ‘General Logic’ of Multialgebras

  • Yngve Lamo
  • Michał Walicki
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2755)


We recall basic facts about the institution of multialgebras, \(\mathcal{MA}\), and introduce a new, quantifier-free reasoning system for deriving consequences of multialgebraic specifications. We then show how \(\mathcal{MA}\) can be used for combining specifications developed in other algebraic frameworks. We spell out the definitions of embeddings of institution of partial algebras, \(\mathcal{PA}\), and membership algebras, \(\mathcal{MEMB}\) into \(\mathcal{MA}\). We also show an alternative relation, namely, institution transformation of \(\mathcal{PA}\) into \(\mathcal{MA}\) and discuss its role as compared to the embedding.


Natural Transformation Horn Clause General Logic Partial Algebra Algebraic Framework 
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.
    Adámek, J., Rosický, J.: Locally Presentable and Accessible Categories. Cambridge University Press, Cambridge (1994)CrossRefzbMATHGoogle Scholar
  2. 2.
    Białasik, M., Konikowska, B.: Reasoning with first-order nondeterministic specifications. Acta Informatica 36, 357–403 (1999)MathSciNetzbMATHGoogle Scholar
  3. 3.
    Burmeister, P.: Partial algebra - an introductory survey. Algebra Universalis 15, 306–358 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Cerioli, M., Mossakowski, T., Reichel, H.: From total equational to partial first order. In: Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B. (eds.) on Algebraic Foundations of Systems Specification. ch. 3, Springer, Heidelberg (1999)Google Scholar
  5. 5.
    Hussmann, H.: Nondeterminism in Algebraic Specifications and Algebraic Programs. Birkhäuser, Basel (1993)CrossRefzbMATHGoogle Scholar
  6. 6.
    Lamo, Y.: Institution of multialgebras as a general framework for algebric specification. PhD thesis, University of Bergen, Department of Informatics (2002)Google Scholar
  7. 7.
    Lamo, Y., Walicki, M.: Modeling partiality by nondeterminism. In: Callaos, N., Pineda, J.M., Sanchez, M. (eds.) Proceedings of SCI/ISAS 2001, Orlando, FL, vol. I (2001)Google Scholar
  8. 8.
    Lamo, Y., Walicki, M.: Specification of parameterized data types: Persistency revisited. Nordic Journal of Computing 8, 278–303 (2001)zbMATHGoogle Scholar
  9. 9.
    Lamo, Y., Walicki, M.: Composition and refinement of specifications and parameterised data types. In: Derrick, J., Boiten, E., Woodcock, J., von Wright, J. (eds.) Proceedings of the REFINE 2002 workshop, vol. 70/3. Elsevier Science Publishers, Amsterdam (2002), Google Scholar
  10. 10.
    Martini, A., Wolter, U.: A systematic study of mappings between institutions. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 300–315. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  11. 11.
    Meseguer, J.: General logics. In: Ebbinghaus, H.-D., et al. (eds.) Logic colloquium 1987, pp. 275–329. Elsevier Science Publisher B.V(North-Holland), Amsterdam (1989)Google Scholar
  12. 12.
    Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  13. 13.
    Mossakowski, T.: Equivalences among various logical frameworks of partial algebras. In: Kleine Büning, H. (ed.) CSL 1995. LNCS, vol. 1092, pp. 403–433. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  14. 14.
    Mosses, P.: Unified algebras and institutions. In: Proceedings of LICS 1989, 4-th Annual Symposium (1989)Google Scholar
  15. 15.
    Orejas, F.: Structuring and modularity. In: Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B. (eds.) on Algebraic Foundations of Systems Specification. ch. 6. Springer, Heidelberg (1999)Google Scholar
  16. 16.
    Pliuškievičienė, A.: Specialization of the use of axioms for deduction search in axiomatic theories with equality. J. Soviet Math. 1 (1973)Google Scholar
  17. 17.
    Tarlecki, A.: Institutions: An abstract framework for formal specifications. In: Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B. (eds.) on Algebraic Foundations of Systems Specification. ch. 4. Springer, Heidelberg (1999)Google Scholar
  18. 18.
    Walicki, M., Hodzic, A., Meldal, S.: Compositional homomorphisms of relational structures (modeled as multialgebras). In: Freivalds, R. (ed.) FCT 2001. LNCS, vol. 2138, p. 359. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  19. 19.
    Walicki, M., Meldal, S.: A complete calculus for the multialgebraic and functional semantics of nondeterminism. ACM TOPLAS 17(2) (March 1995)Google Scholar
  20. 20.
    Walicki, M., Meldal, S.: Multialgebras, power algebras and complete calculi of identities and inclusions. In: Recent Trends in Algebraic Specification Techniques. LNCS, vol. 906. Springer, Heidelberg (1995)Google Scholar
  21. 21.
    Walicki, M., Meldal, S.: Algebraic approaches to nondeterminism-an overview. ACM Computing Surveys 29 (1997)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Yngve Lamo
    • 1
  • Michał Walicki
    • 2
  1. 1.Bergen University CollegeBergenNorway
  2. 2.Dept. of InformaticsUniversity of BergenBergenNorway

Personalised recommendations