## Interpolation with Decidable Fixpoint Logics

* Michael
Benedikt*, * Balder ten Cate * and * Michael Vanden Boom*
A logic satisfies Craig interpolation if whenever one formula in the logic entails another formula
in the logic, there is an intermediate
formula --- one entailed by the first and entailing second --- using only relations in the common signature of the two formulas.
Uniform interpolation strengthens this by requiring
the interpolant to depend only on the antecedent formula and the common signature. A uniform interpolant
can thus be thought of as a minimal upper approximation of a formula within a subsignature.
For first-order logic, interpolation holds but uniform interpolation fails. Uniform interpolation is known to hold
for several modal and description logics, but little is known about uniform interpolation for fragments of predicate
logic over relations with arbitrary arity. Further, little is known about ordinary Craig interpolation for logics over relations
of arbitrary arity that
have a recursion mechanism, such as fixpoint logics.
In this work we take a step towards filling these gaps, proving interpolation for a decidable fragment of least fixpoint logic
called
unary negation fixpoint logic. We prove this by showing that for any fixed k$ uniform interpolation holds for the k-variable
fragment of the logic. In order to show this we develop the technique of reducing questions about logics with tree-like models
to questions about modal logics, following an approach by Gradel, Hirsch, and Otto. While this technique has been applied~to expressivity
and satisfiability questions before, we show how to extend it to reduce interpolation questions about such logics to
interpolation for the mu-calculus.

*Accepted at LICS* 2015. 12 pages.

© 2015 Michael Benedikt, Balder ten Cate , and Michael Vanden Boom.