Proof Construction and Non Commutativity: a Cluster Calculus
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
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.