Dealing with Symmetries in Modal Tableaux

C. Areces and E. Orbe. Dealing with Symmetries in Modal Tableaux. In D. Galmiche and D. Larchey-Wendling, editors, Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Computer Science, pp. 13–27, Springer, 2013.

Download

[pdf] 

Abstract

We present a technique that is able to detect symmetries in formulas of the basic modal logic (BML). Then we introduce a modal tableaux calculus for BML with a blocking mechanism that takes advantage of symmetry information about the input formula to restrict the application of the ($\Diamond$) rule. We prove completeness of the calculus. Finally, we empirically evaluate both, the detection technique and the blocking mechanism in different modal benchmarks.

BibTeX

@InCollection{Areces2013c,
  author =       "C. Areces and E. Orbe",
  booktitle =    "Automated Reasoning with Analytic Tableaux and Related
                 Methods",
  publisher =    "Springer",
  title =        "Dealing with Symmetries in Modal Tableaux",
  year =         "2013",
  editor =       "D. Galmiche and D. Larchey-Wendling",
  pages =        "13--27",
  series =       "Lecture Notes in Computer Science",
  volume =       "8123",
  abstract =     "We present a technique that is able to detect
                 symmetries in formulas of the basic modal logic (BML).
                 Then we introduce a modal tableaux calculus for BML
                 with a blocking mechanism that takes advantage of
                 symmetry information about the input formula to
                 restrict the application of the ($\Diamond$) rule. We
                 prove completeness of the calculus. Finally, we
                 empirically evaluate both, the detection technique and
                 the blocking mechanism in different modal benchmarks.",
  owner =        "areces",
  timestamp =    "2013.06.24",
  ISBN =         "978-3-642-40536-5",
}