Proof construction and non-commutativity
Claudia Faggian · 2000
An increasing interest is directed at the extension of the \proof search as computation" paradigm, already successfully applied to Linear Logic, to a logic that is not only resource-aware but also order-sensitive.This paper is a contribution to proof search in Non-Commutative L o g i c .Our key result is to give a simple method for propagating the order structure during proof search.Such a method is general, in that it can be applied to n-ary connectives.This enables us to de ne a cluster calculus, which analyses clusters of synchronous and of asynchronous connectives in a single step, with a single n-ary rule.