After introducing the axioms of equality, we present rewrite systems as a tool for studying equations. Two important properties of a rewrite system are termination and confluence. The Knuth-Bendix completion procedure may be used to obtain a terminating and confluent rewrite system from a set of equations. We present three special rewrite systems: ground rewrite systems, string rewrite systems, and polynomial rewrite systems. Using rewrite systems, we show how induction theorem proving is performed for recursively defined functions. Resolution can be extended with equality, and examples are given using Prover9. The chapter ends with finite model finding in first-order logic with examples from McCune’s Mace4.