Craig Interpolation for Decidable First-Order Fragments

The Craig Interpolation Property (CIP) is a property of logics. It states that, for all formulas φ and ψ, if φ ⊧ ψ, then there exists an "interpolant" ϑ such that φ ⊧ ϑ and ϑ ⊧ ψ, and such that all non-logical symbols occurring in ϑ occur both in φ and in ψ. Craig [Craig, 1957] proved in 1957 that first-order logic (FO) has this property. Since then, many refinements of Craig’s result have been obtained (e.g., [Otto, 2000; Benedikt et al., 2016]). These have found applications in various areas of computer science and AI, including formal verification, modular hard/software specification and automated deduction [McMillan, 2018; Calvanese et al., 2020; Hoder et al., 2012], and more recently prominently in databases [Toman and Weddell, 2011; Benedikt et al., 2016] and knowledge representation [Lutz and Wolter, 2011; ten Cate et al., 2013; Koopmann and Schmidt, 2015]. 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 [Bárány et al., 2013]). 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 [Jung and Wolter, 2021; ten Cate and Comer, 2023].