Equational logic is a formal system for reasoning with equations. It has simple rules for manipulating equations, based on the reflexivity, symmetry, transivity of equality and the substitution of equal terms into equations. Birkhoff’s completeness theorem says that an equation e is provable in equational logic from the equations in a set E if and only if e is true in all algebras that satisfy the equations in the set E. Related to the theorem is the fact that a class of algebras is definable as the class of all models of some set of equations if and only if the class is closed under constructing subalgebras, homomorphic images, and direct products. These results were proved by G. Birkhoff in 1935. See also equational specification, term rewriting system.