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

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
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
article

Craig Interpolation for Decidable First-Order Fragments

Jesse Comer, Balder ten Cate
1 links
Logical Methods in Computer Science
Computability, Logic, AI Algorithms
article

Craig Interpolation for Decidable First-Order Fragments

Jesse Comer, Balder ten Cate
article en

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.

Logical Methods in Computer ScienceVol. Volume 21, Issue 3
Openalex Percentile: Top 75%
Computability, Logic, AI Algorithms
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.

Craig Interpolation for Decidable First-Order Fragments — Jesse Comer, Balder ten Cate · Logical Methods in Computer Science (2025) | TGRS Research Map | TGRS