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

Full metadata record
DC FieldValueLanguage
dc.contributor.authorDiaconescu, Razvanpor
dc.contributor.authorMadeira, Alexandrepor
dc.date.accessioned2015-04-15T11:46:44Z-
dc.date.available2015-04-15T11:46:44Z-
dc.date.issued2016-
dc.identifier.issn0960-1295-
dc.identifier.issn1469-8072-
dc.identifier.urihttp://hdl.handle.net/1822/34859-
dc.description"First published online: 12 November 2014"por
dc.description.abstractA ‘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.por
dc.description.sponsorshipWe thank both Till Mossakowski and Andrzej Tarlecki for the technical suggestion of using the predicates D. The work of the first author has been supported by a grant of the Romanian National Authority for Scientific Research, CNCS-UEFISCDI, project number PN-II-ID-PCE-2011-3-0439. The work of the second author was funded by the European Regional Development Fund through the COMPETE Programme, and by the Portuguese Foundation for Science and Technology through the projects FCOMP-01-0124-FEDER-028923 and NORTE-01-0124-FEDER-000060.por
dc.language.isoengpor
dc.publisherCambridge University Presspor
dc.rightsopenAccesspor
dc.titleEncoding hybridised institutions into first order logicpor
dc.typearticlepor
dc.peerreviewedyespor
dc.comments1508por
sdum.publicationstatuspublishedpor
oaire.citationStartPage1por
oaire.citationEndPage42por
oaire.citationIssue5por
oaire.citationTitleMathematical structures in computer sciencepor
oaire.citationVolume26por
dc.publisher.uriCambridge University Presspor
dc.identifier.doi10.1017/S0960129514000383por
dc.subject.wosScience & Technologypor
sdum.journalMathematical structures in computer sciencepor
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