24 - 25 July 2026, CI-BD-SOQE 2026: Workshop on Craig Interpolation, Beth Definability, and Second-Order Quantifier Elimination, Lisbon [PT]
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.
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.
CI-BD-SOQE continues a series of previous workshops on Craig Interpolation, Beth Definability, and Second-Order Quantifier Elimination. Contributions shall be in the form of original research (full papers or extended abstracts) and abstracts of previously published research. If selected, at least one author is expected to present their work in person at the conference.