Structuring theories on consequence

Jose Fiadeiro, Amilcar Sernadas

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

71 Citations (Scopus)

Abstract

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
PublisherSpringer
Pages44-72
Number of pages29
Volume332
ISBN (Electronic)9783540459705
ISBN (Print)9783540503255
Publication statusPublished - 1988

Publication series

Name Lecture Notes in Computer Science
PublisherSpringer Verlag
Volume332

Keywords

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

Fingerprint

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

Cite this