A New Linear Time Correctness Condition for Multiplicative Linear Logic

Abstract

In this paper, we give a new linear time correctness condition for proof nets of Multiplicative Linear Logic without units. Our approach is based on a rewriting system over trees. We have only three rewrite rules. Compared with previous linear time correctness conditions, our system is surprisingly simple and intuitively appealing.

Found an bug in the proof of the linear time claim in the second version. Adapted the algorithm in order to guarantee the linear time termination. Added an additional example