Visser, Albert Uniform interpolation and layered bisimulation. (English) Zbl 0854.03026 Hájek, Petr (ed.), Gödel ’96. Logical foundations of mathematics, computer science and physics – Kurt Gödel’s legacy. Proceedings of a conference, Brno, Czech Republic, August 1996. Berlin: Springer-Verlag. Lect. Notes Log. 6, 139-164 (1996). Summary: 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.For the entire collection see [Zbl 0844.00017]. Cited in 1 ReviewCited in 32 Documents MSC: 03C40 Interpolation, preservation, definability 03C80 Logic with extra quantifiers and operators 03C10 Quantifier elimination, model completeness, and related topics Keywords:uniform interpolation; bounded bisimulations; quantifier elimination for bisimulation extension quantifiers PDFBibTeX XMLCite \textit{A. Visser}, Lect. Notes Log. 6, 139--164 (1996; Zbl 0854.03026)