This paper constitutes a first attempt at constructing semantic theories over institutions and examining the logical relations holding between different such theories. Our results show that this approach can be very useful for theoretical computer science (and may also contribute to the current philosophical debate regarding the semantic and the syntactic presentation of scientific theories). First we provide a definition of semantic theories in the institution theory framework - in terms of a set of models satisfying a given set of sentences - using the language-independent satisfaction relation characterizing institutions (Definition 17.3). Then we give a proof of the logical equivalence holding between the syntactic and the semantic presentation of a theory, based on the Galois connection holding between sentences and models (Theorem 17.1). We also show how to integrate and combine semantic theories using colimits (Theorem 17.2). Finally we establish when the output of a model-based software verification method applied to a semantic theory over an institution also holds for a semantic theory defined over a different institution (Theorem 17.3).

Building and integrating semantic theories over institutions / Angius, Nicola; Dimarogkona, Maria; Stefaneas, Petros. - 219:(2017), pp. 363-374. [10.1007/978-3-319-68103-0_17]

Building and integrating semantic theories over institutions

Angius, Nicola
;
2017-01-01

Abstract

This paper constitutes a first attempt at constructing semantic theories over institutions and examining the logical relations holding between different such theories. Our results show that this approach can be very useful for theoretical computer science (and may also contribute to the current philosophical debate regarding the semantic and the syntactic presentation of scientific theories). First we provide a definition of semantic theories in the institution theory framework - in terms of a set of models satisfying a given set of sentences - using the language-independent satisfaction relation characterizing institutions (Definition 17.3). Then we give a proof of the logical equivalence holding between the syntactic and the semantic presentation of a theory, based on the Galois connection holding between sentences and models (Theorem 17.1). We also show how to integrate and combine semantic theories using colimits (Theorem 17.2). Finally we establish when the output of a model-based software verification method applied to a semantic theory over an institution also holds for a semantic theory defined over a different institution (Theorem 17.3).
2017
9783319681023
Building and integrating semantic theories over institutions / Angius, Nicola; Dimarogkona, Maria; Stefaneas, Petros. - 219:(2017), pp. 363-374. [10.1007/978-3-319-68103-0_17]
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11388/203410
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact