发表机构
ELTE E\" o tv\" o s Lor\' a nd University Budapest, Hungary
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文针对匹配逻辑框架中的模型组合问题，基于多元多类别匹配逻辑变体提出依赖类型化的组合定义，确保组合保持可满足性证明，可为后续Rocq证明助手的机械化实现提供直接蓝本。
AI 中文摘要
本文研究匹配逻辑框架内的模型组合（常被称为“粘合”）。具体而言，我们考察了现有签名、变量赋值、理论及其对应模型的系统化组合方式。我们的核心目标是确保这种组合能够保持可满足性证明，即：所有能被各组成模型验证的理论，同样能被最终得到的组合模型验证。我们的定义基于匹配逻辑的多元、多类别变体，该变体也已在Rocq证明助手中实现形式化表达。因此，我们使用依赖类型来阐述这些定义，以期本研究能作为近期机械化实现的直接蓝本。
英文摘要
This paper investigates model composition—often referred to as "gluing"—within the framework of matching logic. Specifically, we examine the systematic combination of existing signatures, variable valuations, theories, and their corresponding models. Our primary objective is to ensure that this composition preserves satisfaction proofs; that is, any theory validated by the individual constituent models is also validated by the resulting composite model. Our definitions are based on a polyadic, sorted variant of matching logic, which has also been expressed in the Rocq proof assistant. Therefore, we outline our definitions with dependent types for this work to serve as a direct blueprint for the mechanization in the short-term future.
CommentsIn Proceedings FROM 2026, arXiv:2609.30324
Journal refEPTCS 452, 2026, pp. 191-216
