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

Table of Contents

• Preface
  Summary: There were 12 submissions for peer review to this workshop: 4 full-length papers, 4 extended abstracts, and 4 abstracts of research published elsewhere. All of these 12 submissions were accepted for this volume.

Invited Talks

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

Papers

• An Algorithm for Existential Boolean Unification with Predicates (Extended Abstract) 7-14
  Fabian Achammer , Stefan Hetzl
• Modular Constructive Lyndon Interpolation for Nondistributive Logics 15-28
  Andrea De Domenico , Giuseppe Greco , Alessandra Palmigiano , Apostolos Tzimoulis
• Craig Interpolation Theorem in the Logic of Russellian Definite Descriptions 29-42
  Andrzej Indrzejczak
• Correspondence Theory for Intuitionistic Łukasiewicz Logic 43-58
  Andrew Lewis-Smith , Zhiguang Zhao
• Interpolation above S4 (Extended Abstract) 59-65
  Simon Santschi , Niels C. Vooijs
• Multiple Definitions from a Single Resolution Proof (Extended Abstract) 66-74
  Friedrich Slivovsky
• Craig-Lyndon Interpolation for the Logic of Here and There with a Variation of Mints' Sequent System (Extended Abstract) 75-85
  Christoph Wernhard
• Whereof One Cannot Explain, Thereof One Must Invent: Definitorial Abduction in ALCI via Strong Forgetting 86-102
  Jinghan Wu , Renate A. Schmidt , Yizheng Zhao

Abstracts of Research Published Elsewhere

• Computing Witnesses Using the SCAN Algorithm (Extended Abstract) 103-108
  Fabian Achammer , Stefan Hetzl , Renate A. Schmidt
• Computation and Size of Interpolants for Hybrid Modal Logics (Extended Abstract) 109-113
  Jean Christoph Jung , Jędrzej Kołodziejski , Frank Wolter
• Using Craig Interpolation for Explanation of Neural Networks (Abstract) 114-115
  Faezeh Labbaf , Tomas Kolarik , Martin Blicha , Grigory Fedyukovich , Michael Wand , Natasha Sharygina
• Second-Order Quantifier Elimination and Uniform Interpolation for Basic Path Logic and the Ordered Fragment (Extended Abstract) 116-122
  Renate A. Schmidt , Hongkai Yin