Title: A Linear Time Algorithm for Automatic Generation of Multiplicative Planar Proof Nets

Abstract

Recently we have found a new linear time correctness condition for multiplicative proof nets of Linear Logic. We have given an implementation for this condition, but found a bug in the first version, although it has been fixed in the second version. The bug was subtle: we must introduce a deadlock prevention mechanism in order to fix it.

In order to confirm that the current version is correct, we would like to have a lot of test data: we need both correct MLL proof nets and MLL proof structures that are not proof nets. It is relatively easy to generate a large number of general MLL proof structures. But correct MLL proof nets are quite few among them. One approach to generate correct MLL proof nets is to apply an assignment algorithm of multiplicative links to "pre-proof structures". But this algorithm is quadratic: it is not appropriate to generate big correct MLL proof nets.

In this talk, we show that a linear time improvement of this assignment algorithm is possible in

a special class of MLL proof nets: in the planar case. This linear time algorithm has a geometric flavor and uses union-find data structures.