Symmetric blocking
| Title | Symmetric blocking |
| Publication Type | Journal Article |
| Year of Publication | 2015 |
| Authors | Areces, C, Orbe, E |
| Journal | Theoretical Computer Science |
| 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. |
Work Package:
WP2
