The consistency and complexity of multiplicative additive system virtual

Research output: Contribution to journalArticlepeer-review

13 Citations (Scopus)


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 defined 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 verification of protocols and to querying.
Original languageEnglish
Pages (from-to)245-316
Number of pages72
JournalScientific Annals of Computer Science
Issue number2
Publication statusPublished - 1 Oct 2015


  • proof theory
  • deep inference
  • non-commutative logic


Dive into the research topics of 'The consistency and complexity of multiplicative additive system virtual'. Together they form a unique fingerprint.

Cite this