Skip navigation
Skip navigation

Classical modal display logic in the calculus of structures and minimal cut-free deep inference calculi for S5

Gore, Rajeev; Tiu, Alwen

Description

We begin by showing how to faithfully encode the Classical Modal Display Logic (CMDL) of Wansing into the Calculus of Structures (CoS) of Guglielmi. Since every CMDL calculus enjoys cut-elimination, we obtain a cut-elimination theorem for all corresponding CoS calculi. We then show how our result leads to a minimal cut-free CoS calculus for modal logic S5. No other existing CoS calculi for S5 enjoy both these properties simultaneously.

dc.contributor.authorGore, Rajeev
dc.contributor.authorTiu, Alwen
dc.date.accessioned2015-12-10T22:20:28Z
dc.identifier.issn0955-792X
dc.identifier.urihttp://hdl.handle.net/1885/51936
dc.description.abstractWe begin by showing how to faithfully encode the Classical Modal Display Logic (CMDL) of Wansing into the Calculus of Structures (CoS) of Guglielmi. Since every CMDL calculus enjoys cut-elimination, we obtain a cut-elimination theorem for all corresponding CoS calculi. We then show how our result leads to a minimal cut-free CoS calculus for modal logic S5. No other existing CoS calculi for S5 enjoy both these properties simultaneously.
dc.publisherOxford University Press
dc.sourceJournal of Logic and Computation
dc.subjectKeywords: Computational methods; Modal analysis; Calculus of structures; Cut-free sequent calculi; Deep inference; Modal logic; Formal logic Calculus of structures; Cut-free sequent calculi; Deep inference; Display logic; Proof theory of modal logic
dc.titleClassical modal display logic in the calculus of structures and minimal cut-free deep inference calculi for S5
dc.typeJournal article
local.description.notesImported from ARIES
local.identifier.citationvolume17
dc.date.issued2007
local.identifier.absfor080203 - Computational Logic and Formal Languages
local.identifier.absfor010104 - Combinatorics and Discrete Mathematics (excl. Physical Combinatorics)
local.identifier.absfor080303 - Computer System Security
local.identifier.ariespublicationu4251866xPUB235
local.type.statusPublished Version
local.contributor.affiliationGore, Rajeev, 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.issue4
local.bibliographicCitation.startpage767
local.bibliographicCitation.lastpage794
local.identifier.doi10.1093/logcom/exm026
dc.date.updated2015-12-09T08:47:13Z
local.identifier.scopusID2-s2.0-34548396698
CollectionsANU Research Publications

Download

File Description SizeFormat Image
01_Gore_Classical_modal_display_logic_2007.pdf272.54 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