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.

CollectionsANU Research Publications
Date published: 2007
Type: Journal article
URI: http://hdl.handle.net/1885/51936
Source: Journal of Logic and Computation
DOI: 10.1093/logcom/exm026

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:  23 August 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator