Mathematical foundations for the reconfiguration paradigm

在本项目的最后一年，我们证明了一类大型混合动态逻辑的Robinson一致性。在经典一阶逻辑中，鲁滨逊一致性定理是著名的克雷格插值定理的历史前身，它与克雷格插值定理是等价的。在一阶逻辑的背景下，自从Lindstrom的工作以来，我们知道在紧性的存在下，Robinson一致性是省略类型定理的结果。跟随Lindstrom的脚步，我们使用在本项目前一年建立的多分类混合动态一阶逻辑的省略类型定理来获得罗宾逊一致性定理。这个结果的一个重要推论是插值，这是一个主要处理组合和分解理论的逻辑性质。对插值感兴趣的原因是它是许多其他结果的来源。对于结构化规范和形式化方法，插值保证了模块语义的良好组合行为。在致力于本项目的整个研究期间，我们为可重构系统的正式规范和验证奠定了基础。混合动态逻辑的知识——被认为适用于描述和推理具有可重构特征的系统——是在分层制度的基于类别的定义提供的抽象层次上统一发展的。

In the final year of the present project, we proved a Robinson Consistency Property for a large class of hybrid-dynamic logics. In classical first-order logic, Robinson's Consistency Theorem was a historical forerunner of Craig's celebrated Interpolation Theorem, to which it is equivalent. In the context of first-order logic, it is known since Lindstrom's work that in the presence of compactness, the Robinson Consistency Property is a consequence of the Omitting Types Theorem. Following in Lindstrom's footsteps, we used an Omitting Types Theorem for many-sorted hybrid-dynamic first-order logics established in the previous year of the present project to obtain a Robinson Consistency Theorem. An important corollary of this result is interpolation, which is a logical property that mostly deal with combining and decomposing theories. The reason for the interest in interpolation is the fact that it is the source of many other results. For structured specifications and formal methods, interpolation ensures a good compositional behavior of module semantics.Throughout the entire research period dedicated to the present project, we set the foundations for the formal specification and verification of reconfigurable systems. The knowledge on hybrid-dynamic logics -- recognized as suitable for describing and reasoning about systems with reconfigurable features -- was developed uniformly at an abstract level provided by the category-based definition of stratified institution.