19
$\begingroup$

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.

$\endgroup$
15
$\begingroup$

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:

$\endgroup$
  • 2
    $\begingroup$ It is probably useful to link to (lists of) proofs where the respective tools have been used, e.g. Archive of Formal Proofs for Isabelle. $\endgroup$ – Raphael Mar 29 '12 at 13:31
  • $\begingroup$ @GuyCoder: For some reason your additions were removed. I added them back in. $\endgroup$ – Dave Clarke Mar 29 '12 at 16:22
  • $\begingroup$ “Some new systems falling into this category include Agda and Epigram.”: seems disappeared. Is there a new location for Eprigram? Or a close alternative? $\endgroup$ – Hibou57 Jul 27 '14 at 3:11
  • 1
    $\begingroup$ “Regarding which ones are still very active, I think they all are. Coq, Isabelle, Twelf, and PVS”: PVS is know to have soundness bugs. Unlike Isabelle and Coq, PVS does not follow the micro‑kernel architecture. Search about the De Bruijn criterion to know why it matters. $\endgroup$ – Hibou57 Jul 27 '14 at 3:16
  • 1
    $\begingroup$ Along to Agda and (defunct?) Epigram, there is the ATS programming language, which according to its mailing list, seems to be active up to now in 2014. $\endgroup$ – Hibou57 Jul 27 '14 at 3:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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