FISP Kick-Off 2016   

Invited Speakers

Alessio Guglielmi, University of Bath, Bath, UK
Title: Making several computation/normalisation mechanisms coexist
Abstract: As is well known, we can interpret computationally any proof compression mechanism by unfolding, i.e., normalising, what is compressed. Normalisation generates proof complexity and one can hope that if the proof language is expressive and well designed, then useful notions of computation can be observed. If we look closely, we see different sources of proof complexity in the normalisation of predicate logic proofs: one is producing witnesses in Herbrand expansions by unpacking the contractive behaviour of quantifiers, another is unfolding propositional contractions. However, the elimination of cuts per se does not produce complexity, as is witnessed by cut elimination in propositional multiplicative linear logic. In Gentzen proof systems, these different mechanisms - cut on the one hand, propositional contraction and quantification on the other - cannot be separated and individually controlled. This is a pity, and indeed one could argue that the ability to do so might be important for computational interpretations, and not just in classical logic, but in every (well designed) logic. Therefore a natural question is: would it be possible to obtain a good normalisation theory where the sources of complexity can be separated, i.e., different normalisation mechanisms can coexist independently? In this talk, I will report about ongoing research with Andrea Aler Tubella and Benjamin Ralph and will state several results that taken together give a positive answer to that question, if we are willing to move beyond Gentzen theory and liberalise the way we compose proofs. As a matter of fact, we are on our way to integrating into a modular normalisation scheme a further computational mechanism associated to compression by substitution. I will also show that at the heart of these normalisation mechanisms there is a surprisingly simple inference shape and I will argue that understanding its dynamics is all it takes in order to understand most of normalisation across all proof systems for all logics.

Roman Kuznets, Vienna University of Techology, Vienna, Austria
Title: Interpolation beyond sequent calculi: modal, intuitionistic, and intermediate logics
Abstract: We will survey the recently developed method of proving Craig and Lyndon interpolation using analytic generalizations of sequent calculi, such as hypersequent, grafted hypersequent, nested sequent, linear nested sequent, and labelled sequent calculi. We discuss the pros and contras of the method, as well as the area of its applicability. The talk will include new, unpublished results on using the method for intermediate logics.

George Metcalfe, University of Bern, Bern, Switzerland
Title: Proof and Order
Abstract: I will speak about the structure and interpretation of proofs for ordered groups, emphasizing applications of proof theory in algebra.