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.
| 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 b.d.tencate@uva.nl or any of the other organizers.
| 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 | |
| 10:30 – 11:00 | Coffee Break |
| 11:00 – 11:50 | Invited Talk Chair: Rahaleh Jalali |
| George Metcalfe | |
| Uniform Interpolation: An Algebraic Perspective | |
| 11:50 – 12:20 | Contributed Talks |
| 11:50 – 12:05 | Silvio Ghilardi |
| Interpolation Properties for Array Theories: Positive and Negative Results | |
| 12:05 – 12:20 | Sam van Gool |
| First Order Interpolation via Polyadic Spaces | |
| 12:20 – 13:20 | Lunch |
| 13:20 – 14:10 | Invited Talk Chair: Michael Benedikt |
| Thomas Place | |
| The Separation Problem in Automata Theory | |
| 14:10 – 14:40 | Contributed Talks |
| 14:10 – 14:25 | Reijo Jaakkola |
| Uniform Guarded Fragments: Interpolation and Complexity | |
| 14:25 – 14:40 | Quentin Blomet |
| Split Interpolations | |
| 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 | |
| 16:00 – 17:00 | Brainstorming on the Craig Interpolation Volume |
| Evening | Workshop Dinner |
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.