SAT-Based Decision Procedure for Analytic Sequent Calculi

Опубликовано 27 июля 2016, 19:31

We present a general reduction of the derivability problem in a given analytic sequent calculus to SAT. This reduction generalizes of the one in [Gurevich and Beklemishev 2012] for the propositional fragment of Primal Logic, and it applies to a wide family of sequent calculi for propositional non-classical logics. Next, we study the extension of such calculi with simple modal operators, of a similar nature to the quotations employed in Primal Logic. We modify the reduction to SAT for these extended calculi, based on general (possibly, non-deterministic) Kripke-style semantics. In particular, it follows that Primal Logic with quotations can be decided in linear time by applying an off-the-shelf HORN-SAT solver. In addition, we point out several possible extensions of Primal Logic that still allow a linear time decision procedure. The talk is based on a work in-progress together with Yoni Zohar (also from TAU).