SAT-based Decision Procedure for Analytic Pure Sequent Calculi

Speaker: Ori Lahav , 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

Public: Yes

Location: 32-G882 (reading room)

Event Type:

Room Description:

Host: Adam Chlipala, CSAIL

Contact: Adam Chlipala, adamc@csail.mit.edu

Relevant URL: http://www.cs.tau.ac.il/~orilahav/

Speaker URL: None

Speaker Photo:
None

Reminders to: seminars@csail.mit.edu, pl@csail.mit.edu

Reminder Subject: 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)

Research Areas:

Impact Areas:

See other events that are part of the PL/SE Seminar Series 2013/2014.

Created by Adam Chlipala at Thursday, January 09, 2014 at 11:05 AM.