Interpolation with Decidable Fixpoint Logics

A logic satisfies Craig interpolation if whenever one formula phi_1 in the logic entails another formula phi_2 in the logic, there is an intermediate formula in the logic --- one entailed by phi_1 and entailing phi_2 --- using only relations in the common signature of phi_1 and phi_2. Uniform interpolation strengthens this by requiring the interpolant to depend only on phi_1 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 recent joint work with Michael Benedikt and Balder ten Cate (to appear in LICS'15), we have taken a step towards filling these gaps, proving interpolation for a decidable fragment of least fixpoint logic called unary negation fixpoint logic (UNFP). UNFP restricts least fixpoint logic by only allowing monadic fixpoint predicates and the negation of formulas with at most one free variable. This leads to decidable satisfiability and many other nice properties, include the tree-like model property. To prove interpolation for UNFP, we show 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 Graedel, 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 modal mu-calculus.

Authors

• Michael Vanden Boom

Keywords

No keywords are indexed for this paper.