论文标题
乘法线性逻辑中的消除和切割
Elimination and cut-elimination in multiplicative linear logic
论文作者
论文摘要
我们将乘法线性逻辑中的每个证明结构都关联为理想，它表示证明的逻辑内容为多项式方程。我们展示了乘法证明网中的切割量如何对应于淘汰理论中计算Gröbner基础的Buchberger算法的实例。
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.
