Lyndon Interpolation for Modal Logic via Type Elimination Sequences
Balder ten Cate

Abstract:
This note describes a method for constructing Lyndon interpolants based on quasi-models and type elimination sequences. The same method was employed in [Benedikt et al., 2015] (using mosaics) to compute optimal-size Lyndon interpolants for formulas in the guarded-fragment and the guarded-negation fragment. This note serves to showcase the method in a simpler setting, namely that of the basic modal language. To provide context, I also briefly survey some other general approaches that have been used to prove interpolation for modal logic in the past.
We finish with a list of questions.