Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
435777 | Theoretical Computer Science | 2015 | 17 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Carlos Areces, Ezequiel Orbe,