Craig Interpolation for Decidable First-Order Fragments

Balder ten Cate, Jesse Comer

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-ord…