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

• This sounds like a fairly broad question. That's about 18 theorems you want to prove, so it sounds like you're basically asking 18 questions. In any case, if you want to prove those 18 theorems, one possibility is to write down 18 proofs, one for each theorem. Is that really what you're asking? I'm not clear on precisely what your question is. – D.W. Aug 19 '17 at 23:41
• @D.W. I already wrote all this proofs manually, my goal is to automatize this process, that is, construct algorithms that would proof this kind of statements by themselves taking as input previous lemmas – Rodrigo Aug 19 '17 at 23:49

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$.
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.8095682859420776, "perplexity": 435.93246835516004}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2021-10/segments/1614178374217.78/warc/CC-MAIN-20210306004859-20210306034859-00519.warc.gz"}