Contractible Proof Structures
Roberto Maieli · Iris (Roma Tre University) · 2013
We present an application of a confluent rewriting system, based on local deformation steps (contrac- tions) of special graphs (proof structures), to the proof construction paradigm of the pure multiplicative and additive fragment of linear logic. This system allows to detect, among proof structures, those (correct) ones that correspond to very compact (bipolar and focussing) derivations of the sequent calculus of linear logic. In particular, a correct proof structure, called transitory net, is a proof structure that retracts to a special invariant graph, called normal form (i.e., a set of single nodes).