Craig Interpolation for Decidable First-Order Fragments

Balder ten Cate, Jesse Comer

公開日: 2023/10/12

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.

Craig Interpolation for Decidable First-Order Fragments | SummarXiv | SummarXiv