CI-BD-SOQE 2026
Workshop on Craig Interpolation, Beth Definability, and Second-Order Quantifier Elimination

FLoC 2026
Lisbon, Portugal, 24–25 July 2026

Topics and Aim

CI-BD-SOQE continues a series of previous workshops on Craig Interpolation, Beth Definability, and Second-Order Quantifier Elimination:

• Workshop on Craig Interpolation and Beth Definability (CIBD 2024)
• 4th Workshop on Interpolation: From Proofs to Applications (iPRA 2022)
• Second Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2021)
• First Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017)

Broadly viewed, Craig Interpolation (CI), Beth Definability (BD), and Second-Order Quantifier Elimination (SOQE) concern the existence and computation of formulas that capture consequences or logical constraints under some syntactic restrictions. Since such existence/computation questions arise in many areas of computer science, CI, BD, and SOQE have been thoroughly investigated by different communities, which has led to a large number of results, from foundational issues to practical applications. Relevant fields include proof theory, model theory, proof complexity, automated reasoning, automata theory, knowledge representation, program verification and databases as well as philosophy and linguistics.

Topics of interest for the workshop include, but are not limited to:

• Abductive reasoning
• Algorithms for CI, BD, SOQE and related tasks
• Applications of CI, BD, SOQE and related techniques
• Automating circumscription
• Automating modal correspondence theory
• CI and BD for specific logics
• CI and BD in model theory
• CI in program verification
• Forgetting in answer set programming
• Forgetting in knowledge representation
• Generalizations of CI
• Generating explanations via CI
• Implementation of CI, BD, SOQE and related tasks
• Ontology modularization and content extraction
• Proof complexity and feasible interpolation
• Proof systems for CI and BD
• Query rewriting on the basis of CI and BD
• Separability
• Solving constrained Horn clauses
• Solving formula equations
• Uniform interpolation

The aim of the workshop is to bring together researchers from the many relevant fields to exchange experiences and findings about approaches, techniques, ongoing research and important open problems. We strongly believe that CI, BD, and SOQE – beyond sharing a similar historical background – offer a common basis for fruitful cross-disciplinary exchange.

Invited Talks

• Marta Bílková, Czech Academy of Sciences, Czechia Agent Interpolation in Distributed Systems
  We introduce a new type of proof formalism for multiagent modal epistemic logics with S5-type modalities, viewed here as a logic of multiagent epistemic reasoning in distributed systems. We use this formalism to give a constructive proof that multiagent epistemic logic S5 enjoys a strong form of Craig interpolation property with respect to both propositional variables and agents, the latter in the form of agent-indexed knowledge modalities, a fact that has previously been proven using semantic methods. Our new proof formalism uses cross-word sequents that combine the features of hypersequents to represent individual S5 modalities—equivalence classes of individual agents—with nested sequents to represent the tree structure for alternating agent modalities—intersecting equivalence classes of distinct individual agents. The resulting calculus is sound and cut-free complete, allowing for strongly terminating proof search, and yields decidability and the finite model property for multiagent epistemic logic S5. No strongly terminating nested sequent calculus for S5 has been provided so far, and combining the structural features of hypersequents and nested sequents seems to be necessary to obtain computationally effective interpolation for agents rather than merely propositional variables. We further obtain Lyndon interpolation for propositional variables, which goes beyond existing semantic proofs of agent interpolation for multi agent epistemic logic S5. The talk is based on joint work with Wesley Fussner and Roman Kuznets.
• Balder ten Cate, University of Amsterdam, Netherlands Craig Interpolation within the Landscape of Decidable Fragments of First-Order Logic
  Motivated by applications of Craig interpolation in computer science, I will discuss some recent work pertaining to the Craig interpolation property (CIP) 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. We will discuss strategies that have been proposed to deal with this lack of CIP, as well as results that shed light on where, within the landscape of decidable fragment of first-order logic, one may find logics that enjoy CIP.
