A Gentzen system for involutive residuated lattices

We establish a cut-free Gentzen system for involutive residuated lattices and provide an algebraic proof of completeness. As a result we conclude that the equational theory of involutive residuated lattices is decidable. The connection to noncommutative linear logic is outlined. Received July 22, 2004; accepted in final form July 19, 2005.