In this paper, we establish an analogue of Craig Interpolation Property for a many-sorted variant of first-order hybrid logic. We develop a forcing technique that dynamically adds new constants to the underlying signature in a way that preserves consistency, even in the presence of models with possibly empty domains. Using this forcing method, we derive general criteria that are sufficient for a signature square to satisfy Craig interpolation property.

翻译：本文针对一阶混合逻辑的多类变体建立了克雷格插值性质的类似结果。我们发展了一种力迫技术，该技术以保持一致性的方式动态地向底层签名添加新常量，即使在可能具有空域模型的情况下也有效。利用这种力迫方法，我们推导出使签名矩形满足克雷格插值性质的充分通用准则。