• Arie Gurfinkel, University of Waterloo, Canada Constrained Horn Clauses for Program Verification and Synthesis
  First-Order Logic (FOL) is a powerful formalism that naturally captures a wide range of decision and optimization problems. Over the past two decades, automated reasoning tools such as SAT and Satisfiability Modulo Theories (SMT) solvers have advanced dramatically, making logic-based approaches practical for many applications in computer science and program analysis. Today, many program analysis techniques formulate their verification tasks as logical constraints and rely on SAT or SMT solvers to reason about them automatically.

  In this talk, we focus on a fragment of FOL known as Constrained Horn Clauses (CHCs) and on SPACER, a state-of-the-art CHC solver. CHCs arise naturally in many verification and synthesis applications, including the discovery and verification of inductive invariants, safety verification of finite- and infinite-state systems, model checking of pushdown systems and their extensions, modular verification of distributed and parameterized systems, type inference, and many others.

  A key advantage of the CHC-based approach is the separation of proof methodology from proof search. Verification tasks are first encoded as CHCs through the generation of Verification Conditions (VCs), while the responsibility for solving these conditions is delegated to a CHC solver. This separation enables a single framework to support multiple proof methodologies, programming languages, and verification tasks, while maintaining high performance and scalability.

• Alessandra Palmigiano, Vrije Universiteit Amsterdam, Netherlands From Unified Correspondence to Parametric Correspondence
  In this talk, we discuss a research program aimed at establishing systematic connections among the first-order correspondents of Sahlqvist/inductive formulas/inequalities across various relational semantic settings. We will focus on modal reduction principles, and the relational settings we will discuss include crisp and many-valued Kripke frames, and crisp and many-valued polarity-based frames (aka enriched formal contexts). Building on unified correspondence theory, we will discuss a theoretical environment which makes it possible to: (a) compare and inter-relate the various frame correspondents (in different relational settings) of any given Sahlqvist modal reduction principle; (b) recognize when first-order sentences in the frame-correspondence languages of different types of relational structures encode the same “modal content”; (c) meaningfully transfer and represent well known relational properties such as reflexivity, transitivity, symmetry, seriality, confluence, density, across different semantic contexts; (d) transfer notions and results such as the van Benthem theorem and the Goldblatt-Thomason theorem across different semantic contexts. These results can be understood as a first step in a research program aimed at making correspondence theory not just (methodologically) unified, but also (effectively) parametric.
• Alexis Saurin, CNRS, France Proof-Relevant Interpolation: Beyond Cut-Free and Sequent Proofs
  In this talk, I will discuss several proof-relevant interpolation theorems, where we do not only factor a validity or provability judgment though an interpolant formula as is traditional, but also a deduction (or program if viewed through the lenses of Curry-Howard correspondence): if 𝜋 is a cut-free proof of 𝐴 ⊢ 𝐵, one can find an interpolant formula 𝐼 in the common vocabulary of 𝐴 and 𝐵 and proofs 𝜋₁, 𝜋₂ of 𝐴 ⊢ 𝐼 and 𝐼 ⊢ 𝐵 respectively such that 𝜋₁ composed with 𝜋₂ cut-reduces to 𝜋. I will refer to such results as Čubrić' interpolation, after Djordje Čubrić who first considered this kind of statements in the 90's.

  I will first focus on linear logic sequent calculus and refine Maehara's method to obtain a proof-relevant interpolation result where the interpolant is completely synthesised via cut-introduction. The flexibility of the approach is exploited to carry the interpolation-as-cut-introduction to classical and intuitionistic logics.

  While Maehara and Čubrić' interpolation results strongly rely on the tree structure of the deduction and its cut-freeness, I will then consider the question of how one can weaken some of those assumptions and show how proof-relevant interpolation naturally leads us to consider the interpolation problem for proofs with cuts as well as for LL proof-nets.

  This talk is based on a recent FSCD paper as well as joint works with Fiorillo, Le Boulc'h, Osorio and Pellissier.

