Observational Logic
Observational Logic
复制标题
观察逻辑
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
M. Bidoit
中科院分区：
文献类型：
--
作者：
R. Hennicker;M. Bidoit
我们提出了一种适合于基于状态的系统规范的观察逻辑制度。该制度是基于观测签名的概念（它包含了一组杰出观察者的声明）和观测代数，其操作要求与给定观察者确定的不可区分关系兼容。特别地，我们引入了一个观测代数的同态概念，它充分表达了代数之间的观测关系。然后我们考虑了一个灵活的观测特征态射的概念，它保证了机构的满足条件，而不是任意一阶句子的观测满足。从证明理论的角度，构建了一个完善的观测结果关系证明体系。然后，我们考虑结构化的观测规范，并通过使用一般的、独立于机构的[6]结果，为这些规范提供了一个健全和完整的证明系统。
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].