FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Unique perfect matchings and proof nets

Author: Lê Thành Dũng Nguyễn

Paper Information

Title:Unique perfect matchings and proof nets
Authors:Lê Thành Dũng Nguyễn
Proceedings:FSCD Presented Papers
Editor: Helene Kirchner
Keywords:graph algorithms, linear logic, correctness criteria, complexity classes
Abstract:

ABSTRACT. This paper establishes a bridge between linear logic and mainstream graph theory, building previous work by Retoré (2003). We show that the problem of correctness for MLL+Mix proof nets is equivalent to the problem of uniqueness of a perfect matching. By applying matching theory, we obtain new results for MLL+Mix proof nets: a linear-time correctness criterion, a quasi-linear sequentialization algorithm, and a characterization of the sub-polynomial complexity of the correctness problem. We also use graph algorithms to compute the dependency relation of Bagnol et al. (2015) and the kingdom ordering of Bellin (1997), and relate them to the notion of blossom which is central to combinatorial maximum matching algorithms.

Pages:20
Talk:Jul 09 11:30 (Session 47B: Linear Logic)
Paper: