Categorical equational systems : algebraic models and equational reasoning

This work develops a sound logical deduction system, called Term Equational Logic (TEL), for equational reasoning about algebras of TESs, and gives an internal completeness result, from which together with the explicit construction of free algeBRas one can typically synthesize sound and complete rewriting-style equational logics.