2015/09/10 by Etienne Lozes
Computer Science · #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.191.12
published as EPTCS 191, 2015, pp. 132-142 · In Proceedings FICS 2015, arXiv:1509.02826
arxiv created 2015/09/10 · arxiv updated 2016/08/08
In the modal mu-calculus, a formula is well-formed if each recursive variable occurs underneath an even number of negations. By means of De Morgan's laws, it is easy to transform any well-formed formula into an equivalent formula without negations -- its negation normal form. Moreover, if the formula is of size n, its negation normal form of is of the same size O(n). The full modal mu-calculus and the negation normal form fragment are thus equally expressive and concise. In this paper we extend this result to the higher-order modal fixed point logic (HFL), an extension of the modal mu-calculus with higher-order recursive predicate transformers. We present a procedure that converts a formula into an equivalent formula without negations of quadratic size in the worst case and of linear size when the number of variables of the formula is fixed.