equational logicFirst-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)