Die Kategorisierung in dieser Liste ist sicherlich noch aktuell.
Vielleicht hat sich eine neue Kategorie herausgebildet, nämlich abhängig typisierte Programmiersprachen . Dies sind im Wesentlichen automatisierte Theorembeweiser, bei denen das Hauptziel nicht das Beweisen von Theoremen, sondern das Programmieren ist. Aufgrund der Curry-Howard-Korrespondenz sind diese beiden Konzepte eng miteinander verknüpft. Das ultimative Ziel solcher Programmiersprachen ist es, Programme zu schreiben, die viel stärkere Garantien haben als reguläre typisierte Programmiersprachen. Die Leute benutzen diese auch für Theorembeweise. Einige neue Systeme, die in diese Kategorie fallen, umfassen Agda und Epigram. Eines der Hauptmerkmale solcher Sprachen besteht darin, dass sie den Programmierern die Definition induktiver Datentypfamilien erheblich erleichtern. Ein einfaches Beispiel ist ein Vektor, der von natürlichen Zahlen abhängt (induktiv definiert).
In Bezug auf diejenigen, die immer noch sehr aktiv sind, denke ich, dass sie es alle sind. Coq , Isabelle , Twelf und PVS werden in der Community der Programmiersprachen häufig verwendet. Maude wird häufig in Modellierungssystemen eingesetzt. (Persönlich habe ich Coq und Maude verwendet .)
Ich hatte noch nie von ein paar gehört. In dem PDF, auf das Sie verlinken, gibt es Links zu den Theoremprüfern. Einige Links sind aktuell, andere defekt. Gandalf scheint jetzt eine Art bärtiger Zauberer zu sein.
Die Theoremprüfer, die in „Ein Überblick über Theoremprüfer“ erwähnt werden, sind:
- ALF : Unter ALFA, Coq und Agda.
- ALFA : scheint nicht länger nicht mehr unterstützt zu werden.
- COQ : aktiv unterstützt.
- MetaPRL : scheint nicht mehr unterstützt zu werden.
- NuPRL : aktiv unterstützt.
- HOL : aktiv unterstützt.
- PVS : aktiv unterstützt.
- Isabelle : aktiv unterstützt.
- TWELF : aktiv unterstützt.
- ACL2 : aktiv unterstützt.
- INKA : scheint nicht mehr unterstützt zu werden.
- GANDALF : scheint nicht mehr unterstützt zu werden.
- TPS : ist möglicherweise noch aktiv, hat aber nur eine geringe Anhängerschaft.
- OTTER : wird möglicherweise nicht mehr unterstützt.
- SETHEO : ersetzt durch E-SETHEO, das anscheinend nicht mehr unterstützt wird.
- SPASS : scheint immer noch aktiv zu sein.
- EQP : scheint nicht mehr unterstützt zu werden.
- MAUDE : sehr aktiv unterstützt.
- OMEGA : scheint nicht mehr unterstützt zu werden.
- Mizar : aktiv unterstützt.
Es gibt zweifellos viele neue automatisierte Theorembeweiser, die in dieser Liste nicht erwähnt wurden.
Der Vollständigkeit halber gibt es , wie von Raphael vorgeschlagen , Beweise für die Site-Archivierung, die mit verschiedenen Tools erstellt wurden. Beispielsweise:
