Abstract We consider the problem of the existence of uniform interpolants in the modal logic K4. We first prove that all Box-free formulas have uniform interpolants in this logic. In the general case, we shall prove that given a modal formula phi and a sublanguage L of the language of the formula, we can decide whether phi has a uniform interpolant with respect to L in K4. The Box-free case is proved using a reduction to the Gödel Löb Logic GL, while in the general case we prove that the question of whether a modal formula has uniform interpolants over transitive frames can be reduced to a decidable expressivity problem on the mu-calculus.
Deciding the existence of uniform interpolants over transitive models
LENZI, Giacomo;
2011
Abstract
Abstract We consider the problem of the existence of uniform interpolants in the modal logic K4. We first prove that all Box-free formulas have uniform interpolants in this logic. In the general case, we shall prove that given a modal formula phi and a sublanguage L of the language of the formula, we can decide whether phi has a uniform interpolant with respect to L in K4. The Box-free case is proved using a reduction to the Gödel Löb Logic GL, while in the general case we prove that the question of whether a modal formula has uniform interpolants over transitive frames can be reduced to a decidable expressivity problem on the mu-calculus.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
