Craig Interpolation for Decidable First-Order Fragments
Logic in Computer Science
2025-09-03 v6
Abstract
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.
Cite
@article{arxiv.2310.08689,
title = {Craig Interpolation for Decidable First-Order Fragments},
author = {Balder ten Cate and Jesse Comer},
journal= {arXiv preprint arXiv:2310.08689},
year = {2025}
}