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.
CITATION STYLE
Visser, A. (2017). Uniform Interpolation and Layered Bisimulation. In Gödel ’96 (pp. 139–164). Cambridge University Press. https://doi.org/10.1017/9781316716939.010
Mendeley helps you to discover research relevant for your work.