How to start with automated theorem proving?

Question

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?

Answer 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/

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

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

Answer 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

• The CADE ATP System Competition - The World Championship for Automated Theorem Proving
• The TPTP Problem Library for Automated Theorem Proving
• The TSTP Solution Library for Automated Theorem Proving

Answer 5

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

Answer 6

I have used theorem provers, and written other formal reasoning tools, but I haven't written a theorem prover. A basic understanding of mathematics should suffice to start using a theorem prover. I think that writing one requires years of study and work, and good knowledge of the foundations of mathematics.

The theorem prover I would suggest is TLAPS for the TLA+, the temporal logic of actions introduced by Leslie Lamport. The proof style is hierarchically structured and readable. An introduction to the proof style is this paper and a detailed description is given here.

A good starting point for TLA+ is the book Specifying systems. Some of the notation bears similarity to LaTeX. Theorems and proofs are pretty-printed with the tool tla2tex and LaTeX.

For the mainstream theorem provers there are good books in tutorial style. You may want to look at:

• Isabelle/HOL: Concrete semantics by Tobias Nipkow and Gerwin Klein
• Coq: A tutorial by Mike Nahas
• Lean: A tutorial by Jeremy Avigad, Leonardo de Moura, and Soonho Kong (PDF).

To answer the last question: I'm not aware of any entirely "language agnostic" approaches. Perhaps TLA+ could be regarded as the most generic approach, because it is based on Zermelo-Fraenkel set theory, which serves as foundation for most mathematics done today, and the language reflects the mathematics notation that we usually read and write.

Aging of theorem provers is probably a good thing, as long as they remain maintained and with an active community. Benefits: libraries of formalized mathematical results grow larger, bugs are discovered and corrected, impractical theorem proving projects become unmaintained, thus pointing at the more practical ones (fewer choices -> easier to choose).

There is no choosing the wrong one. You should look or try at least a couple to make an informed decision, similarly to learning several programming languages with different paradigms.

A list of several theorem provers can be found here.