Sciweavers

Share
TABLEAUX
2009
Springer

Taming Displayed Tense Logics Using Nested Sequents with Deep Inference

9 years 1 months ago
Taming Displayed Tense Logics Using Nested Sequents with Deep Inference
We consider two sequent calculi for tense logic in which the syntactic judgements are nested sequents, i.e., a tree of traditional onesided 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 ...
Rajeev Goré, Linda Postniece, Alwen Tiu
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where TABLEAUX
Authors Rajeev Goré, Linda Postniece, Alwen Tiu
Comments (0)
books