2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2015)
July 6, 2015 to July 10, 2015
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2015.43
A logic satisfies Craig interpolation if whenever one formula ?1 in the logic entails another formula ?2 in the logic, there is an intermediate formula -- one entailed by ?1 and entailing ?2 -- using only relations in the common signature of ? and ?2. Uniform interpolation strengthens this by requiring the interpolant to depend only on ?1 and the common signature. A uniform interpolant can thus be thought of as a minimal upper approximation of a formula within a sub signature. 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 fix point logics. In this work we take a step towards filling these gaps, proving interpolation for a decidable fragment of least fix point logic called unary negation fix point 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 µ-calculus.
Interpolation, Games, Grammar, Semantics, Standards, Encoding
M. Benedikt, B. T. Cate and M. V. Boom, "Interpolation with Decidable Fixpoint Logics," 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Kyoto, Japan, 2015, pp. 378-389.