Bounded Sequent Calculi for Non-classical Logics via Hypersequents

Agata Ciabattoni; Timo Lang; Revantha Ramanayake

doi:10.1007/978-3-030-29026-9_6

Bounded Sequent Calculi for Non-classical Logics via Hypersequents

Agata Ciabattoni^*, Timo Lang, Revantha Ramanayake

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

5 Citations (Scopus)

Abstract

Using substructural and modal logics as case studies, a uniform method is presented for transforming cut-free hypersequent proofs into sequent calculus proofs satisfying relaxations of the subformula property. As a corollary we prove decidability for a large class of commutative substructural logics with contraction and mingle, and get a simple syntactic proof of a well known result: the sequent calculus for

Original language	English
Title of host publication	Automated Reasoning with Analytic Tableaux and Related Methods
Editors	Serenella Cerrito, Andrei Popescu
Publisher	Springer
Pages	94-110
Number of pages	17
ISBN (Electronic)	978-3-030-29026-9
ISBN (Print)	978-3-030-29025-2
DOIs	https://doi.org/10.1007/978-3-030-29026-9_6
Publication status	Published - 2019
Externally published	Yes
Event	28th International Conference, TABLEAUX 2019 - London, United Kingdom Duration: 3-Sept-2019 → 5-Sept-2019

Conference

Conference	28th International Conference, TABLEAUX 2019
Country/Territory	United Kingdom
City	London
Period	03/09/2019 → 05/09/2019

Access to Document

10.1007/978-3-030-29026-9_6

Handle.net

Persistent link

Embargoed Document

Bounded Sequent Calculi for Non-classical Logics via Hypersequents
Final publisher's version, 447 KB
Request copy

Cite this

@inproceedings{f50158afa7dc4a86b378bc3d072ec19e,

title = "Bounded Sequent Calculi for Non-classical Logics via Hypersequents",

abstract = "Using substructural and modal logics as case studies, a uniform method is presented for transforming cut-free hypersequent proofs into sequent calculus proofs satisfying relaxations of the subformula property. As a corollary we prove decidability for a large class of commutative substructural logics with contraction and mingle, and get a simple syntactic proof of a well known result: the sequent calculus for ",

author = "Agata Ciabattoni and Timo Lang and Revantha Ramanayake",

year = "2019",

doi = "10.1007/978-3-030-29026-9_6",

language = "English",

isbn = "978-3-030-29025-2",

pages = "94--110",

editor = "Cerrito, {Serenella } and Popescu, {Andrei }",

booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods",

publisher = "Springer",

note = "28th International Conference, TABLEAUX 2019 ; Conference date: 03-09-2019 Through 05-09-2019",

}

Bounded Sequent Calculi for Non-classical Logics via Hypersequents. / Ciabattoni, Agata; Lang, Timo; Ramanayake, Revantha.
Automated Reasoning with Analytic Tableaux and Related Methods. ed. / Serenella Cerrito; Andrei Popescu. Springer, 2019. p. 94-110.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Bounded Sequent Calculi for Non-classical Logics via Hypersequents

AU - Ciabattoni, Agata

AU - Lang, Timo

AU - Ramanayake, Revantha

PY - 2019

Y1 - 2019

N2 - Using substructural and modal logics as case studies, a uniform method is presented for transforming cut-free hypersequent proofs into sequent calculus proofs satisfying relaxations of the subformula property. As a corollary we prove decidability for a large class of commutative substructural logics with contraction and mingle, and get a simple syntactic proof of a well known result: the sequent calculus for

AB - Using substructural and modal logics as case studies, a uniform method is presented for transforming cut-free hypersequent proofs into sequent calculus proofs satisfying relaxations of the subformula property. As a corollary we prove decidability for a large class of commutative substructural logics with contraction and mingle, and get a simple syntactic proof of a well known result: the sequent calculus for

U2 - 10.1007/978-3-030-29026-9_6

DO - 10.1007/978-3-030-29026-9_6

M3 - Conference contribution

SN - 978-3-030-29025-2

SP - 94

EP - 110

BT - Automated Reasoning with Analytic Tableaux and Related Methods

A2 - Cerrito, Serenella

A2 - Popescu, Andrei

PB - Springer

T2 - 28th International Conference, TABLEAUX 2019

Y2 - 3 September 2019 through 5 September 2019

ER -