I'm working with the Welder proof assistant. Basically, this system uses basic inference rules to modify the goal one wants to proof. At a latter step, the modified goals are passed to a SMT solver to see if it can prove them. I have already written automatic induction tactics that generate by themselves the induction hypothesis. Now I want to write a procedure that will allow me to solve automatically the following problem:Proof basic field theory statements using the axioms of group and  already proved lemmas.Could you describe successful approaches to solve this problem?Here I leave you the kind of axioms that I want to use:And here you have the kind of goals I would like to proof automatically:The idea is that the procedure is given the theorem, a list of lemmas (axioms of other proved theorems) and is able to deduce by itself the goal.
Procedure to automatically solve field theorems in a SMT solver
logic;proof assistants;automated theorem proving
All of the theorems you want to prove (except uniqueAddNeutral) are of the form $\forall x . \phi(x)$ where $\phi(x)$ is quantifier-free.  Herbrandization is typically the first step towards proving those theorems: replace $x$ with an arbitrary constant $c$, with no assumptions made about $x$, and prove $\phi(c)$ holds without making any assumptions about $c$.The theorems you want to prove are simple enough that exhaustive search over candidate proof trees might suffice to find a proof.  At each step, you apply one of the axioms, instantiating the universally-quantified variables in the axiom with appropriately chosen values.  You have to choose which axiom to apply and how to instantiate the variables; typically you instantiate each variable in the axiom with one of the subexpressions in the current expression/goal, so there are only finitely many choices at each step, and you can simply exhaustively search over all possibilities (up to a given size/depth).