SAT-Based Decision Procedure for Analytic Sequent Calculi

  • Ori Lahav | Tel Aviv University

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).

Speaker Details

Ori Lahav is completing his PhD in computer science at Tel Aviv University under the supervision of Prof. Arnon Avron. In his research, Ori explored syntax-semantics connections in general families of Gentzen-type proof calculi for non-classical logics. In particular, he studied semantic characterizations of proof-theoretic properties in sequent systems, such as the subformula property and cut-elimination.

Series: Microsoft Research Talks