The Consistency and Complexity of Multiplicative Additive System Virtual
Date of Issue2015-12-16
School of Computer Engineering
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.
Scientific Annals of Computer Science
© 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.