We identify a wide family of analytic sequent calculi for propositional non-classical logics whose derivability problem can be uniformly reduced to SAT. The proposed reduction is based on interpreting these calculi using non-deterministic semantics. Its time complexity is polynomial, and, in fact, linear for a useful subfamily. We further study an extension of such calculi with Next operators, and show that this extension preserves analyticity and is subject to a similar reduction to SAT. A particular interesting instance of these results is a HORNSAT-based linear-time decision procedure for Gurevich and Neeman's primal infon logic and several natural extensions of it. © 2014 Springer International Publishing Switzerland.
CITATION STYLE
Lahav, O., & Zohar, Y. (2014). SAT-Based decision procedure for analytic pure sequent calculi. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8562 LNAI, pp. 76–90). Springer Verlag. https://doi.org/10.1007/978-3-319-08587-6_6
Mendeley helps you to discover research relevant for your work.