First-order equational logic consists of quantifier-free terms of ordinary first-order logic, with equality as the only predicate symbol.The model theory of this logic was developed into Universal algebra by Birkhoff et al.[Birkhoff, Gratzer, Cohn].It was later made into a branch of category theory by Lawvere ("algebraic theories").(1995-02-21)