Unsorted Functional Translations

C. Areces and D. Gor\'in. Unsorted Functional Translations. Electronic Notes in Theoretical Computer Science, 278(0):3–16, 2011. Proceedings of the 7th Workshop on Methods for Modalities (M4M 2011)

Download

[pdf] 

Abstract

In this article we first show how the functional and the optimized functional translation from modal logic to many-sorted first-order logic can be naturally extended to the hybrid language H(@,\downarrow). The translation is correct not only when reasoning over the class of all models, but for any first-order definable class. We then show that sorts can be safely removed (i.e., without affecting the satisfiability status of the formula) for frame classes that can be defined in the basic modal language, and show a counterexample for a frame class defined using nominals.

BibTeX

@Article{Areces2011f,
  author =       "C. Areces and D. Gor{\'i}n",
  journal =      "Electronic Notes in Theoretical Computer Science",
  title =        "Unsorted Functional Translations",
  year =         "2011",
  ISSN =         "1571-0661",
  note =         "Proceedings of the 7th Workshop on Methods for
                 Modalities (M4M 2011)",
  number =       "0",
  pages =        "3--16",
  volume =       "278",
  abstract =     "In this article we first show how the functional and
                 the optimized functional translation from modal logic
                 to many-sorted first-order logic can be naturally
                 extended to the hybrid language H(@,\downarrow). The
                 translation is correct not only when reasoning over the
                 class of all models, but for any first-order definable
                 class. We then show that sorts can be safely removed
                 (i.e., without affecting the satisfiability status of
                 the formula) for frame classes that can be defined in
                 the basic modal language, and show a counterexample for
                 a frame class defined using nominals.",
  doi =          "10.1016/j.entcs.2011.10.002",
  keywords =     "Automated theorem proving",
  URL =          "http://www.sciencedirect.com/science/article/pii/S1571066111001307",
}