## Author: Dominic Hughes

## Paper Information

Title: | Unification nets: canonical proof net quantifiers |

Authors: | Dominic Hughes |

Proceedings: | LICS PDF files |

Editors: | Anuj Dawar and Erich Grädel |

Keywords: | Linear Logic, Proof nets, First-order multiplicative linear logic, Quantifiers, Unification, Cut elimination |

Abstract: | ABSTRACT. Proof nets for MLL (unit-free Multiplicative Linear Logic) are concise graphical representations of proofs which are canonical in the sense that they abstract away syntactic redundancy such as the order of non-interacting rules. We argue that Girard’s extension to MLL1 (first-order MLL) fails to be canonical because of redundant existential witnesses, and present canonical MLL1 proof nets called unification nets without them. For example, while there are infinitely many cut-free Girard nets ∀xPx ⊢ ∃xPx, one per arbitrary choice of witness for ∃x, there is a unique cut-free unification net, with no specified witness. Redundant existential witnesses cause Girard’s MLL1 nets to suffer from severe complexity issues: (1) cut elimination is non-local and exponential-time (and -space), and (2) some sequents require exponentially large cut-free Girard nets. Unification nets solve both problems: (1) cut elimination is local and linear-time, and (2) a cut-free unification net is only a linear factor larger than its underlying sequent. Since some unification nets are exponentially smaller than corresponding Girard nets and sequent proofs, technical delicacy is required to ensure correctness is polynomial-time (quadratic). These results extend beyond MLL1 via a broader methodological insight: for canonical quantifiers, the standard parallel/sequential dichotomy of proof nets fails; an implicit/explicit witness dichotomy is also needed. Work in progress extends unification nets to additives and uses them to extend combinatorial proofs [Proofs without syntax, Annals of Mathematics, 2006] to classical first-order logic. |

Pages: | 10 |

Talk: | Jul 10 14:40 (Session 55E) |

Paper: |