CI-BD-SOQE — PROGRAM
Days: Friday, 24 July 2026 Saturday, 25 July 2026
Friday, 24 July 2026
09:00-10:30
Session 1
CI-BD-SOQE
Location:
C5.01
| 09:00-10:00 |
Invited Talk: Agent Interpolation in Distributed Systems (abstract) 60 min
1 Czech Academy of Sciences, Czechia
|
| 10:00-10:30 |
Interpolation above S4 (abstract) 30 min
1 Universität Bern
|
10:30-11:00
Coffee Break
CI-BD-SOQE
Location:
C5.01
11:00-12:30
Session 2
CI-BD-SOQE
Location:
C5.01
| 11:00-11:30 |
Craig-Lyndon Interpolation for the Logic of Here and There with a Variation of Mints' Sequent System (abstract) 30 min
1 University of Potsdam
|
| 11:30-12:00 |
Craig Interpolation Theorem in the Logic of Russellian Definite Descriptions (abstract) 30 min
1 University of Lodz
|
| 12:00-12:30 |
Modular Constructive Lyndon Interpolation for Nondistributive Logics (abstract) 30 min
1 IMDEA Software Institute
2 Vrije Universiteit Amsterdam
3 University of Luxembourg
|
12:30-14:00
Lunch
CI-BD-SOQE
Location:
C5.01
14:00-15:30
Session 3
CI-BD-SOQE
Location:
C5.01
| 14:00-15:00 |
Invited Talk: Craig Interpolation within the Landscape of Decidable Fragments of First-Order Logic (abstract) 60 min
1 University of Amsterdam, Netherlands
|
| 15:00-15:30 |
Computation and Size of Interpolants for Hybrid Modal Logics (abstract) 30 min
1 TU Dortmund University
2 University of Warsaw
3 University of Liverpool
|
15:30-16:00
Coffee Break
CI-BD-SOQE
Location:
C5.01
16:00-17:30
Session 4
CI-BD-SOQE
Location:
C5.01
| 16:00-17:00 |
Invited Talk: Feasible Interpolation: Power and Limitations (abstract) 60 min
1 University of Groningen, Netherlands
|
| 17:00-17:30 |
Multiple Definitions from a Single Resolution Proof (abstract) 30 min
1 University of Liverpool
|
17:30-18:00
Book Launch
CI-BD-SOQE
Location:
C5.01
| 17:30-18:00 |
Book Launch: Theory and Applications of Craig Interpolation (abstract) 30 min
1 University of Amsterdam, Netherlands
2 TU Dortmund University, Germany
3 Vrije Universiteit Amsterdam, Netherlands
4 University of Potsdam, Germany
5 University of Liverpool, UK
|
Saturday, 25 July 2026
09:00-10:30
Session 5
CI-BD-SOQE
Location:
C5.01
| 09:00-10:00 |
Invited Talk: Constrained Horn Clauses for Program Verification and Synthesis (abstract) 60 min
1 University of Waterloo, Canada
|
| 10:00-10:30 |
Computing Witnesses Using the SCAN Algorithm (abstract) 30 min
1 TU Wien
2 The University of Manchester
|
10:30-11:00
Coffee Break
CI-BD-SOQE
Location:
C5.01
11:00-12:30
Session 6
CI-BD-SOQE
Location:
C5.01
| 11:00-11:30 |
Whereof One Cannot Explain, Thereof One Must Invent: Definitorial Abduction in ALCI via Strong Forgetting (abstract) 30 min
1 Nanjing University
2 The University of Manchester
|
| 11:30-12:00 |
Second-Order Quantifier Elimination and Uniform Interpolation for Basic Path Logic and the Ordered Fragment (abstract) 30 min
1 The University of Manchester
2 Central European University
|
| 12:00-12:30 |
An Algorithm for Existential Boolean Unification with Predicates (abstract) 30 min
1 TU Wien
|
12:30-14:00
Lunch
CI-BD-SOQE
Location:
C5.01
14:00-15:30
Session 7
CI-BD-SOQE
Location:
C5.01
| 14:00-15:00 |
Invited Talk: From Unified Correspondence to Parametric Correspondence (abstract) 60 min
1 Vrije Universiteit Amsterdam, Netherlands
|
| 15:00-15:30 |
Correspondence Theory for Intuitionistic Lukasiewicz Logic (abstract) 30 min
1 Middlesex University
2 Taishan University
|
15:30-16:00
Coffee Break
CI-BD-SOQE
Location:
C5.01
16:00-17:30
Session 8
CI-BD-SOQE
Location:
C5.01
| 16:00-17:00 |
Invited Talk: Proof-Relevant Interpolation: Beyond Cut-Free and Sequent Proofs (abstract) 60 min
1 CNRS, France
|
| 17:00-17:30 |
Using Craig Interpolation for Explanation of Neural Networks (abstract) 30 min
1 University of Lugano
2 Florida State University
3 SUPSI, IDSIA, Lugano
|