5
$\begingroup$

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.

Welder-Inox-SMT solver stack

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:

enter image description here

And here you have the kind of goals I would like to proof automatically:

enter image description here

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.

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – D.W. Aug 19 '17 at 23:41
  • $\begingroup$ @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 $\endgroup$ – Javier Aug 19 '17 at 23:49
3
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.