Equational logic

Summary

Equational logic is the fragment of first-order logic whose statements are identities between terms and whose proofs use only equational reasoning. Its rules are reflexivity, symmetry, transitivity, replacement of equals inside an operation, and substitution of terms for variables. By Birkhoff's completeness theorem these rules derive exactly the identities that follow semantically from a given set of identities. It is the logic of algebraic manipulation, and it underlies term rewriting and automated equational reasoning.