Unification nets: canonical proof net quantifiers

DOI10.1145/3209108.3209159MaRDI QIDQ5145330zbMATH OpenOpenAlexWikidataFDO

Authors Dominic J. D. Hughes

Publication date 20 January 2021

Published in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1802.03224

zbMATH Keywords

linear logicproof netsquantifiersunification nets

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52)

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 $forallxPxvdashexistsxPx$, one per arbitrary choice of witness for $existsx$, 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) cut-free unification nets grow linearly with the size of the 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.

Recommendations

• Proof nets for unit-free multiplicative-additive linear logic
• Conflict nets
• A linear algorithm for MLL proof net correctness and sequentialization
• Canonical proof nets for classical logic
• Computer Science Logic

Cited in

(8)

• scientific article; zbMATH DE number 1377612 (Why is no real title available?)
• Proof nets, coends and the Yoneda isomorphism
• Proof nets for first-order additive linear logic
• Deep inference and expansion trees for second-order multiplicative linear logic
• Uniform Circuits, & Boolean Proof Nets
• The exponential logic of sequentialization
• A new conjecture about identity of proofs
• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)

This page was built for publication: Unification nets: canonical proof net quantifiers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145330)