Skip navigation
Skip navigation

Taming displayed tense logics using nested sequents with deep inference

Gore, Rajeev; Postniece (previously Buisman), Linda; Tiu, Alwen

Description

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]

dc.contributor.authorGore, Rajeev
dc.contributor.authorPostniece (previously Buisman), Linda
dc.contributor.authorTiu, Alwen
dc.coverage.spatialOslo Norway
dc.date.accessioned2015-12-07T22:19:15Z
dc.date.createdJuly 6-10 2009
dc.identifier.isbn9783642027154
dc.identifier.urihttp://hdl.handle.net/1885/19240
dc.description.abstractWe 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.
dc.publisherSpringer
dc.relation.ispartofseriesInternational Conference on Analytic Tableaux and Related Methods (TABLEAUX 2009)
dc.sourceProceedings of International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2009)
dc.subjectKeywords: Cut elimination; Deep inference; Display logic; Inference rules; Logical rules; Multi-sets; Nested structures; Proof search; Sequent calculus; Structural rules; Automata theory; Biomineralization; Differentiation (calculus); Pathology; Problem solving; Ca
dc.titleTaming displayed tense logics using nested sequents with deep inference
dc.typeConference paper
local.description.notesImported from ARIES
local.description.refereedYes
dc.date.issued2009
local.identifier.absfor010107 - Mathematical Logic, Set Theory, Lattices and Universal Algebra
local.identifier.absfor080203 - Computational Logic and Formal Languages
local.identifier.ariespublicationu4607519xPUB7
local.type.statusPublished Version
local.contributor.affiliationGore, Rajeev, College of Engineering and Computer Science, ANU
local.contributor.affiliationPostniece (previously Buisman), Linda, College of Engineering and Computer Science, ANU
local.contributor.affiliationTiu, Alwen, College of Engineering and Computer Science, ANU
local.description.embargo2037-12-31
local.bibliographicCitation.startpage189
local.bibliographicCitation.lastpage204
local.identifier.doi10.1007/978-3-642-02716-1_15
dc.date.updated2016-02-24T11:13:56Z
local.identifier.scopusID2-s2.0-77956312366
CollectionsANU Research Publications

Download

File Description SizeFormat Image
01_Gore_Taming_displayed_tense_logics_2009.pdf222.04 kBAdobe PDF    Request a copy


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator