From a computer algebra library to a system with an equational prover

We consider joining to our computer algebra library a certain prover based on the TRW machine with an order-sorted algebraic specification language for input. A resource distribution approach helps to automate the proof tactics. Inductive reasoning is organized through adding of equalities. The unfailing Knuth-Bendix completion combined with special completion for the Boolean terms enables proofs in predicate logic. The question is how to develop further a language for equational reasoning/computing, the prover library and special provers to make possible the solution of more substantial problems than the ones mentioned in the examples.