@article {414,
	title = {Symmetric blocking},
	journal = {Theoretical Computer Science},
	year = {2015},
	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.},
	author = {Carlos Areces and Ezequiel Orbe}
}