Proof Construction and Non Commutativity: a Cluster Calculus

Claudia Faggian

To appear at the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000


An increasing amount of interest has been directed at the extension of the "proof-search as computation" paradigm, successfully applied to Linear logic, to a logic not only resources-aware but also order-sensitive. This paper is a contribution to proof-search in Non Commutative Logic.

We define a "cluster" calculus, where packs of synchronous and packs of asynchronous connectives are decomposed (bottom-up) at once, as single n-ary connectives. We give a homogeneous "coherence condition" on the partition of the context of synchronous connectives and reach optimal solutions to the problem of associating orders to the premises of a rule through an opportune restriction of the order structure associated to the conclusion.