14
$\begingroup$

Can I prove following statements with using available automated theorem provers?

  1. $(a+b)^2=a^2+b^2+2ab$.

  2. If $ 11 \mid 2a-3b$, then $ 11 \mid 7a-5b $.

  3. If $ ax^2+bx+c=0$, then $x=\frac{-b\pm\sqrt{b^2-4ac} }{2a}$.

  4. If $a$ is even then $4a$ is even.

and so on!

I am asking this question because I just found the application of Automated theorem provers in proving theorems in logic.

Improve this question
$\endgroup$
6
  • $\begingroup$ You can certainly prove all of these (except perhaps 3, which is wrong as written) using all standard proof assistants, though it probably won't be automatic. $\endgroup$
    – Yuval Filmus
    Commented Apr 15, 2018 at 11:48
  • $\begingroup$ @YuvalFilmus. Thanks! So what kind of problems can be solved automatically? $\endgroup$
    – Math-fort
    Commented Apr 15, 2018 at 11:51
  • $\begingroup$ You can simplify expressions automatically, though this is a service provided by Computer Algebra Systems. I don't think modern proof assistants can automatically prove anything of substance, though it's better to ask the experts. $\endgroup$
    – Yuval Filmus
    Commented Apr 15, 2018 at 11:53
  • $\begingroup$ @YuvalFilmus I think that what you say is often true, in the sense that only when an automated proof method gives interesting results, we are willing to call it a part of a CAS... $\endgroup$
    – Discrete lizard ♦
    Commented Apr 15, 2018 at 14:52
  • 1
    $\begingroup$ "(a + b)^2 == a^2 + b^2 + 2ab" on WolframAlpha $\endgroup$
    – Nat
    Commented Apr 16, 2018 at 0:39

1 Answer 1

Reset to default
20
$\begingroup$

Most of your statements are elementary algebra, so these can be proved automatically by a computer algebra system (CAS), such as Maple or Mathematica.

(In case you're interested in the mathematics behind CAS, I can recommend the book Modern Computer Algebra by Joachim von zur Gathen and Jürgen Gerhard, a beautiful book, considered the 'bible' of the field)

Automated theorem proving tends to be mostly a case of doing heuristic search on a structure that represents proofs, if the proof is not one of the few cases for which there is an algorithm that can conclusively solve it. Given that this statements aren't very complicated, it is likely that an automated prover is able to 'find' a proof.

However, I think it is interesting to say a bit more about the statements for which there are nice algorithms:

Statement 3 is (a very simple case of) about roots of a (system of) polynomial equations and can be solved by finding a Gröbner basis with Buchberger's algorithm. The Gröbner basis and Buchberger's algorithm to find one are very nice tools for automated theorem proving. For example, we can even automatically prove elementary theorems in geometry by automatically transforming the problem to finding a root of a polynomial equation in a clever way!

Another interesting class of theorems are statements expressible in quantifier-free Presburger arithmetic (in particular, this arithmetic is without multiplication, so this doesn't apply to your statements), as there is an algorithm to solve all such statements, even though the algorithm is a bit slow.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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