Elimination and Cut-Elimination in Multiplicative Linear Logic

Introduction

Motivation: The Canonical Detour

The Ideal of a Proof

Reduction

Elimination Theory

Buchberger’s Algorithm

Monomial Orders

Main Theorems

Conclusion

Geometry of Interaction: Multiplicatives