The Consistency and Complexity of Multiplicative Additive System Virtual
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...
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
2016
|
| Subjects: | |
| Online Access: | https://hdl.handle.net/10356/81581 http://hdl.handle.net/10220/40261 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Institution: | Nanyang Technological University |
| Language: | English |
| Summary: | 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. |
|---|