We consider various classes of algebras obtained by expanding idempotent semirings with meet, residuals and Kleene-*. An investigation of congruence properties (e-permutability, e-regularity, congruence distributivity) is followed by a section on algebraic Gentzen systems for proving inequalities in idempotent semirings, in residuated lattices, and in (residuated) Kleene lattices (with cut). Finally we define (one-sorted) residuated Kleene lattices with tests to complement two-sorted Kleene algebras with tests.

We will give here a purely algebraic proof of the cut elimination theorem for various sequent systems. Our basic idea is to introduce mathematical structures, called Gentzen structures, for a given sequent system without cut, and then to show the completeness of the sequent system without cut with respect to the class of algebras for the sequent system with cut, by using the quasi-completion of these Gentzen structures. It is shown that the quasi-completion is a generalization of the MacNeille completion. (...) Moreover, the finite model property is obtained for many cases, by modifying our completeness proof. This is an algebraic presentation of the proof of the finite model property discussed by Lafont [12] and Okada-Terui [17]. (shrink)