SAT-based Decision Procedure for Analytic Pure Sequent Calculi
, Tel Aviv University
Date: Friday, January 17, 2014
Time: 4:00 PM to 5:15 PM Note: all times are in the Eastern Time Zone
Location: 32-G882 (reading room)
Host: Adam Chlipala, CSAIL
Contact: Adam Chlipala, email@example.com
Relevant URL: http://www.cs.tau.ac.il/~orilahav/
Speaker URL: None
TALK: SAT-based Decision Procedure for Analytic Pure Sequent Calculi
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 the 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.
Based on a work in-progress together with Yoni Zohar (also from Tel Aviv University)
Created by Adam Chlipala at Thursday, January 09, 2014 at 11:05 AM.