Please use this identifier to cite or link to this item:
|Title:||The Consistency and Complexity of Multiplicative Additive System Virtual||Authors:||Horne, Ross||Keywords:||Proof theory
|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
|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|
Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.