Please use this identifier to cite or link to this item: http://hdl.handle.net/1822/34859

TitleEncoding hybridised institutions into first order logic
Author(s)Diaconescu, Razvan
Madeira, Alexandre
Issue date2016
PublisherCambridge University Press
JournalMathematical structures in computer science
Abstract(s)A ‘hybridization’ of a logic, referred to as the base logic, consists of developing the characteristic features of hybrid logic on top of the respective base logic, both at the level of syntax (i.e. modalities, nominals, etc.) and of the semantics (i.e. possible worlds). By ‘hybridized institutions’ we mean the result of this process when logics are treated abstractly as institutions (in the sense of the institution theory of Goguen and Burstall). This work develops encodings of hybridized institutions into (many-sorted) first order logic (abbreviated FOL) as a ‘hybridization’ process of abstract encodings of institutions into FOL, which may be seen as an abstraction of the well known standard translation of modal logic into first order logic. The concept of encoding employed by our work is that of comorphism from institution theory, which is a rather comprehensive concept of encoding as it features encodings both of the syntax and of the semantics of logics/institutions. Moreover we consider the so-called theoroidal version of comorphisms that encode signatures to theories, a feature that accommodates a wide range of concrete applications. Our theory is also general enough to accomodate various constraints on the possible worlds semantics as well a wide variety of quantifications. We also provide pragmatic sufficient conditions for the conservativity of the encodings to be preserved through the hybridization process, which provides the possibility to shift a formal verification process from the hybridized institution to FOL.
TypeArticle
Description"First published online: 12 November 2014"
URIhttp://hdl.handle.net/1822/34859
DOI10.1017/S0960129514000383
ISSN0960-1295
1469-8072
Peer-Reviewedyes
AccessOpen access
Appears in Collections:HASLab - Artigos em revistas internacionais

Files in This Item:
File SizeFormat 
1508.pdf492,44 kBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID