Scientific Annals of Computer Science | |
The Consistency and Complexity of Multiplicative Additive System Virtual | |
article | |
R. Horne1  | |
[1] School of Computer Engineering, Nanyang Technological University, Singapore and Institute of Computer Science | |
关键词: proof theory; deep inference; non-commutative logic; | |
DOI : 10.7561/SACS.2015.2.245 | |
来源: Alexandru Ioan Cuza University of Iasi | |
【 摘 要 】
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.
【 授权许可】
CC BY-ND
【 预 览 】
Files | Size | Format | View |
---|---|---|---|
RO202106050001101ZK.pdf | 620KB | download |