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
    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 623 times.
    This article's PDF has been downloaded 302 times.