A non-commutative extension of MELL
A Guglielmi, L Straßburger - … , LPAR 2002 Tbilisi, Georgia, October 14–18 …, 2002 - Springer
Logic for Programming, Artificial Intelligence, and Reasoning: 9th …, 2002•Springer
We extend multiplicative exponential linear logic (M EL) L by a non-commutative, self-dual
logical operator. The extended system, called NEL is defined in the formalism of the calculus
of structures, which is a generalisation of the sequent calculus and provides a more refined
analysis of proofs. We should then be able to extend the range of applications of MEL, L by
modelling a broad notion of sequentiality and providing new properties of proofs. We show
some proof theoretical results: decomposition and cut elimination. The new operator …
logical operator. The extended system, called NEL is defined in the formalism of the calculus
of structures, which is a generalisation of the sequent calculus and provides a more refined
analysis of proofs. We should then be able to extend the range of applications of MEL, L by
modelling a broad notion of sequentiality and providing new properties of proofs. We show
some proof theoretical results: decomposition and cut elimination. The new operator …
Abstract
We extend multiplicative exponential linear logic(M EL)L by a non-commutative, self-dual logical operator. The extended system, called NEL is defined in the formalism of the calculus of structures, which is a generalisation of the sequent calculus and provides a more refined analysis of proofs. We should then be able to extend the range of applications of M E L,L by modelling a broad notion of sequentiality and providing new properties of proofs. We show some proof theoretical results: decomposition and cut elimination. The new operator represents a significant challenge: to get our results we use here for the first time some novel techniques, which constitute a uniform and modular approach to cut elimination, contrary to what is possible in the sequent calculus.
Springer
以上显示的是最相近的搜索结果。 查看全部搜索结果