Mathematica 6 for the first time brings general automated theorem proving into an immediate interactive environment. Extending Mathematica's already uniquely powerful algebraic theorem-proving capabilities, Mathematica 6 introduces equational theorem proving capable of operating on industrial-scale arbitrary abstract systems of axioms or relations, and integrating theorem proving into the computational workflow.