Types of Automated Theorem Provers

Question

^{I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here.}

Which are the relevant automated theorem provers? I found A Review of Theorem Provers

Is this still current?

Which ones are still very active, i.e. which are currently used beyond the group that created it?

^{Find the series' next question here.}

Answer 1

The categorization in that list is certainly still current.

Perhaps one new category has emerged, namely, dependently-typed programming languages. These are essentially automated theorem provers where the primary goal is not proving theorems, but programming. Due to the Curry-Howard correspondence, these two concepts are strongly intertwined. The ultimate goal of such programming languages is to write programs that have much stronger guarantees than regular typed programming languages. People also use these for theorem proving. Some new systems falling into this category include Agda and Epigram. One of the key characteristics of such languages is that they put a lot of effort into making it easier for programmers to define inductive families of datatypes. A simple example is a vector, which depends upon natural numbers (defined inductively).

Regarding which ones are still very active, I think they all are. Coq, Isabelle, Twelf, and PVS are used a lot in the programming languages community. Maude is used extensively in modelling systems. (Personally, I've used Coq and Maude.)

I'd never heard of a few of them. In the pdf you link to, there are links to the theorem provers. Some links are current, some are broken. Gandalf now seems to be some sort of bearded wizard.

The theorem provers mentioned in “A Review of Theorem Provers” are:

• ALF: subsumbed by ALFA, Coq, and Agda.
• ALFA: seems to no longer unsupported.
• COQ: actively supported.
• MetaPRL: seems to be no longer supported.
• NuPRL: actively supported.
• HOL: actively supported.
• PVS: actively supported.
• Isabelle: actively supported.
• TWELF: actively supported.
• ACL2: actively supported.
• INKA: seems to be no longer supported.
• GANDALF: seems to be no longer supported.
• TPS: may still be active, but has only a small following.
• OTTER: may no longer be supported.
• SETHEO: replaced by E-SETHEO, which seems to no longer be supported.
• SPASS: seems to be still active.
• EQP: seems to be no longer supported.
• MAUDE: very actively supported.
• OMEGA: seems to be no longer supported.
• Mizar: actively supported.

There are undoubtedly many new automated theorem provers that have not been mentioned in this list.

For completeness, as suggested by Raphael, there are site archiving proofs made using various tools. For example:

• The Archive of Formal Proofs for Isabelle
• Formalized Mathematics for Mizar
• The Constructive Coq Repository
• The ACL2 Books Directory
• Selections from the PRL Math Library
• NASA Langley PVS Libraries