This paper provides a reasonably good summary of the current state of research into unification in Boolean rings. Beginning with the essentials on Boolean rings, the paper proceeds to describe two algorithms for Boolean unification. A discussion of the algebraic structure of the Boolean ring in terms of an orthogonal normal form follows in order that the problem of finding particular solutions of Boolean equations can be investigated. The paper concludes with a description of the methods needed to unify terms in the unquantified predicate calculus considered as a Boolean ring under exclusive or and conjunction. The authors present applications to first-order theorem proving.