Name
Abstract | ||
|---|---|---|
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 phi into an equivalent formula without negations - the negation normal form of phi. Moreover, if phi is of size n, the negation normal form of phi 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-ordermodal 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 of size n into an equivalent formula without negations of size O(n(2)) in the worst case and O(n) when the number of variables of the formula is fixed. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.4204/EPTCS.191.12 | ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE |
DocType | Issue | ISSN |
Journal | 191 | 2075-2180 |
Citations | PageRank | References |
3 | 0.40 | 10 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Étienne Lozes | 1 | 121 | 14.32 |