We present an institution of observational logic suited for state-based systems specifications. The institution is based on the notion of an observational signature (which incorporates the declaration of a distinguished set of observers) and on observational algebras whose operations are required to be compatible with the indistinguishability relation determined by the given observers. In particular, we introduce a homomorphism concept for observational algebras which adequately expresses observational relationships between algebras. Then we consider a flexible notion of observational signature morphism which guarantees the satisfaction condition of institutions w.r.t. observational satisfaction of arbitrary first-order sentences. From the proof theoretical point of view we construct a sound and complete proof system for the observational consequence relation. Then we consider structured observational specifications and we provide a sound and complete proof system for such specifications by using a general, institution-independent result of [6].
CITATION STYLE
Hennicker, R., & Bidoit, M. (1998). Observational logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1548, pp. 263–277). Springer Verlag. https://doi.org/10.1007/3-540-49253-4_20
Mendeley helps you to discover research relevant for your work.