Dealing with Symmetries in Modal Tableaux

Areces, C. and Orbe, E.. 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: (download)

@INCOLLECTION{arec:deal13,
  author = {Areces, C. and Orbe, E.},
  title = {Dealing with Symmetries in Modal Tableaux},
  booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods},
  publisher = {Springer},
  year = {2013},
  editor = {D. Galmiche and D. Larchey-Wendling},
  volume = {8123},
  series = {Lecture Notes in Computer Science},
  pages = {13--27},
  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}
}

Generated by bib2html.pl (written by Patrick Riley) on Sun Oct 02, 2016 17:05:49