Mathematical foundations for the reconfiguration paradigm

重构范式的数学基础

• 批准号: 20K03718
• 负责人: GAINA Daniel
• 金额: $ 2.83万
• 依托单位: Kyushu University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2020
• 资助国家: 日本
• 起止时间: 2020-04-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-20K03718/
• 关键词: reconfiguration paradigm; hybrid logics; dynamic logics; stratified institutions; interpolation; Robinson Consistency; omitting types theorem; hybrid logic; dynamic logic; institution; forcing; model theory; proof theory; algebraic specificat

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.

在本项目的最后一年中，我们证明了鲁滨逊的一致性逻辑的一致性属性。在古典的一阶逻辑中，鲁滨逊的一致性定理是克雷格（Craig）著名的插值定理的历史先驱，与之相同。在一阶逻辑的背景下，自Lindstrom的工作是在紧凑性的情况下以来就知道了，Robinson一致性属性是省略类型定理的结果。在Lindstrom的脚步之后，我们使用了省略类型定理用于本项目上一年中建立的许多分类混合动力的一阶逻辑，以获得Robinson一致性定理。该结果的重要推论是插值，这是一个逻辑属性，主要涉及结合和分解理论。引起插值兴趣的原因是，它是许多其他结果的来源。对于结构化的规格和形式方法，插值确保了模块语义的良好组成行为。通过整个研究期间，我们为本项目的整个研究时期设定了基础，以正式规范和可重新配置系统的形式规范和验证。关于混合动力逻辑的知识 - 被认为是适用于具有可重构功能的系统的描述和推理的知识 - 是在基于类别的分层机构定义提供的抽象级别上统一开发的。

项目成果

Omitting types theorem in hybrid dynamic first-order logic with rigid symbols

刚性符号混合动态一阶逻辑中的省略类型定理

• DOI: 10.1016/j.apal.2022.103212
• 发表时间: 2023
• 期刊: Annals of Pure and Applied Logic
• 影响因子: 0.8
• 作者: GAINA Daniel;BADIA Guillermo;KOWALSKI Tomasz
• 通讯作者: KOWALSKI Tomasz

Stability of termination under pushouts via amalgamation

通过合并推出的终止稳定性

• 发表时间: 2022
• 作者: Gaina Daniel;Kowalski Tomasz;Gaina Daniel;GAINA Daniel;GAINA Daniel
• 通讯作者: GAINA Daniel

Horn clauses in Hybrid-Dynamic Quantum Logic

混合动态量子逻辑中的 Horn 子句

• 发表时间: 2023
• 作者: Gaina Daniel;Kowalski Tomasz;Gaina Daniel;GAINA Daniel
• 通讯作者: GAINA Daniel

Forcing and its applications in hybrid-dynamic logics

力及其在混合动态逻辑中的应用

• 发表时间: 2020
• 作者: Gaina Daniel;Kowalski Tomasz;Gaina Daniel;GAINA Daniel;GAINA Daniel;GAINA Daniel;Daniel Gaina;Daniel Gaina;Daniel Gaina;Daniel Gaina;Daniel Gaina;Daniel Gaina
• 通讯作者: Daniel Gaina

La Trobe University(オーストラリア)

拉筹伯大学（澳大利亚）