Abstract
Quantitative Equational Logic, or "QEL" for short, is a proof system which extends Birkhoff's equational logic. QEL is used to reason about quantitative algebras, and was shown to be complete for the defined semantics. While classical equational logic is known to be undecidable, I will give a sketch of the proof that all of the "other" content of QEL is decidable.