LP, the Larch Prover -- Proofs of operator theories
LP permits users to prove operator theories as well as
assert them. Proving that an operator + is commutative involves
proving a single subgoal consisting of the formula x + y = y + x. Proving
that an operator is associative-commutative involves proving an additional
subgoal consisting of the formula x + (y + z) = (x + y) + z.