No CrossRef data available.
Article contents
Completeness of MLL proof-nets w.r.t. weak distributivity
Published online by Cambridge University Press: 12 March 2014
Abstract
We examine ‘weak-distributivity’ as a rewriting rule defined on multiplicative proofstructures (so, in particular, on multiplicative proof-nets: MLL). This rewriting does not preserve the type of proof-nets, but does nevertheless preserve their correctness. The specific contribution of this paper, is to give a direct proof of completeness for : starting from a set of simple generators (proof-nets which are a n-ary ⊗ of Ց-ized axioms), any mono-conclusion MLL proof-net can be reached by rewriting (up to ⊗ and Ց associativity and commutativity).
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 2007