TY - GEN

T1 - Taming displayed tense logics using nested sequents with deep inference

AU - Goré, Rajeev

AU - Postniece, Linda

AU - Tiu, Alwen

PY - 2009

Y1 - 2009

N2 - We consider two sequent calculi for tense logic in which the syntactic judgements are nested sequents, i.e., a tree of traditional one-sided sequents built from multisets of formulae. Our first calculus SKt is a variant of Kashima's calculus for Kt, which can also be seen as a display calculus, and uses "shallow" inference whereby inference rules are only applied to the top-level nodes in the nested structures. The rules of SKt include certain structural rules, called "display postulates", which are used to bring a node to the top level and thus in effect allow inference rules to be applied to an arbitrary node in a nested sequent. The cut elimination proof for SKt uses a proof substitution technique similar to that used in cut elimination for display logics. We then consider another, more natural, calculus DKt which contains no structural rules (and no display postulates), but which uses deep-inference to apply inference rules directly at any node in a nested sequent. This calculus corresponds to Kashima's S2Kt, but with all structural rules absorbed into logical rules. We show that SKt and DKt are equivalent, that is, any cut-free proof of SKt can be transformed into a cut-free proof of DKt, and vice versa. We consider two extensions of tense logic, Kt.S4 and S5, and show that this equivalence between shallow- and deep-sequent systems also holds. Since deep-sequent systems contain no structural rules, proof search in the calculi is easier than in the shallow calculi. We outline such a procedure for the deep-sequent system DKt and its S4 extension.

AB - We consider two sequent calculi for tense logic in which the syntactic judgements are nested sequents, i.e., a tree of traditional one-sided sequents built from multisets of formulae. Our first calculus SKt is a variant of Kashima's calculus for Kt, which can also be seen as a display calculus, and uses "shallow" inference whereby inference rules are only applied to the top-level nodes in the nested structures. The rules of SKt include certain structural rules, called "display postulates", which are used to bring a node to the top level and thus in effect allow inference rules to be applied to an arbitrary node in a nested sequent. The cut elimination proof for SKt uses a proof substitution technique similar to that used in cut elimination for display logics. We then consider another, more natural, calculus DKt which contains no structural rules (and no display postulates), but which uses deep-inference to apply inference rules directly at any node in a nested sequent. This calculus corresponds to Kashima's S2Kt, but with all structural rules absorbed into logical rules. We show that SKt and DKt are equivalent, that is, any cut-free proof of SKt can be transformed into a cut-free proof of DKt, and vice versa. We consider two extensions of tense logic, Kt.S4 and S5, and show that this equivalence between shallow- and deep-sequent systems also holds. Since deep-sequent systems contain no structural rules, proof search in the calculi is easier than in the shallow calculi. We outline such a procedure for the deep-sequent system DKt and its S4 extension.

UR - http://www.scopus.com/inward/record.url?scp=77956312366&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-02716-1_15

DO - 10.1007/978-3-642-02716-1_15

M3 - Conference contribution

SN - 3642027156

SN - 9783642027154

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 189

EP - 204

BT - Automated Reasoning with Analytic Tableaux and Related Methods - 18th International Conference, TABLEAUX 2009, Proceedings

T2 - 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009

Y2 - 6 July 2009 through 10 July 2009

ER -