Elimination and cut-elimination in multiplicative linear logic
Daniel Murfet, William Anthony Troiani · arXiv (Cornell University) · 2022
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.