Gore, Rajeev; Postniece (previously Buisman), Linda; Tiu, Alwen
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]
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.