Invited Tutorials
Language
Tutorial speaker: Peter Sutton (UPF Barcelona)
Tutorial title: Polysemy, Copredication and Individuation.
Abstract: Click here
Logic & Computation
Tutorial speaker: Frank Wolter (University of Liverpool)
Tutorial title: Theory and Applications of Craig Interpolants.
Abstract: In 1957, Craig showed that first-order logic has the following property: if a formula P entails a formula Q, then there exists a formula I in the shared language of P and Q which is entailed by P and entails Q. The formula I is now called a Craig interpolant for P and Q and the property is called Craig interpolation. Craig interpolation proved to be a central property of first-order logic, implying in particular that any implicit definition of a predicate can be converted into an explicit definition (Beth definability property). More broadly, Craig interpolation indicates a good balance between syntax and semantics, and is nowadays one of the main properties considered when a new logic is proposed. It also has many practical applications, in particular in program verification, databases, and knowledge representation.
In this tutorial, I will start with a gentle introduction to Craig interpolation, taking propositional logic as an illustrating example. I will also discuss Beth definability and uniform interpolation. I will then discuss applications and give examples of logics enjoying the Craig interpolation property and also logics not enjoying it. Finally, I might briefly introduce a recent research project on investigating Craig interpolants for logics that do not enjoy Craig interpolation.