A Proof Theoretic Interpretation of Model Theoretic Hiding

Mihai Codescu; Fulya Horozal; Michael Kohlhase; Till Mossakowski; Florian Rabe

In: Hans-Jörg Kreowski; Till Mossakowski (Hrsg.). Recent Trends in Algebraic Development Techniques. International Workshop on Algebraic Development Techniques (WADT-10), 20th, July 1-4, Schloss Etelsen, Germany, Pages 118-138, Lecture Notes in Computer Science (LNCS), Vol. 7137, Springer, 2012.


Logical frameworks like LF are used for formal representa- tions of logics in order to make them amenable to formal machine-assisted meta-reasoning. While the focus has originally been on logics with a proof theoretic semantics, we have recently shown how to define model theoretic logics in LF as well. We have used this to define new institutions in the Heterogeneous Tool Set in a purely declarative way. It is desirable to extend this model theoretic representation of logics to the level of structured specifications. Here a particular challenge among structured specification building operations is hiding, which restricts a specification to some export interface. Specification languages like ASL and CASL support hiding, using an institution-independent model theoretic semantics abstracting from the details of the underlying logical system. Logical frameworks like LF have also been equipped with structuring languages. However, their proof theoretic nature leads them to a theory- level semantics without support for hiding. In the present work, we show how to resolve this difficulty.


Weitere Links

latin-hiding_wadt10.pdf (pdf, 492 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence