Inducing Syntactic Cut-Elimination for Indexed Nested Sequents

R. Ramanayake*

*Bijbehorende auteur voor dit werk

OnderzoeksoutputAcademicpeer review

4 Citaten (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.

Originele taal-2English
TitelAutomated Reasoning
RedacteurenNicola Olivetti, Ashish Tiwari
Aantal pagina's17
ISBN van elektronische versie978-3-319-40229-1
ISBN van geprinte versie978-3-319-40228-4
StatusPublished - 2016
Extern gepubliceerdJa
Evenement8th International Joint Conference, IJCAR 2016 - Coimbra, Portugal
Duur: 27-jun-20162-jul-2016

Publicatie series

NaamLecture Notes in Computer Science (LNCS)


Conference8th International Joint Conference, IJCAR 2016

Citeer dit