• Amir Akbar Tabatabai, University of Groningen, Netherlands Feasible Interpolation: Power and Limitations
  Feasible interpolation is a property of a proof system, a complexity-sensitive variant of Craig interpolation, which has become a powerful tool in proof complexity. It can be used to establish the existence of hard theorems, that is, short formulas that require exponentially long proofs in a given system. In this talk, we provide a gentle introduction to feasible interpolation and its applications. We show that it holds for weak proof systems such as resolution and the cut-free sequent calculus, yielding exponential lower bounds on proof length. We then turn to strong proof systems, such as the sequent calculus LK, and show that feasible interpolation fails for them, assuming widely believed cryptographic hardness assumptions, including the security of RSA and the Diffie–Hellman key-exchange protocol against polynomial-size circuits. Finally, we explain how this failure implies that these strong proof systems are not automatable in a precise formal sense.

Submission

We invite submissions of:

• Works with original research, either as
  • Full paper: 10–15 pages + references, or
  • Extended abstract: 5–9 pages + references
• Abstracts of research published elsewhere, as
  • Abstract: 1–4 pages + references

Presentations of applications, new systems or relevant benchmarks are welcome.

It is expected that accepted submissions are presented at the workshop by at least one of the authors.

Submissions should be written in English, formatted with the CEURART style.

Submissions must be uploaded via the submission page https://submissions.floc26.org/ci-bd-soqe/.

Submissions will be reviewed by the program committee, which will select a balanced program of high-quality contributions.

The complete call for papers in text format suitable for posting is available from here.

Proceedings

The proceedings of the workshop have been submitted to CEUR Workshop Proceedings.

• Draft of the proceedings

Registration

Registration for the workshop is via the FLoC 2026 Registration. Note that 1 June 2026 is the deadline for early registration, and 13 July 2026 for late registration. After this deadline, on-site registration will be available at an increased rate.

Program

Schedule and Abstracts in the FLoC Detailed Program

Invited Talks

• Marta Bílková Agent Interpolation in Distributed Systems
• Balder ten Cate Craig Interpolation within the Landscape of Decidable Fragments of First-Order Logic
• Arie Gurfinkel Constrained Horn Clauses for Program Verification and Synthesis
• Alessandra Palmigiano From Unified Correspondence to Parametric Correspondence
• Alexis Saurin Proof-Relevant Interpolation: Beyond Cut-Free, Sequent Proofs
• Amir Akbar Tabatabai Feasible Interpolation: Power and Limitations

Book Launch

Balder ten Cate, Jean Christoph Jung, Patrick Koopmann, Christoph Wernhard and Frank Wolter (editors) Theory and Applications of Craig Interpolation
Ubiquity Press, 2026, DOI 10.5334/bdg, open access, to appear
Preprints available from https://cibd.bitbucket.io/taci/

Contributed Presentations

• Fabian Achammer and Stefan Hetzl An Algorithm for Existential Boolean Unification with Predicates
• Fabian Achammer, Stefan Hetzl and Renate A. Schmidt Computing Witnesses Using the SCAN Algorithm
• Andrea De Domenico, Giuseppe Greco, Alessandra Palmigiano and Apostolos Tzimoulis Modular Constructive Lyndon Interpolation for Nondistributive Logics
• Andrzej Indrzejczak Craig Interpolation Theorem in the Logic of Russellian Definite Descriptions
• Jean Christoph Jung, Jędrzej Kołodziejski and Frank Wolter Computation and Size of Interpolants for Hybrid Modal Logics
• Faezeh Labbaf, Tomas Kolarik, Martin Blicha, Grigory Fedyukovich, Michael Wand and Natasha Sharygina Using Craig Interpolation for Explanation of Neural Networks
• Andrew Lewis-Smith and Zhiguang Zhao Correspondence Theory for Intuitionistic Łukasiewicz Logic
• Simon Santschi and Niels C. Vooijs Interpolation above S4
• Renate A. Schmidt and Hongkai Yin Second-Order Quantifier Elimination and Uniform Interpolation for Basic Path Logic and the Ordered Fragment
• Friedrich Slivovsky Multiple Definitions from a Single Resolution Proof
• Christoph Wernhard Craig-Lyndon Interpolation for the Logic of Here and There with a Variation of Mints' Sequent System
• Jinghan Wu, Renate A. Schmidt and Yizheng Zhao Whereof One Cannot Explain, Thereof One Must Invent: Definitorial Abduction in ALCI via Strong Forgetting

Important Dates

Program Committee

Program Committee Chairs and Organizers