@Article{Areces2010,
  author =       "C. Areces and D. Gor{\'i}n",
  journal =      "Journal of Applied Logic",
  title =        "Coinductive models and normal forms for modal logics
                 (or how we learned to stop worrying and love
                 coinduction)",
  year =         "2010",
  number =       "4",
  pages =        "305--318",
  volume =       "8",
  abstract =     "We present a coinductive definition of models for
                 modal logics and show that it provides a homogeneous
                 framework in which it is possible to include different
                 modal languages ranging from classical modalities to
                 operators from hybrid and memory logics. Moreover,
                 results that had to be proved separately for each
                 different language --but whose proofs were known to be
                 mere routine-- now can be proved in a general way. We
                 show, for example, that we can have a unique definition
                 of bisimulation for all these languages, and prove a
                 single invariance-under-bisimulation theorem. We then
                 use the new framework to investigate normal forms for
                 modal logics. The normal form we introduce may have a
                 smaller modal depth than the original formula, and it
                 is inspired by global modalities like the universal
                 modality and the satisfiability operator from hybrid
                 logics. These modalities can be extracted from under
                 the scope of other operators. We provide a general
                 definition of extractable modalities and show how to
                 compute extracted normal forms. As it is the case with
                 other classical normal forms --e.g., the conjunctive
                 normal form of propositional logic-- the extracted
                 normal form of a formula can be exponentially bigger
                 than the original formula, if we require the two
                 formulas to be equivalent. If we only require
                 equi-satisfiability, then every modal formula has an
                 extracted normal form which is only polynomially bigger
                 than the original formula, and it can be computed in
                 polynomial time.",
  keywords =     "Modal logics; Hybrid logics; Normal forms; Modal
                 depth",
  publisher =    "Elsevier",
}