Proofs by induction in equational theories with constructors
initial algebra of an equational variety
extension of the Knuth-Bendix completion algorithm
scientific article; zbMATH DE number 3845044