Uniform Interpolation and Layered Bisimulation

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

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.
Original languageEnglish
Title of host publicationGödel '96
PublisherCambridge University Press
Pages139-164
Number of pages26
DOIs
Publication statusPublished - 21 Mar 2017

Publication series

NameGödel '96

Fingerprint

Dive into the research topics of 'Uniform Interpolation and Layered Bisimulation'. Together they form a unique fingerprint.

Cite this