Structuring theories on consequence

Jose Fiadeiro, Amilcar Sernadas

Research output: Chapter in Book/Report/Conference proceedingConference contribution

82 Citations (Scopus)


Building on the work of Goguen and Burstall on institutions and on Tarski's notion of deductive system, a categorial framework for manipulating theories in an arbitrary logic is presented. Its main contribution is the formalisation of the semantics of theory-building operations on top of a consequence relation. For that purpose, the notion of π-institution is proposed as an alternative to the notion of institution, replacing the notions of model and satisfaction by a primitive consequence operator in the definition of a logic. The resulting approach to the semantics of specification languages is intrinsically different from the original one in the sense that the ultimate denotation of a specification is taken herein to be a class of theories (sets of formulae closed for the consequence relation) and not a class of models of that logic. Adopting this point of view, the semantics of Clear-like specification building operations is analysed.
Original languageEnglish
Title of host publicationRecent Trends in Data Type Specification
Place of PublicationBerlin
Number of pages29
ISBN (Electronic)9783540459705
ISBN (Print)9783540503255
Publication statusPublished - 1988

Publication series

Name Lecture Notes in Computer Science
PublisherSpringer Verlag


  • Consequence Operator
  • Theory Level
  • Forgetful Functor
  • Data Constraint
  • Conservative Extension


Dive into the research topics of 'Structuring theories on consequence'. Together they form a unique fingerprint.

Cite this