Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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 (mathemathical logic, programming and other) should one have prior to engaging with automathed theorem proving (ATP)? Are there any fields of mathematical logic that aren't necessary prerequisites but still provide a deeper insighting into ATP?

After the prequisites 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?

share|improve this question
    
Aren't mathematicians doing mathematics the language-agnostic approach? Though I suppose they age as well... –  Cam McLeman Mar 5 '12 at 22:06
    
I think this should be tagged (soft-question). –  user2468 Mar 5 '12 at 22:10
    
It is going to be hard if you do not know your way about (formal) logics. –  Raphael Mar 7 '12 at 11:58

4 Answers 4

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

share|improve this answer
    
thanks for the answer and the wishes. :) –  user5501 Mar 7 '12 at 13:31

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/

share|improve this answer
    
Thanks for the suggestions magma, both Mizar and Theorema sound interesting! –  user5501 Mar 9 '12 at 11:48
    
you are most welcome –  magma Mar 9 '12 at 13:02

I built a 1rst order theorem prover in undergrad. It's 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 program to be usable (parsing is a big topic, if I had to do it again I would use a predefined grammar)

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 http://www.cosmolearning.com/courses/artificial-intelligence-with-prof-p-dasgupta/video-lectures/

share|improve this answer
    
@Q__ If you try this and run into any issues let me know! –  user833970 Apr 4 '13 at 21:53

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

From what I can tell not very. Or at least in certain cases. I say this because of a talk that Michael Beeson gave in Japan. Beeson's notes say:

"This strategy consists in using all the subformulas of the goal, or of the axioms, or of some other theorems or axiom systems in the same logic, as resonators. This amazingly simple strategy was not discovered in 1970, 1980, 1900, or 2003, but in 2008. It is this simple technique that enables automated deduction today to reach the levels of deductive power of Meredith and Lukasiewicz. In particular, this was the technique used to derive Church’s 3-base from Meredith’s single axiom in three hours, just using the subformulas of the single axiom as resonators. The improvements mentioned came from using the subformulas of other known axiom systems as resonators as well. It is worth noting that the change since 1992 is not accounted for by faster computers or larger memory. This could have been done in 1992 if somebody had thought of the subformula strategy then! Michael Beeson Logic and Computers"

Actually, Beeson's first sentence here isn't correct, but fortunately that's not really relevant.

Also, Wos still uses OTTER, even though the author of OTTER went on to develop Prover9 also, and some people claim Prover9 better than OTTER.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.