Procedure to automatically solve field theorems in a SMT solver

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.

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).

StackExchange Computer Science Q#79893, answer score: 3