Uniform Interpolation, Automata and the Modal μ-Calculus.
Giovanna D’Agostino, Marco Hollenberg · Utrecht University Repository (Utrecht University) · 1996
A logic has interpolation if whenever we have two formulas and such that j then there is a formula I in the common language of and and in our logic of course such that j I j This intermediate formula is called the interpolant By the language of a formula we mean the non logical symbols i e the atomic actions and propositional constants that occur in it This notion is familiar from rst order logic and is known there as Craig Interpolation