Balder ten Cate ; Jesse Comer - Craig Interpolation for Decidable First-Order Fragments

lmcs:14096 - Logical Methods in Computer Science, August 29, 2025, Volume 21, Issue 3 - https://doi.org/10.46298/lmcs-21(3:22)2025
Craig Interpolation for Decidable First-Order FragmentsArticle

Authors: Balder ten Cate ORCID; Jesse Comer ORCID

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.


Volume: Volume 21, Issue 3
Secondary volumes: Selected Papers of the 27th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2024)
Published on: August 29, 2025
Imported on: August 22, 2024
Keywords: Logic in Computer Science
Funding:
    Source : OpenAIRE Graph
  • Logic and Learning: an Algebra and Finite-Model-Theory Approach; Funder: European Commission; Code: 101031081

Consultation statistics

This page has been seen 777 times.
This article's PDF has been downloaded 434 times.