[PlanetKR] CfP: CI-BD-SOQE 2026: Workshop on Craig Interpolation, Beth Definability, and Second-Order Quantifier Elimination

[Christoph Wernhard]

[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)