Elimination and cut-elimination in multiplicative linear logic
Logic
2022-07-25 v1 Logic in Computer Science
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\"obner bases in elimination theory.
Keywords
Cite
@article{arxiv.2207.10871,
title = {Elimination and cut-elimination in multiplicative linear logic},
author = {Daniel Murfet and William Troiani},
journal= {arXiv preprint arXiv:2207.10871},
year = {2022}
}