Construction of retractile proof structures

ABSTRACT. In this work we present a paradigm of focusing proof search based on an incremental construction of ''correct'' (i.e, sequentializable) proof structures of the pure (units free) multiplicative and additive fragment of linear logic (J.-Y. Girard, 1987). The correctness of proof construction steps (or expansion steps) is ensured by means of a system of graph retraction rules; this graph rewriting system is shown to be convergent, that is, terminating and confluent. The proposed proof construction follows a specific - ''parsimonious'', indeed - retraction strategy that, at each expansion attempt, allows to take into account (abstract) graphs that are ''smaller'' (w.r.t. the size) than the starting proof structures.