Uniform Interpolation and Layered Bisimulation

Abstract

In this paper we give perspicuous proofs of Uniform Interpolation for the theories IPC, K, GL and S4Grz, using bounded bisimulations. We show that the uniform interpolants can be interpreted as propositionally quantified formulas, where the propositional quantifiers get a semantics with bisimulation extension or bisimulation reset as the appropriate accessibility relation. Thus, reversing the conceptual order, the uniform interpolation results can be viewed as quantifier elimination for bisimulation extension quantifiers.