一句话：证明 guarded-negation 片段是 guarded 片段保持 Craig 插值的最小扩张，并给出其他片段插值扩张的不可判定性。
论文研究可判定一阶逻辑片段在加入 Craig 插值性质后需要扩张到多大。作者证明 guarded-negation 片段恰好是 guarded 片段保持 Craig 插值的最小扩张；相对地，二变量片段和 forward 片段保持 Craig 插值的任何扩张都包含完整一阶逻辑，因此其最小扩张是一阶逻辑。此外，论文证明二变量片段与 fluted 片段的所有保持 Craig 插值的扩张都是不可判定的。这些结果刻画了可判定一阶片段与插值性质之间的边界。
We show that the guarded-negation fragment is, in a precise sense, the smallest extension of the guarded fragment with Craig interpolation. In contrast, we show that full first-order logic is the smallest extension of both the two-variable fragment and the forward fragment with Craig interpolation. Similarly, we also show that all extensions of the two-variable fragment and of the fluted fragment with Craig interpolation are undecidable.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{CateC24,
title = {Craig Interpolation for Decidable First-Order Fragments},
author = {Balder ten Cate and Jesse Comer},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 3},
year = {2025},
doi = {10.46298/lmcs-21(3:22)2025}
}