Symmetric blocking

C. Areces and E. Orbe. Symmetric blocking. Theoretical Computer Science, 606:25–41, Elsevier, 2015.

Download

[pdf] 

Abstract

We present three different techniques that use information about symmetries detected in the input formula to block the expansion of diamonds in a modal tableau. We show how these blocking techniques can be included in a standard tableaux calculus for the basic modal logic, and prove that they preserve soundness and completeness. We empirically evaluate these blocking mechanisms in different modal benchmarks.

BibTeX

@Article{Areces2015e,
  author =       "C. Areces and E. Orbe",
  journal =      "Theoretical Computer Science",
  title =        "Symmetric blocking",
  year =         "2015",
  pages =        "25--41",
  volume =       "606",
  abstract =     "We present three different techniques that use
                 information about symmetries detected in the input
                 formula to block the expansion of diamonds in a modal
                 tableau. We show how these blocking techniques can be
                 included in a standard tableaux calculus for the basic
                 modal logic, and prove that they preserve soundness and
                 completeness. We empirically evaluate these blocking
                 mechanisms in different modal benchmarks.",
  owner =        "areces",
  publisher =    "Elsevier",
  timestamp =    "2015.09.01",
}