Please use this identifier to cite or link to this item: https://hdl.handle.net/10356/81581
Title: The Consistency and Complexity of Multiplicative Additive System Virtual
Authors: Horne, Ross
Keywords: Proof theory
Deep inference
Non-commutative logic
Issue Date: 2015
Source: Horne, R. (2015). The Consistency and Complexity of Multiplicative Additive System Virtual. Scientific Annals of Computer Science, 25(2), 245-316.
Series/Report no.: Scientific Annals of Computer Science
Abstract: This paper investigates the proof theory of multiplicative additive system virtual (MAV). MAV combines two established proof calculi: multiplicative additive linear logic (MALL) and basic system virtual (BV). Due to the presence of the self-dual non-commutative operator from BV, the calculus MAV is de fined in the calculus of structures - a generalisation of the sequent calculus where inference rules can be applied in any context. A generalised cut elimination result is proven for MAV, thereby establishing the consistency of linear implication defined in the calculus. The cut elimination proof involves a termination measure based on multisets of multisets of natural numbers to handle subtle interactions between operators of BV and MAV. Proof search in MAV is proven to be a PSPACE-complete decision problem. The study of this calculus is motivated by observations about applications in computer science to the veri cation of protocols and to querying.
URI: https://hdl.handle.net/10356/81581
http://hdl.handle.net/10220/40261
ISSN: 1843-8121
DOI: http://dx.doi.org/10.7561/SACS.2015.2.245
Rights: © 2015 Scientic Annals of Computer Science. This paper was published in Scientific Annals of Computer Science and is made available as an electronic reprint (preprint) with permission of Scientific Annals of Computer Science. The published version is available at: [http://dx.doi.org/10.7561/SACS.2015.2.245]. One print or electronic copy may be made for personal use only. Systematic or multiple reproduction, distribution to multiple locations via electronic or other means, duplication of any material in this paper for a fee or for commercial purposes, or modification of the content of the paper is prohibited and is subject to penalties under law.
Fulltext Permission: open
Fulltext Availability: With Fulltext
Appears in Collections:SCSE Journal Articles

Files in This Item:
File Description SizeFormat 
XXV2_2.pdf620.4 kBAdobe PDFThumbnail
View/Open

Google ScholarTM

Check

Altmetric

Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.