Machine-checked interpolation theorems for substructural logics using display calculi

Abstract

We present a mechanised formalisation, in Isabelle/HOL, of Brotherston and Goré’s proof of Craig interpolation for a large of class display calculi for various propositional substructural logics. Along the way, we discuss the particular difficulties associated with the local interpolation property for various rules, and some important differences between our proofs and those of Brotherston and Goré, which are motivated by the ease of mechanising the development. Finally, we discuss the value for this work of using a prover with a programmable user interface (here, Isabelle with its Standard ML interface).