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