2022•arXiv (Cornell University)Open access
Elimination and cut-elimination in multiplicative linear logic
Daniel Murfet, William Anthony Troiani
Open full text 0 citations
Abstract
We associate to every proof structure in multiplicative linear logic an ideal which represents the logical content of the proof as polynomial equations. We show how cut-elimination in multiplicative proof nets corresponds to instances of the Buchberger algorithm for computing Gröbner bases in elimination theory.
Open-access reader