Symmetric blocking

TitleSymmetric blocking
Publication TypeJournal Article
Year of Publication2015
AuthorsAreces, C, Orbe, E
JournalTheoretical Computer Science
AbstractWe 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: