Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] CfP: CI-BD-SOQE 2026: Workshop on Craig Interp...


view this post on Zulip Email Gateway (Feb 25 2026 at 13:35):

From: Christoph Wernhard <info@christophwernhard.com>

[Apologies if you receive multiple copies. Please forward
this call to interested parties.]

CALL FOR PAPERS

CI-BD-SOQE 2026
WORKSHOP ON CRAIG INTERPOLATION, BETH DEFINABILITY,
AND SECOND-ORDER QUANTIFIER ELIMINATION

FLoC 2026, Lisbon, Portugal
24-25 July 2026

Deadline: 4 May 2026

http://2026.ci-bd.soqe.org/

GENERAL INFORMATION

CI-BD-SOQE 2026 is a FLoC 2026 workshop and will take
place in Lisbon, Portugal, 24-25 July 2026. It 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, https://cibd.bitbucket.io/cibd2024/)

* 4th Workshop on Interpolation: From Proofs to
Applications (iPRA 2022, https://ipra-2022.bitbucket.io/)

* Second Workshop on Second-Order Quantifier Elimination
and Related Topics (SOQE 2021, http://2021.soqe.org/);

* First Workshop on Second-Order Quantifier Elimination and
Related Topics (SOQE 2017, http://2017.soqe.org/).

TOPICS AND AIM

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.

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
(https://ceur-ws.org/HOWTOSUBMIT.html#CEURART).

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.

PROCEEDINGS

Proceedings of the workshop will be published as CEUR
Workshop Proceedings.

REGISTRATION

Registration is via FLoC 2026:
https://www.floc26.org/registration

IMPORTANT DATES

4 May 2026: Submission deadline
25 May 2026: Author notification
1 June 2026: Early registration for FLoC workshops
24-25 July 2026: CI-BD-SOQE Workshop @ FLoC 2026

ORGANIZATION

Stefan Hetzl (TU Wien)
Jean Christoph Jung (TU Dortmund University)
Renate A. Schmidt (The University of Manchester)
Christoph Wernhard (University of Potsdam)


Last updated: Mar 14 2026 at 08:38 UTC