The Expressive Power of Memory Logics

C. Areces, D. Figueira, S. Figueira, and S. Mera. The Expressive Power of Memory Logics. Review of Symbolic Logic, 4(2):290–318, Cambridge University Press, 2011.

Download

[pdf] 

Abstract

We investigate the expressive power of memory logics. These are modal logics extended with the possibility to store (or remove) the current node of evaluation in (or from) a memory, and to perform membership tests on the current memory. From this perspective, the hybrid logic HL(\downarrow), for example, can be thought of as a particular case of a memory logic where the memory is an indexed list of elements of the domain. This work focuses in the case where the memory is a set, and we can test whether the current node belongs to the set or not. We prove that, in terms of expressive power, the memory logics we discuss here lie between the basic modal logic and HL(\downarrow). We show that the satisfiability problem of most of the logics we cover is undecidable. The only logic with a decidable satisfiability problem is obtained by imposing strong constraints on which elements can be memorized.

BibTeX

@Article{Areces2011b,
  author =       "C. Areces and D. Figueira and S. Figueira and S.
                 Mera",
  journal =      "Review of Symbolic Logic",
  title =        "The Expressive Power of Memory Logics",
  year =         "2011",
  number =       "2",
  pages =        "290--318",
  volume =       "4",
  abstract =     "We investigate the expressive power of memory logics.
                 These are modal logics extended with the possibility to
                 store (or remove) the current node of evaluation in (or
                 from) a memory, and to perform membership tests on the
                 current memory. From this perspective, the hybrid logic
                 HL(\downarrow), for example, can be thought of as a
                 particular case of a memory logic where the memory is
                 an indexed list of elements of the domain. This work
                 focuses in the case where the memory is a set, and we
                 can test whether the current node belongs to the set or
                 not. We prove that, in terms of expressive power, the
                 memory logics we discuss here lie between the basic
                 modal logic and HL(\downarrow). We show that the
                 satisfiability problem of most of the logics we cover
                 is undecidable. The only logic with a decidable
                 satisfiability problem is obtained by imposing strong
                 constraints on which elements can be memorized.",
  doi =          "10.1017/S1755020310000389",
  publisher =    "Cambridge University Press",
  timestamp =    "2010.09.23",
  URL =          "http://dx.doi.org/10.1017/S1755020310000389",
}