Craig Interpolation for Decidable Fragments of First-Order Logic

The Craig Interpolation Property (CIP) is a property of logics. It states that, for all formulas f and phi, if f phi satisfies psi, then there exists an "interpolant" (sic) such that phi satisfies (sic) and satisfies psi, and such that all non-logical symbols occurring in. occur both in f and in.. Craig [6] proved in 1957 that first-order logic (FO) has this property. Since then, many refinements of Craig's result have been obtained (e.g., [12, 3]). These have found applications in various areas of computer science and AI, including formal verification, modular hard/software specification and automated deduction [11, 4, 7], and more recently prominently in databases [14, 2] and knowledge representation [10, 5, 9]. In this invited talk, we will survey recent work pertaining to Craig interpolation for various important decidable fragment of first-order logic, including guarded fragments, finite-variable fragments, and ordered fragments. Most of these fragments lack the CIP (the guarded-negation fragment GNFO being a notable exception [1]). We will discuss strategies that have been proposed in recent literature to deal with this lack of CIP, as well as recent results that shed light on where, within the landscape of decidable fragment of first-order logic, one may find logics that enjoy CIP [8, 13].