Craig Interpolation for Decidable Fragments of First-Order Logic (Invited Talk)

Author Balder ten Cate

Thumbnail PDF


  • Filesize: 403 kB
  • 2 pages

Document Identifiers

Author Details

Balder ten Cate
  • ILLC, University of Amsterdam, The Netherlands

Cite AsGet BibTex

Balder ten Cate. Craig Interpolation for Decidable Fragments of First-Order Logic (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


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].

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
  • Theory of computation → Automated reasoning
  • First-Order Logic
  • Decidable Fragments
  • Craig Interpolation


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Vince Bárány, Michael Benedikt, and Balder ten Cate. Rewriting guarded negation queries. In Proceedings of MFCS 2013, pages 98-110, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  2. Michael Benedikt, Julien Leblay, Balder ten Cate, and Efthymia Tsamoura. Generating plans from proofs : the interpolation-based approach to query reformulation. Synthesis Lectures on Data Management. Morgan & Claypool, 2016. Google Scholar
  3. Michael Benedikt, Balder ten Cate, and Efthymia Tsamoura. Generating plans from proofs. ACM Trans. Database Syst., 40(4):22:1-22:45, 2016. URL:
  4. Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, and Andrey Rivkin. Combined covers and beth definability. In Proceedings of the 10th International Joint Conference on Automated Reasoning, Part I, IJCAR 2020, pages 181-200. Springer, 2020. URL:
  5. Balder ten Cate, Enrico Franconi, and Inanç Seylan. Beth definability in expressive description logics. J. Artif. Int. Res., 48(1):347-414, October 2013. Google Scholar
  6. William Craig. Three uses of the herbrand-gentzen theorem in relating model theory and proof theory. Journal of Symbolic Logic, 22(3):269-285, 1957. URL:
  7. Krystof Hoder, Andreas Holzer, Laura Kovács, and Andrei Voronkov. Vinter: A Vampire-based tool for interpolation. In Ranjit Jhala and Atsushi Igarashi, editors, Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings, volume 7705 of Lecture Notes in Computer Science, pages 148-156. Springer, 2012. URL:
  8. Jean Christoph Jung and Frank Wolter. Living without beth and craig: Definitions and interpolants in the guarded and two-variable fragments. In Proceedings of LICS 2021, pages 1-14. IEEE Computer Society, July 2021. URL:
  9. Patrick Koopmann and Renate A. Schmidt. Uniform interpolation and forgetting for ALC ontologies with ABoxes. In Proceedings of the 29th AAAI Conference on Artificial Intelligence, AAAI 2015, pages 175-181. AAAI Press, 2015. URL:
  10. Carsten Lutz and Frank Wolter. Foundations for uniform interpolation and forgetting in expressive description logics. In Proceedings of the 22nd International Joint Conference on Artificial Intelligence, IJCAI 2011, pages 989-995. IJCAI/AAAI, 2011. URL:
  11. Kenneth L. McMillan. Interpolation and model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 421-446. Springer, 2018. URL:
  12. Martin Otto. An interpolation theorem. The Bulletin of Symbolic Logic, 6(4):447-462, 2000. URL:
  13. Balder ten Cate and Jesse Comer. Craig interpolation for decidable first-order fragments, 2023. URL:
  14. David Toman and Grant E. Weddell. Fundamentals of Physical Design and Query Compilation. Synthesis Lectures on Data Management. Morgan & Claypool Publishers, 2011. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail