Abstract: Bill McCune produced the program EQP that deals with first order logic formulas and in 1996 managed to solve Robbins’ Conjecture. This very powerful tool reduces to triviality any result that can be obtained by encoding the assumptions and the goals. The next step was to turn the program into a genuine assistant for the working mathematician: find ways to help the prover with proofs; reduce the lengths of the automatic proofs to better crack them;  solve problems in higher order logic; devise tools that autonomously prove results of a given type, etc.

In this talk we are going to show some of the tools and strategies we have been producing. There will be real illustrations of theorems obtained for groups, loops, semigroups, logic algebras, lattices and generalizations, quandles, and many more.