Workshop on Theory and Applications of Craig Interpolation and Beth Definability (CIBD 2024)

Invited Speakers Registration Book of Abstracts Program Venue Organizers

The aim of this workshop is to bring together experts from different research communities (such as proof theory, model theory, proof complexity, verification, database theory, knowledge representation, automated reasoning, automata theory, philosophy, linguistics) in order to discuss and disseminate recent and ongoing research pertaining to Craig interpolation and Beth definability.

The workshop will take place in Amsterdam on April 22-23, 2024.

Invited Speakers

Michael Benedikt University of Oxford, UK
Raheleh Jalali Czech Academy of Sciences, Czech Republic
Jean Christoph Jung TU Dortmund University, Germany
George Metcalfe University of Bern, Switzerland
Thomas Place LaBRI, France
Philipp Rümmer University of Regensburg, Germany


Attendance is free. There is limited funding available to support travel and accommodation costs of participants. Participants are also given the opportunity to give short presentations, selected by relevance and quality on the basis of a submitted abstract, as well as availability of slots. Abstracts should be at most one page using the easychair LaTeX style, and, if accepted for presentation, will be published on the webpage of the event (not as a formal proceedings).

The workshop is free to attend -- please register using this form.

For more information, please contact or any of the other organizers.

Book of Abstracts

CIBD 2024 – Book of Abstracts (PDF)


Monday, 22 April 2024

09:30 – 09:40 Opening Balder ten Cate, Patrick Koopmann, Christoph Wernhard, Frank Wolter
09:40 – 10:30 Invited Talk Chair: Christoph Wernhard
Philipp Rümmer
Craig Interpolation in SMT: A Survey [abstract, slides]
10:30 – 11:00 Coffee Break
11:00 – 11:50 Invited Talk Chair: Raheleh Jalali
George Metcalfe
Uniform Interpolation: An Algebraic Perspective [abstract]
11:50 – 12:20 Contributed Talks
11:50 – 12:05 Silvio Ghilardi
Interpolation Properties for Array Theories: Positive and Negative Results [abstract, slides]
12:05 – 12:20 Sam van Gool
First Order Interpolation via Polyadic Spaces[abstract, slides]
12:20 – 13:20 Lunch
13:20 – 14:10 Invited Talk Chair: Michael Benedikt
Thomas Place
The Separation Problem in Automata Theory [ abstract, slides ]
14:10 – 14:40 Contributed Talks
14:10 – 14:25 Reijo Jaakkola
Uniform Guarded Fragments: Interpolation and Complexity[abstract, slides]
14:25 – 14:40 Quentin Blomet
Split Interpolations [abstract]
14:40 – 15:10 Coffee Break
15:10 – 16:00 Invited Talk Chair: Frank Wolter
Jean Christoph Jung
Living without Beth and Craig: Interpolant and Definition Existence in Decidable Fragments of First-Order Logic [abstract, slides]
16:00 – 17:00 Brainstorming on the Craig Interpolation Volume
Evening Workshop Dinner

Tuesday, 23 April 2024

09:00 – 09:50 Invited Talk Chair: Balder ten Cate
Michael Benedikt
Nested Relations, Beth's theorem, and Gaifman Coordinitisation [abstract]
09:50 – 10:20 Contributed Talks
09:50 – 10:05 Jan Heuer and Christoph Wernhard
Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic [abstract, slides]
10:05 – 10:20 Mingqi Yang, Kevin Batz, Mingshuai Chen, Joost-Pieter Katoen, Zhiang Wu and Jianwei Yin
Latticed Craig Interpolation with an Application to Probabilistic Verification [abstract, slides]
10:20 – 10:50 Coffee Break
10:50 – 11:40 Invited Talk Chair: Patrick Koopmann
Raheleh Jalali
Is Every Interpolation Procedure Complete? [abstract, slides]
11:40 – 12:25 Contributed Talks
11:40 – 11:55 Iris van der Giessen
Uniform Interpolants and Bisimulation Quantifiers: Verified Constructions via Proof Systems [abstract, slides]
11:55 – 12:10 Bartosz Bednarczyk
Towards Model Theory of Ordered Logics: Expressivity and Interpolation [abstract]
12:10 – 12:25 Alexis Saurin
Craig-Lyndon Interpolation as Cut-Introduction[abstract]
12:25 – 14:00 Lunch
14:00 – 17:00 Planning the Craig Interpolation Volume


University of Amsterdam
Bushuis / Oost-Indisch Huis, Room 0.01
Kloveniersburgwal 48 (main entrance)
1012 CX Amsterdam


Balder ten Cate University of Amsterdam, The Netherlands
Patrick Koopmann Vrije Universiteit Amsterdam, The Netherlands
Christoph Wernhard University of Potsdam, Germany
Frank Wolter University of Liverpool, UK

Supported by a grant from the Evert Willem Beth Foundation and funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – Project-ID 457292495.