Sciweavers

Share
LOGCOM
2007

Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-free Deep Inference Calculi for S5

9 years 11 months ago
Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-free Deep Inference Calculi for S5
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. ∗NICTA is funded by the Australian Government’s Dept of Communications, Information Technology and the Arts and the Australian Research Council through Backing Australia’s Ability and the ICT Centre of Excellence program. 1
Rajeev Goré, Alwen Tiu
Added 16 Dec 2010
Updated 16 Dec 2010
Type Journal
Year 2007
Where LOGCOM
Authors Rajeev Goré, Alwen Tiu
Comments (0)
books