Equational Logic

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
<ul>
<li>`E subset C`
<li>`t=t` is in `C` for all terms `t`
<li>`s=t` in `C` implies `t=s` in `C`
<li>`r=s` and `s=t` in `C` implies `r=t` in `C`
<li>`s_1=t_1` and ... and `s_n=t_n` in `C` implies 
`r(s_1,...,s_n)=r(t_1,...,t_n)` in `C`, 
where `r` is any `n`-ary term
<li>`s=t` in `C` implies `si(s)=si(t)` in `C`, 
where `si` is any substitution
</ul>

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

<ul>
<li> including interactive equational proofs in webpages
<li> collecting equational theories and their consequences on a database of webpages
<li> cataloging interpretabilities between equational theories
</ul>