Craig Interpolation for Decidable First-Order Fragments
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.
Authors
- Jesse Comer (ORCID: https://orcid.org/0009-0006-9734-3457)
- Balder ten Cate (ORCID: https://orcid.org/0000-0002-2538-5846)
Publication Details
- Journal
- Logical Methods in Computer Science
- Published
- 2025-08-29
- DOI
- https://doi.org/10.46298/lmcs-21(3:22)2025
- Primary Topic
- Computability, Logic, AI Algorithms
- Type
- article
- Field-Weighted Citation Impact
- 0.00