Many algebraic theories are defined by conjunctions of identities,
and equational proofs are constructed by very simple rules.
This is the starting point of universal algebra, and Garrett Birkhoff
proved in his famous 1935 paper
On the structure of abstract algebras that
the following rules
are sufficient to derive all equational consequences from a
given set of identities `E`:
`Th_e.(Mod(E))` is the smallest set `C` such that
This deduction system has been implemented in many rewrite systems
and automated theorem provers.
Special cases are built into Mathematica, Maple, Derive, handheld calculators etc.
However these systems are generally not so easy to use or cost money (or both)
Can equations be manipulated in a webbrowser?
Would be useful for