How to start with automated theorem proving?

logic computer-science reference-request soft-question automated-theorem-proving

I'm interested in this question, but I'm not going to list my knowledge/demands but rather gear it to more general purpose; so the first thing concerns the prerequisites, i.e.

How much theoretical knowledge (mathematical logic, programming and other) should one have prior to engaging with automated theorem proving (ATP)? Are there any fields of mathematical logic that aren't necessary prerequisites but still provide a deeper insight into ATP?

After the prerequisities are done, one just needs to dive in:

How does one start with ATP? Are there any books, lecture notes, which explain the crucial concepts? After one is done with the general idea of ATP, how does one proceed to do it?

However, one might be concerned (at least that's what my main concern is) about the many different theorem-provers; how does one choose, and is there a chance that if one chooses the wrong one, they are going to be stuck with obsolete knowledge (even in terms of pure mathematics). In other words

How concerned should one be with "aging" of the theorem-provers? Are there any language-agnostic approaches?


Solution 1:

Besides @dtldarek suggestions, I would like to draw your attention to

Mizar: a project aiming to formalize all of mathematics. It has been going on since the 70's so it is not likely to disappear any time soon. To learn and participate in the project you just need to study some basic (standard) logic/theory of demonstration and to look at the axioms of Tarsky-Grothendieck set theory (set theory with universes). http://en.wikipedia.org/wiki/Mizar_system

The Japanese mirror site: http://markun.cs.shinshu-u.ac.jp/mirror/mizar/

If you manage to formalize a new proof in Mizar (even of a well-known theorem), your result may be published in their peer-reviewed journal.

However if you really are interested in ATP, that is in systems which discover a proof by themselves (or with very little human help), than my experience and suggestion goes to Theorema a project developed in Austria. In order to use Theorema you need to use the commercial software Mathematica by Wolfram Research

http://www.wolfram.com/products/

Mathematica is one the (2 or 3) most powerful computer algebra systems (CAS) available today. I would recommend you to become familiar with a CAS as soon as possible, basically for the same reasons that I would recommend a would-be journalist or writer to become proficient in using a word-processor. Fortunately student or home editions of Mathematica are not too expensive (100-300$ range). Please note that these versions are exactly as powerful as the full commercial version

Theorema is a (free) add-on to Mathematica.

The technology behind Theorema is very advanced (for example you can create new mathematical notation, the proofs are generated and explained in plain English, etc.), but it seems (to me, at least) that the system is not widely used outside its own developing team. Nevertheless studying and using it is fascinating and well-worth.

http://www.risc.jku.at/research/theorema/description/

Theorema can be requested from this page:

http://www.risc.jku.at/research/theorema/software/

Solution 2:

  1. I never developed an ATP, just did some related stuff, so an answer form someone who did will be infinitely better. Still, I think I might help just a bit.

  2. It greatly depends what would you want to do with it (the theorem prover).

  3. To develop something entirely new that really works you would need a whole team of experienced people for few years (compare who did what in Coq). That kind of software is very hard to write and requires a lot of programming skill. Still, it's not a lost case yet: to play with developing such a tool may be a valid exercise, even if it is a hard one.

  4. I can't help you with any books (Google seems to spit out many related things, though), because I learned it by trial and error. On the other hand I can say that learning to use existing one (if you don't know some yet) might be a good idea. For that purpose I recommend Coq -- it is not exactly what you want (proof assistant instead of theorem prover), but has nice, large community and (from my perspective) a lot of people use/know it, I would say that it is kind of standard.

  5. I can't help you with aging of theorem provers -- I'm not old enough :-) However, I can say how I deal with aging of programming languages (and theorem provers are much like specialized programming languages interpreters), every some time there is a new feature you would want to have, so if any of available tools support it, go ahead, if not -- develop(expand an existing app?) your own (or convince someone to develop it for you).

Good luck with your endeavor ;-)

Solution 3:

I built a 1rst order theorem prover in undergrad. It was only a toy compared to the serous provers, but it is a good place to start. To retrace my steps you should:

  • Have confidence in your programing ability
  • Understand the basics of first order logic
  • Understand the resolution algorithm
  • You will need to write a parser for your ATP to be usable (parsing is a big topic, but parser combinators are an easy place to start)

Don't underestimate the time or effort! But you will understand proofs and the foundations of mathematics better for it.

If I remember right, this series of lectures was hugely helpful

In the years since I have found, Handbook of Practical Logic and Automated Reasoning and this lecture series by the author to be a good reference.

I would not be concerned with the aging of a theorem prover. Much of the insight is transferable.

If you are interested in higher order theorem proving Agda is a great place to start.

Solution 4:

You might want to play around with

metamath

and

eprover

a bit.

The Metamath project also wants to formalize all of math.

The latter can answer this question with X = socrates:

fof(all_men_are_mortal, axiom, 
    ![X]: (man(X) => mortal(X))
).

fof(socrates_is_a_man, axiom, 
    man(socrates)
).

% ----------------------------------

fof(who_is_mortal,question,
    ?[X]:mortal(X)
).

?[X]: is $\exists X$ and ![X]: is $\forall X$

You should also know

Related

Lie algebra of a quotient of Lie groups
100 prisoners and a lightbulb
Prove $7^{71}>75^{32}$
Can someone explain the Y Combinator?
Grothendieck's yoga of six operations - in relatively basic terms?
How to prove Lagrange multiplier theorem in a rigorous but intuitive way?
Is there a continuous bijection from $\mathbb{R}$ to $\mathbb{R}^2$
tensor product of sheaves commutes with inverse image
Evaluating $\int^1_0 \frac{\log(1+x)\log(1-x) \log(x)}{x}\, \mathrm dx$
A closed form for $\int_0^\infty\frac{\ln(x+4)}{\sqrt{x\,(x+3)\,(x+4)}}dx$
If sum of reciprocals of numbers is an integer, then there exists a subset with sum of reciprocals of 1
multiplication equivalent of the summation symbol