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 Invited Speakers Call for Contributions Important Dates Program Committee Program Committee Chairs and Organizers

Topics and Aim

CI-BD-SOQE continues a series of previous workshops on Craig interpolation (CI), Beth definability (BD), and second-order quantifier elimination (SOQE):

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

Broadly viewed, CI, BD, and SOQE concern the existence and computation of formulas that simultaneously satisfy semantic as well as certain syntactic constraints. Since such existence/computation questions arise in many different areas of computer science, CI, BD, and SOQE have been thoroughly investigated, 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 knowledge representation and answer set programming
• 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 Speakers

TBA

Call for Contributions

TBA

Important Dates

w/c 4 May 2026		Workshop paper/extended abstract submission
w/c 18 May 2026		Reviews due
w/c 25 May 2026		Notification
w/c 1 Jun 2026		Early registration for FLoC 2026
w/c 8 Jun 2026		Camera-ready version due
24–25 July 2026		CI-BD-SOQE Workshop @ FLoC 2026

Program Committee

TBA

Program Committee Chairs and Organizers

Stefan Hetzl		TU Wien, Austria
Jean Christoph Jung		TU Dortmund University, Germany
Renate A. Schmidt		The University of Manchester, UK
Christoph Wernhard		University of Potsdam, Germany

---