ABSTRACT

The paper is mainly concerned with the extension of proof-nets to additives, for which the best known solution is presented. It proposes two cut-elimination procedures, the lazy one being in linear time. The solution is shown to be compatible with quantifiers, and the structural rules of exponentials are also accommodated.