摘要: This article introduces a logical system, called BV, which extends multiplicative linear logic by noncommutative self-dual operator. extension is particularly challenging for the sequent calculus, and so far, it not achieved therein. It becomes very natural in new formalism, calculus of structures, main contribution this work. Structures are formulas subject to certain equational laws typical sequents. The structures obtained generalizing such way that top-down symmetry derivations observed, employs inference rules rewrite inside at any depth. These properties, addition allowing design yield modular proof cut elimination.
acm.org
core.ac.uk
bath.ac.uk
computational-logic.org
arxiv.org 参考文章(37)
Lutz Straßburger, Linear Logic and Noncommutativity in the Calculus of Structures pp. 1- 268 ,(2003)
Christian Retoré, Réseaux et séquents ordonnés Université Paris-Diderot - Paris VII. ,(1993)
Charles Stewart, Phiniki Stouppa, A Systematic Proof Theory for Several Modal Logics. advances in modal logic. pp. 309- 333 ,(2004)
A. Nurtazin, G. Martin, H. D. Macpherson, B. Herwig, Abrusci, VM and Ruet, P., Non-commutative logic I: the multiplicative fragment (1) 29} 64 Bridges, D., Richman, F. and Schuster, P., Linear independence without choice (1) 95} 102 Creed, P. and Truss, JK, On o-amorphous sets (2} 3) 185} 226 ,(2000)
Alessio Guglielmi, Alwen Fernanto Tiu, Steffen Hölldobler, Properties of a Logical System in the Calculus of Structures ,(2001)
Kai Brünnler, Atomic Cut Elimination for Classical Logic computer science logic. pp. 86- 97 ,(2003) , 10.1007/978-3-540-45220-1_9
Greg Restall, An Introduction to Substructural Logics ,(1999)
Christian Retoré, Pomset Logic as a Calculus of Directed Cographs INRIA. ,(1999)
Robin Milner, Communication and Concurrency ,(1989)
A Guglielmi, K Bruennler, A First Order System with Finite Choice of Premises Logos Verlag. pp. 59- 74 ,(2004)