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 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",...[Show more]
|Collections||ANU Research Publications|
|Source:||Proceedings of International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2009)|
|01_Gore_Taming_displayed_tense_logics_2009.pdf||222.04 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.