Equational logic was developed over the years (beginning in the early 1980's) by researchers in the formal development of programs, who felt a need for an effective style of manipulation, of calculation. Involved were people like Roland Backhouse, Edsger W. Dijkstra, Wim H.J. Feijen, David Gries, Carel S. Scholten, and Netty van Gasteren. Wim Feijen is responsible for important details of the proof format.

The axioms are similar to those use by Dijkstra and Scholten in their monograph Predicate calculus and program semantics (Springer Verlag, 1990), but our order of presentation is slightly different.

In their monograph, Dijkstra and Scholten use the three
inference rules
Leibniz, Substitution, and
Transitivity. However, Dijkstra/Scholten system is not a logic, as
logicians use the word. Some of their manipulations are based on the
meanings of the terms involved, and not on clearly presented
syntactical rules of manipulation. The first attempt at making a real
logic out of it appeared in
*A Logical Approach to Discrete Math*.
However, inference rule
Equanimity is missing there, and the definition of theorem is
contorted to account for it. The introduction of Equanimity and its
use in the proof format is due to Gries and Schneider. It is used,
for example, in the
proofs
of soundness and completeness,
and it will appear in the second edition of
*A Logical Approach to Discrete Math*.