Skip navigation
Skip navigation

From display calculi to deep nested sequent calculi: Formalised for full intuitionistic linear logic

Dawson, Jeremy; Clouston, Ranald; Gore, Rajeev; Tiu, Alwen

Description

Proof theory for a logic with categorical semantics can be developed by the following methodology: define a sound and complete display calculus for an extension of the logic with additional adjunctions; translate this calculus to a shallow inference nested sequent calculus; translate this calculus to a deep inference nested sequent calculus; then prove this final calculus is sound with respect to the original logic. This complex chain of translations between the different calculi require proofs...[Show more]

CollectionsANU Research Publications
Date published: 2014
Type: Conference paper
URI: http://hdl.handle.net/1885/75302
Source: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
DOI: 10.1007/978-3-662-44602-7_20

Download

File Description SizeFormat Image
01_Dawson_From_display_calculi_to_deep_2014.pdf288.09 kBAdobe PDF    Request a copy


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  20 July 2017/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator