Inducing Syntactic Cut-Elimination for Indexed Nested Sequents

R. Ramanayake*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

4 Citations (Scopus)


The key to the proof-theoretical study of a logic is a cutfree proof calculus. Unfortunately there are many logics of interest lacking suitable proof calculi. The proof formalism of nested sequents was recently generalised to indexed nested sequents in order to yield cutfree proof calculi for extensions of the modal logic K by Geach (Lemmon-Scott) axioms. The proofs of completeness and cut-elimination therein were semantical and intricate. Here we identify a subclass of the labelled sequent formalism and show that it corresponds to the indexed nested sequent formalism. This correspondence is then exploited to induce syntactic proofs for indexed nested sequents using the elegant existing proofs in the labelled sequent formalism. A larger goal of this work is to demonstrate how specialising existing proof-theoretical transformations (adapting these as required to remain within the subclass) is an alternative proof method which can alleviate the need for independent proofs from ‘scratch’ in each formalism. Moreover, such coercion can be used to induce new cutfree calculi. We demonstrate by presenting the first indexed nested sequent calculi for intermediate logics.

Original languageEnglish
Title of host publicationAutomated Reasoning
EditorsNicola Olivetti, Ashish Tiwari
Number of pages17
ISBN (Electronic)978-3-319-40229-1
ISBN (Print)978-3-319-40228-4
Publication statusPublished - 2016
Externally publishedYes
Event8th International Joint Conference, IJCAR 2016 - Coimbra, Portugal
Duration: 27-Jun-20162-Jul-2016

Publication series

NameLecture Notes in Computer Science (LNCS)


Conference8th International Joint Conference, IJCAR 2016

Cite this